Homomorphism indistinguishability

A Lean 4 / Mathlib formalisation of Lovász's theorem and of the results of Logical equivalences, homomorphism indistinguishability, and forbidden minors doi:10.1016/j.ic.2024.105224.

Libraries

The development is split into five libraries, each depending only on the ones above it.

Library	Contents	Status
GraphTheory	Graph-theoretic constructions extending Mathlib, with no homomorphism counting	complete
Hom	Counting homomorphisms	complete
Lovasz	Lovász's theorem	complete
HomInd	Homomorphism indistinguishability and the distinguishing closure	complete
PreservationClosure	The theorems of the paper	complete

GraphTheory

File	Contents
Prod.lean	The categorical (tensor) product ×g, following Mathlib's Prod.lean for the box product □
Sum.lean	Structural facts about ⊕g: walks and homomorphisms stay on one side
Sigma.lean	Indexed disjoint unions SimpleGraph.sigma and sigmaOn, the decomposition of a graph into its connected components, and the reindexing/splitting isomorphisms
LoopGraph.lean	Graphs with loops, the full complement X̂, the looped graph G°, and (G°)^ = Gᶜ
Minor.lean	SimpleGraph.MinorModel and SimpleGraph.IsMinor, spanning subgraphs, contraction quotients F ⊘ L, the equivalence of minors with deleting vertices, deleting edges and contracting edges, and the behaviour of minor models under a single edge contraction

Hom

File	Contents
Count.lean	The image subgraph Hom.range, strongly surjective homomorphisms, and the counting functions homCount, surjCount, injCount, autCount (all defined with Nat.card)
Basic.lean	hom(G ⊕g H, K) = hom(G,K)·hom(H,K), hom(K, G ×g H) = hom(K,G)·hom(K,H), hom(K, G ⊕g H) = hom(K,G) + hom(K,H) for connected K — Lovász, Large Networks and Graph Limits, (5.28)–(5.30) — and the splitting off of isolated vertices
Sigma.lean	hom(∐ i, Gᵢ, K) = ∏ i, hom(Gᵢ, K)
DisjUnion.lean	Decomposition of homomorphism counts over connected components, and eq:disjunion
LoopGraph.lean	Homomorphism counts of graphs with loops
Complement.lean	Equation (5.23), lem:looping, eq:del-contr, and eq:del-contr as a linear combination of homomorphism counts from graphs on Fin _

Lovasz

File	Contents
HomMatrix.lean	GraphFamily, the matrices homMatrix, surjMatrix, injMatrix, autDiag, the factorisation M = S · D⁻¹ · I, triangularity, and Lovász's matrix lemma homMatrix_isUnit
Basic.lean	The family of representatives repFamily, and Lovász's theorem in bounded, unbounded and TFAE form

HomInd

File	Contents
Basic.lean	GraphClass, homomorphism indistinguishability G ≡[𝓕] H, the distinguishing closure cl 𝓕, and lem:lincomb (in two forms: with all coefficients nonzero, and picking out the nonzero ones)
Closure.lean	Closure and preservation properties, the grouping lemmas, lem:minors, and minor-closedness from the three atomic operations (also in the form needing only single-edge contraction)

PreservationClosure

File	Contents
Summands.lean	thm:taking-summands
Complement.lean	thm:complement

Main results

theorem SimpleGraph.tfae_homCount_eq [Finite V] [Finite W] {n : ℕ}
    (hV : Nat.card V ≤ n) (hW : Nat.card W ≤ n) :
    List.TFAE
      [∀ (m : ℕ) (K : SimpleGraph (Fin m)), homCount K G = homCount K H,
       ∀ m ≤ n, ∀ K : SimpleGraph (Fin m), homCount K G = homCount K H,
       Nonempty (G ≃g H)]

theorem SimpleGraph.GraphClass.preservedUnderDisjointUnion_iff_cl_isSummandClosed
    (𝓕 : GraphClass) : 𝓕.PreservedUnderDisjointUnion ↔ 𝓕.cl.IsSummandClosed

theorem SimpleGraph.GraphClass.preservedUnderCompl_iff_cl_isMinorClosed
    (𝓕 : GraphClass) : 𝓕.PreservedUnderCompl ↔ 𝓕.cl.IsMinorClosed

The development is complete: no sorry anywhere, and the three theorems above depend only on propext, Classical.choice and Quot.sound.

Building

lake exe cache get   # optional, fetches Mathlib oleans
lake build