Lax Lean Archive

The homomorphism distinguishing closure

Lax871432.DistinguishingClosure · concepts/Lax871432/DistinguishingClosure.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

    The homomorphism distinguishing closure of a graph class F\mathcal{F} is

    cl(F)≔{K∣∀G,H. G≡FH⇒hom⁡(K,G)=hom⁡(K,H)},\mathrm{cl}(\mathcal{F}) \coloneqq \{K \mid \forall G, H.\ G \equiv_{\mathcal{F}} H \Rightarrow \hom(K, G) = \hom(K, H)\},

    the largest graph class whose homomorphism indistinguishability relation coincides with that of F\mathcal{F}. A class is homomorphism distinguishing closed if it equals its own closure, i.e. if adding any further graph strictly refines its homomorphism indistinguishability relation.

    Concept map
    5 concepts; 8 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 Lax871432.HomomorphismIndistinguishability
    2
    3/-!
    4---
    5title: The homomorphism distinguishing closure
    6type: definition
    7---
    8The *homomorphism distinguishing closure* of a graph class
    9F\mathcal{F} is
    10cl(F)≔{K∣∀G,H. G≡FH⇒hom⁡(K,G)=hom⁡(K,H)},\mathrm{cl}(\mathcal{F}) \coloneqq \{K \mid \forall G, H.\ G \equiv_{\mathcal{F}} H \Rightarrow \hom(K, G) = \hom(K, H)\},
    11
    12the largest graph class whose homomorphism indistinguishability relation coincides with that
    13of F\mathcal{F}. A class is *homomorphism distinguishing closed* if it equals its own
    14closure, i.e. if adding any further graph strictly refines its homomorphism
    15indistinguishability relation.
    16-/
    17
    18open Lax871432.GraphClasses
    19open Lax871432.HomomorphismCounts Lax871432.HomomorphismIndistinguishability
    20open Lax871432.IsomorphismRelaxations
    21
    22open scoped Lax871432.HomomorphismIndistinguishability
    23
    24namespace Lax871432.DistinguishingClosure
    25
    26/-- The relaxation `R` *determines* the homomorphism counts of `K` if related graphs receive
    27equally many homomorphisms from `K`. -/
    28structure Determines (R : GraphIsoRelaxation) {U : Type} [Finite U] (K : SimpleGraph U) :
    29 Prop where
    30 /-- Graphs related by `R` receive equally many homomorphisms from `K`. -/
    31 homCount_eq : ∀ {V W : Type} [Finite V] [Finite W] (G : SimpleGraph V) (H : SimpleGraph W),
    32 R.Rel G H → homCount K G = homCount K H
    33
    34/-- cl(F)\mathrm{cl}(\mathcal{F}), the homomorphism distinguishing closure of `𝓕`. -/
    35def cl (𝓕 : GraphClass) : GraphClass where
    36 Mem K := Determines (homIndRel 𝓕) K
    37 mem_congr {_ _ _ _ F F'} he := by
    38 -- Precomposition with the isomorphism is a bijection between the homomorphisms out of
    39 -- `F` and those out of `F'`, so the two are counted alike into every target.
    40 obtain ⟨e⟩ := he
    41 have key : ∀ {W : Type} (K : SimpleGraph W), homCount F K = homCount F' K := fun K =>
    42 Nat.card_congr
    43 { toFun f := f.comp e.symm.toHom
    44 invFun f := f.comp e.toHom
    45 left_inv _ := by ext a; exact congrArg _ (e.symm_apply_apply a)
    46 right_inv _ := by ext a; exact congrArg _ (e.apply_symm_apply a) }
    47 constructor <;> intro h <;> refine ⟨fun G H hGH => ?_⟩
    48 · rw [← key G, ← key H]; exact h.homCount_eq G H hGH
    49 · rw [key G, key H]; exact h.homCount_eq G H hGH
    50
    51/-- `𝓕` is *homomorphism distinguishing closed* if it contains its own closure, i.e. if
    52adding any graph to `𝓕` strictly refines ≡F\equiv_{\mathcal{F}}. -/
    53def IsHomDistinguishingClosed (𝓕 : GraphClass) : Prop :=
    54 ∀ ⦃V : Type⦄ [Finite V] (F : SimpleGraph V), (cl 𝓕).Mem F → 𝓕.Mem F
    55
    56end Lax871432.DistinguishingClosure
    57
    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…