Lax Lean Archive

Homomorphism indistinguishability

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

definition

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

    Definition

    Two graphs GG and HH are homomorphism indistinguishable over a class F\mathcal{F}, written G≡FHG \equiv_{\mathcal{F}} H, if hom⁡(F,G)=hom⁡(F,H)\hom(F, G) = \hom(F, H) for every F∈FF \in \mathcal{F}.

    Since hom⁡(F,−)\hom(F, -) is an isomorphism invariant, this is a graph isomorphism relaxation, and it is defined as one: homIndRelFhomIndRel \mathcal{F} is the relaxation itself, and G≡FHG \equiv_{\mathcal{F}} H is notation for the relation it carries.

    Concept map
    4 concepts; 10 descendants hidden
    100%
    Proven claimOpen claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 3 of this submission's paper

    Lean source view on GitHub

    1import Mathlib.SetTheory.Cardinal.NatCard
    2import Lax871432.GraphClasses
    3import Lax871432.HomomorphismCounts
    4import Lax871432.IsomorphismRelaxations
    5
    6/-!
    7---
    8title: Homomorphism indistinguishability
    9type: definition
    10---
    11Two graphs GG and HH are *homomorphism indistinguishable over a class F\mathcal{F}*,
    12written G≡FHG \equiv_{\mathcal{F}} H, if hom⁡(F,G)=hom⁡(F,H)\hom(F, G) = \hom(F, H) for every
    13F∈FF \in \mathcal{F}.
    14
    15Since hom⁡(F,−)\hom(F, -) is an isomorphism invariant, this is a graph isomorphism relaxation, and
    16it is defined as one: `homIndRel 𝓕` is the relaxation itself, and
    17G≡FHG \equiv_{\mathcal{F}} H is notation for the relation it carries.
    18-/
    19
    20open Lax871432.GraphClasses Lax871432.HomomorphismCounts Lax871432.IsomorphismRelaxations
    21
    22namespace Lax871432.HomomorphismIndistinguishability
    23
    24/-- *Homomorphism indistinguishability over `𝓕`*: the graph isomorphism relaxation relating
    25two graphs when they receive the same number of homomorphisms from every graph of `𝓕`. -/
    26def homIndRel (𝓕 : GraphClass) : GraphIsoRelaxation where
    27 Rel := @fun _ _ _ _ G H =>
    28 ∀ ⦃m : ℕ⦄ (F : SimpleGraph (Fin m)), 𝓕.Mem F → homCount F G = homCount F H
    29 rel_of_iso := by
    30 -- Postcomposing with the isomorphism is a bijection between the two hom-sets, so
    31 -- isomorphic graphs receive equally many homomorphisms from every graph.
    32 rintro V W _ _ G H ⟨e⟩ m F -
    33 exact Nat.card_congr
    34 { toFun f := e.toHom.comp f
    35 invFun f := e.symm.toHom.comp f
    36 left_inv _ := by ext a; simp
    37 right_inv _ := by ext a; simp }
    38 symm := by
    39 intro V W _ _ G H h m F hF
    40 exact (h F hF).symm
    41 trans := by
    42 intro U V W _ _ _ G H K h h' m F hF
    43 exact (h F hF).trans (h' F hF)
    44
    45@[inherit_doc homIndRel]
    46scoped notation:50 G " ≡[" 𝓕 "] " H => GraphIsoRelaxation.Rel (homIndRel 𝓕) G H
    47
    48end Lax871432.HomomorphismIndistinguishability
    49
    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…