Lax Lean Archive

Graph classes

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

    A graph class is a class F\mathcal{F} of finite simple graphs which is closed under isomorphism: if F∈FF \in \mathcal{F} and F≅F′F \cong F', then F′∈FF' \in \mathcal{F}.

    Graph classes are ordered by inclusion, F⊆F′\mathcal{F} \subseteq \mathcal{F}', written F≤F′\mathcal{F} ≤ \mathcal{F}'. The intersection ⋂i∈IFi\bigcap_{i \in I} \mathcal{F}_i and the union ⋃i∈IFi\bigcup_{i \in I} \mathcal{F}_i of a family of graph classes are again graph classes, written ⨅i,Fi⨅ i, \mathcal{F} i and ⨆i,Fi⨆ i, \mathcal{F} i.

    Concept map
    1 concept; 12 descendants hidden
    100%
    Proven claimOpen claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Maps
    2import Mathlib.Order.SetNotation
    3
    4/-!
    5---
    6title: Graph classes
    7type: definition
    8---
    9A *graph class* is a class F\mathcal{F} of finite simple graphs which is closed under
    10isomorphism: if F∈FF \in \mathcal{F} and F≅F′F \cong F', then F′∈FF' \in \mathcal{F}.
    11
    12Graph classes are ordered by inclusion, F⊆F′\mathcal{F} \subseteq \mathcal{F}', written
    13`𝓕 ≤ 𝓕'`. The intersection ⋂i∈IFi\bigcap_{i \in I} \mathcal{F}_i and the union
    14⋃i∈IFi\bigcup_{i \in I} \mathcal{F}_i of a family of graph classes are again graph classes,
    15written `⨅ i, 𝓕 i` and `⨆ i, 𝓕 i`.
    16
    17# Implementation notes
    18
    19A class of finite simple graphs cannot be a `Set` of graphs, since graphs live over arbitrary
    20vertex types. The underlying datum is therefore a predicate on the finite simple graphs over
    21an arbitrary vertex type, together with a proof that it is invariant under isomorphism.
    22
    23The results about graph classes need that invariance — the homomorphism distinguishing
    24closure is defined by a condition on all graphs of a given isomorphism type — so it is carried
    25in the structure rather than assumed afresh in every statement.
    26
    27The vertex types range over `Type` rather than over an arbitrary universe, matching the
    28quantifiers of `GraphIsoRelaxation`. A universe-polymorphic `Mem` is not available here: a
    29`Type*` in a structure field is not quantified inside the field, it becomes a parameter of
    30`GraphClass` itself, so a class would be tied to one fixed universe instead of covering them
    31all. Fixing `Type` is no loss of generality either, since every finite graph is isomorphic to
    32a graph on some `Fin n` and membership is invariant under isomorphism.
    33-/
    34
    35namespace Lax871432.GraphClasses
    36
    37/-- A class of finite simple graphs, given by an isomorphism-invariant predicate on the
    38finite simple graphs. -/
    39structure GraphClass where
    40 /-- The graphs of the class. -/
    41 Mem : ∀ {V : Type} [Finite V], SimpleGraph V → Prop
    42 /-- The class is invariant under isomorphism. -/
    43 mem_congr : ∀ {V W : Type} [Finite V] [Finite W] {F : SimpleGraph V} {F' : SimpleGraph W},
    44 Nonempty (F ≃g F') → (Mem F ↔ Mem F')
    45
    46/-- Inclusion of graph classes: `𝓕 ≤ 𝓕'` if every graph in `𝓕` is in `𝓕'`. -/
    47instance : PartialOrder GraphClass where
    48 le 𝓕 𝓕' := ∀ ⦃V : Type⦄ [Finite V] (F : SimpleGraph V), 𝓕.Mem F → 𝓕'.Mem F
    49 le_refl _ _ _ _ hF := hF
    50 le_trans _ _ _ h h' _ _ F hF := h' F (h F hF)
    51 le_antisymm := by
    52 rintro ⟨Mem, _⟩ ⟨Mem', _⟩ h h'
    53 have : @Mem = @Mem' := by
    54 funext V _ F
    55 exact propext ⟨h F, h' F⟩
    56 subst this
    57 rfl
    58
    59/-- The intersection of a set of graph classes: the graphs lying in each of them. The
    60intersection of a family is written `⨅ i, 𝓕 i`. -/
    61instance : InfSet GraphClass where
    62 sInf S :=
    63 { Mem F := ∀ 𝓕 ∈ S, 𝓕.Mem F
    64 mem_congr he :=
    65 forall_congr' fun 𝓕 : GraphClass => imp_congr_right fun _ => 𝓕.mem_congr he }
    66
    67/-- The union of a set of graph classes: the graphs lying in at least one of them. The union
    68of a family is written `⨆ i, 𝓕 i`. -/
    69instance : SupSet GraphClass where
    70 sSup S :=
    71 { Mem F := ∃ 𝓕 ∈ S, 𝓕.Mem F
    72 mem_congr he := exists_congr fun 𝓕 : GraphClass => and_congr_right' (𝓕.mem_congr he) }
    73
    74end Lax871432.GraphClasses
    75

    Implementation notes

    A class of finite simple graphs cannot be a SetSet of graphs, since graphs live over arbitrary vertex types. The underlying datum is therefore a predicate on the finite simple graphs over an arbitrary vertex type, together with a proof that it is invariant under isomorphism.

    The results about graph classes need that invariance — the homomorphism distinguishing closure is defined by a condition on all graphs of a given isomorphism type — so it is carried in the structure rather than assumed afresh in every statement.

    The vertex types range over TypeType rather than over an arbitrary universe, matching the quantifiers of GraphIsoRelaxationGraphIsoRelaxation. A universe-polymorphic MemMem is not available here: a Type∗Type* in a structure field is not quantified inside the field, it becomes a parameter of GraphClassGraphClass itself, so a class would be tied to one fixed universe instead of covering them all. Fixing TypeType is no loss of generality either, since every finite graph is isomorphic to a graph on some FinnFin n and membership is invariant under isomorphism.

    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…