Graph classes

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

definition

Loading review…

Natural Language Statement

Definition

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

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

Concept map

1 concept

100%

DefinitionThis conceptDescendants are omitted for concepts with more than 10 descendants.

In the paper

page 1 of the paper of lax-326031, Graph Classes and Width Parameters

Lean source view on GitHub

Show types on hover

1	import Mathlib.Combinatorics.SimpleGraph.Maps
2	import Mathlib.Order.SetNotation
3
4	/-!
5	---
6	title: Graph classes
7	type: definition
8	---
9	A graph class is a class $\mathcal{F}$ of finite simple graphs which is closed under
10	isomorphism: if $F \in \mathcal{F}$ and $F \cong F'$ , then $F' \in \mathcal{F}$ .
11
12	Graph classes are ordered by inclusion, $\mathcal{F} \subseteq \mathcal{F}'$ , written
13	`𝓕 ≤ 𝓕'`. The intersection $\bigcap_{i \in I} \mathcal{F}_i$ and the union
14	$\bigcup_{i \in I} \mathcal{F}_i$ of a family of graph classes are again graph classes,
15	written `⨅ i, 𝓕 i` and `⨆ i, 𝓕 i`.
16
17	# Implementation notes
18
19	A class of finite simple graphs cannot be a `Set` of graphs, since graphs live over arbitrary
20	vertex types. The underlying datum is therefore a predicate on the finite simple graphs over
21	an arbitrary vertex type, together with a proof that it is invariant under isomorphism.
22
23	The results about graph classes need that invariance — the homomorphism distinguishing
24	closure is defined by a condition on all graphs of a given isomorphism type — so it is carried
25	in the structure rather than assumed afresh in every statement.
26
27	The vertex types range over `Type` rather than over an arbitrary universe, matching the
28	quantifiers 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
31	all. Fixing `Type` is no loss of generality either, since every finite graph is isomorphic to
32	a graph on some `Fin n` and membership is invariant under isomorphism.
33	-/
34
35	namespace Lax871432.GraphClasses
36
37	/-- A class of finite simple graphs, given by an isomorphism-invariant predicate on the
38	finite simple graphs. -/
39	structure 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 `𝓕'`. -/
47	instance : 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
60	intersection of a family is written `⨅ i, 𝓕 i`. -/
61	instance : 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
68	of a family is written `⨆ i, 𝓕 i`. -/
69	instance : 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
74	end Lax871432.GraphClasses
75

Implementation notes

A class of finite simple graphs cannot be a $Set$ 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 $Type$ rather than over an arbitrary universe, matching the quantifiers of $GraphIsoRelaxation$ . A universe-polymorphic $Mem$ is not available here: a $Type*$ in a structure field is not quantified inside the field, it becomes a parameter of $GraphClass$ itself, so a class would be tied to one fixed universe instead of covering them all. Fixing $Type$ is no loss of generality either, since every finite graph is isomorphic to a graph on some $Fin 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…

Lax Lean Archive

Graph classes

Flags

Flag this concept