Partitions into connected parts

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

definition

Loading review…

Natural Language Statement

Definition

A partition into connected parts of a simple graph $F$ is a partition $\mathcal{R}$ of $V(F)$ such that the subgraph $F[R]$ induced by every class $R \in \mathcal{R}$ is connected.

Concept map

1 concept; 1 descendant hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 4 of this submission's paper

Lean source view on GitHub

1	import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
2
3	/-!
4	---
5	title: Partitions into connected parts
6	type: definition
7	---
8	A partition into connected parts of a simple graph $F$ is a partition $\mathcal{R}$ of
9	$V(F)$ such that the subgraph $F[R]$ induced by every class $R \in \mathcal{R}$ is connected.
10
11	# Comments
12
13	Two graphs are attached to such a partition: the quotient $F / \mathcal{R}$ , whose vertices
14	are the classes and in which two distinct classes are adjacent when some edge of $F$ joins
15	them, and the disjoint union $\coprod_{R \in \mathcal{R}} F[R]$ of the induced subgraphs.
16	These are the two graphs occurring in the formula for the number of homomorphisms into a
17	lexicographic product.
18
19	The quotient by a partition into connected parts is exactly a contraction of $F$ : its
20	projection has connected fibres, which is the defining property of a contraction. Conversely,
21	every contraction arises this way, from the partition into the fibres of its projection.
22
23	# Implementation notes
24
25	A partition of `V(F)` is given as a `Setoid V`, so that the classes are the fibres of the
26	canonical projection to the quotient type and no choice of representatives is involved. The
27	connectedness requirement is stated for the subgraph induced on the fibre over each point of
28	the quotient.
29
30	`parts` is the disjoint union of the induced subgraphs, indexed by the classes: its vertices
31	are pairs consisting of a class and a vertex of that class, and two of them are adjacent when
32	they are adjacent in `F` and lie in the same class. Since the ambient graph is `F` itself,
33	this is stated without a dependent rewrite.
34	-/
35
36	namespace Lax871432.ConnectedPartitions
37
38	variable {V : Type*}
39
40	/-- A partition of the vertices of `F`, all of whose classes induce connected subgraphs. -/
41	structure ConnPart (F : SimpleGraph V) where
42	/-- The partition, as an equivalence relation on the vertices. -/
43	setoid : Setoid V
44	/-- Every class induces a connected subgraph of `F`. -/
45	connected : ∀ a : Quotient setoid, (F.induce {v \| Quotient.mk setoid v = a}).Connected
46
47	namespace ConnPart
48
49	variable {F : SimpleGraph V} (𝓡 : ConnPart F)
50
51	/-- The class of a vertex. -/
52	def proj (v : V) : Quotient 𝓡.setoid := Quotient.mk 𝓡.setoid v
53
54	/-- The subgraph of `F` induced by a class. -/
55	def part (a : Quotient 𝓡.setoid) : SimpleGraph {v \| 𝓡.proj v = a} := F.induce _
56
57	/-- The quotient `F / 𝓡`: distinct classes are adjacent when `F` joins them. -/
58	def quotientGraph : SimpleGraph (Quotient 𝓡.setoid) where
59	Adj a b := a ≠ b ∧ ∃ x y, F.Adj x y ∧ 𝓡.proj x = a ∧ 𝓡.proj y = b
60	symm := ⟨fun _ _ h => by
61	obtain ⟨hne, x, y, hxy, hx, hy⟩ := h
62	exact ⟨hne.symm, y, x, hxy.symm, hy, hx⟩⟩
63	loopless := ⟨fun _ h => h.1 rfl⟩
64
65	/-- `∐ R ∈ 𝓡, F[R]`, the disjoint union of the subgraphs induced by the classes. -/
66	def parts : SimpleGraph (Σ a : Quotient 𝓡.setoid, {v \| 𝓡.proj v = a}) where
67	Adj p q := F.Adj p.2.1 q.2.1 ∧ 𝓡.proj p.2.1 = 𝓡.proj q.2.1
68	symm := ⟨fun _ _ h => ⟨h.1.symm, h.2.symm⟩⟩
69	loopless := ⟨fun _ h => F.irrefl h.1⟩
70
71
72	/-- A finite graph has finitely many partitions into connected parts. -/
73	instance instFinite [Finite V] : Finite (ConnPart F) :=
74	Finite.of_injective (fun 𝓡 => (𝓡.setoid.r : V → V → Prop)) <\| by
75	intro R S h
76	obtain ⟨s, hs⟩ := R
77	obtain ⟨t, ht⟩ := S
78	obtain rfl : s = t := Setoid.ext fun a b => Eq.to_iff (congrFun (congrFun h a) b)
79	rfl
80
81	noncomputable instance instFintype [Finite V] : Fintype (ConnPart F) := Fintype.ofFinite _
82
83	end ConnPart
84
85	end Lax871432.ConnectedPartitions
86

Comments

Two graphs are attached to such a partition: the quotient $F / \mathcal{R}$ , whose vertices are the classes and in which two distinct classes are adjacent when some edge of $F$ joins them, and the disjoint union $\coprod_{R \in \mathcal{R}} F[R]$ of the induced subgraphs. These are the two graphs occurring in the formula for the number of homomorphisms into a lexicographic product.

The quotient by a partition into connected parts is exactly a contraction of $F$ : its projection has connected fibres, which is the defining property of a contraction. Conversely, every contraction arises this way, from the partition into the fibres of its projection.

Implementation notes

A partition of $V(F)$ is given as a $Setoid V$ , so that the classes are the fibres of the canonical projection to the quotient type and no choice of representatives is involved. The connectedness requirement is stated for the subgraph induced on the fibre over each point of the quotient.

$parts$ is the disjoint union of the induced subgraphs, indexed by the classes: its vertices are pairs consisting of a class and a vertex of that class, and two of them are adjacent when they are adjacent in $F$ and lie in the same class. Since the ambient graph is $F$ itself, this is stated without a dependent rewrite.

Builds on

none

Used by

Lax871432.LexicographicProductCounts

From Mathlib

Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Discussion

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

Loading discussion…

Lax Lean Archive

Partitions into connected parts

Flags

Flag this concept