Lax Lean Archive

Lovász's theorem

Lax871432.LovaszTheorem · concepts/Lax871432/LovaszTheorem.lean · lax-871432

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Lovász (1967): two finite graphs are isomorphic if and only if they are homomorphism indistinguishable over all graphs, i.e. if and only if hom⁡(K,G)=hom⁡(K,H)\hom(K, G) = \hom(K, H) for every graph KK.

    It suffices to test the graphs KK on vertex set {0,…,m−1}\{0, \dots, m-1\}, since every finite graph is isomorphic to one of these and hom⁡(−,G)\hom(-, G) is an isomorphism invariant.

    The theorem is deduced from the invertibility of the homomorphism matrix of a family of graphs. Let F1,…,FNF_1, \dots, F_N be pairwise non-isomorphic graphs on at most nn vertices which represent every isomorphism class of graphs on at most nn vertices. Then the matrix Mij=hom⁡(Fi,Fj)M_{ij} = \hom(F_i, F_j) is invertible over Q\mathbb{Q}.

    Concept map
    3 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 homMatrix_isUnit proven

    2 nonempty_iso_iff_forall_homCount_eq proven

    In the paper

    • page 1 of this submission's paper
    • page 4 of this submission's paper

    Lean source view on GitHub

    1import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
    2import Lax871432.GraphFamilies
    3import Lax871432.HomomorphismCounts
    4
    5/-!
    6---
    7title: Lovász's theorem
    8type: theorem
    9---
    10Lovász (1967): two finite graphs are isomorphic if and only if they are homomorphism
    11indistinguishable over all graphs, i.e. if and only if hom⁡(K,G)=hom⁡(K,H)\hom(K, G) = \hom(K, H) for every
    12graph KK.
    13
    14It suffices to test the graphs KK on vertex set {0,…,m−1}\{0, \dots, m-1\}, since every finite
    15graph is isomorphic to one of these and hom⁡(−,G)\hom(-, G) is an isomorphism invariant.
    16
    17The theorem is deduced from the invertibility of the *homomorphism matrix* of a family of
    18graphs. Let F1,…,FNF_1, \dots, F_N be pairwise non-isomorphic graphs on at most nn vertices which
    19represent every isomorphism class of graphs on at most nn vertices. Then the matrix
    20Mij=hom⁡(Fi,Fj)M_{ij} = \hom(F_i, F_j) is invertible over Q\mathbb{Q}.
    21
    22# Implementation notes
    23
    24The family F1,…,FNF_1, \dots, F_N is a `GraphFamily`, indexed by a type `ι` that then also indexes
    25the rows and columns of the matrix.
    26-/
    27
    28open Lax871432.GraphFamilies Lax871432.HomomorphismCounts
    29
    30namespace Lax871432.LovaszTheorem
    31
    32variable {n : ℕ} {ι : Type*}
    33
    34/-- The *homomorphism matrix* of a graph family, `M i j = hom(F i, F j)`. -/
    35noncomputable def homMatrix (F : GraphFamily n ι) : Matrix ι ι ℚ :=
    36 Matrix.of fun i j => (homCount (F.graph i) (F.graph j) : ℚ)
    37
    38/-- **Lovász's homomorphism matrix lemma.** For a finite family of pairwise non-isomorphic
    39graphs on at most `n` vertices which represents every isomorphism class of graphs on at most
    40`n` vertices, the matrix of homomorphism counts between its members is invertible. -/
    41axiom homMatrix_isUnit [Fintype ι] [DecidableEq ι] (F : GraphFamily n ι)
    42 (hni : F.PairwiseNonIso) (hF : F.IsExhaustive) : IsUnit (homMatrix F)
    43
    44/-- **Lovász's theorem.** Finite graphs with equal homomorphism counts from every graph are
    45isomorphic, and conversely. -/
    46axiom nonempty_iso_iff_forall_homCount_eq {V W : Type} [Finite V] [Finite W]
    47 (G : SimpleGraph V) (H : SimpleGraph W) :
    48 (∀ (m : ℕ) (K : SimpleGraph (Fin m)), homCount K G = homCount K H) ↔ Nonempty (G ≃g H)
    49
    50end Lax871432.LovaszTheorem
    51
    Show ProofShow Proof

    Implementation notes

    The family F1,…,FNF_1, \dots, F_N is a GraphFamilyGraphFamily, indexed by a type ιι that then also indexes the rows and columns of the matrix.

    Builds on
    Used by

    none

    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…