From cbf3062bbc75ad2ca7757e1196690721d6f6b5e8 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Thu, 14 Apr 2022 17:32:49 +0000
Subject: [PATCH] feat(combinatorics/simple_graph/connectivity): define
 connected components (#12766)

---
 .../simple_graph/connectivity.lean            | 66 ++++++++++++++++++-
 1 file changed, 64 insertions(+), 2 deletions(-)

diff --git a/src/combinatorics/simple_graph/connectivity.lean b/src/combinatorics/simple_graph/connectivity.lean
index b582e5ca141e5..32409689aa3dc 100644
--- a/src/combinatorics/simple_graph/connectivity.lean
+++ b/src/combinatorics/simple_graph/connectivity.lean
@@ -52,6 +52,9 @@ counterparts in [Chou1994].
 * `simple_graph.subgraph.connected` gives subgraphs the connectivity
   predicate via `simple_graph.subgraph.coe`.
 
+* `simple_graph.connected_component` is the type of connected components of
+  a given graph.
+
 ## Tags
 walks, trails, paths, circuits, cycles
 
@@ -988,11 +991,70 @@ structure connected : Prop :=
 instance : has_coe_to_fun G.connected (λ _, Π (u v : V), G.reachable u v) :=
 ⟨λ h, h.preconnected⟩
 
-/-- A subgraph is connected if it is connected as a simple graph. -/
-abbreviation subgraph.connected {G : simple_graph V} (H : G.subgraph) : Prop := H.coe.connected
+/-- The quotient of `V` by the `simple_graph.reachable` relation gives the connected
+components of a graph. -/
+def connected_component := quot G.reachable
+
+/-- Gives the connected component containing a particular vertex. -/
+def connected_component_mk (v : V) : G.connected_component := quot.mk G.reachable v
 
+instance connected_component.inhabited [inhabited V] : inhabited G.connected_component :=
+⟨G.connected_component_mk default⟩
+
+section connected_component
 variables {G}
 
+@[elab_as_eliminator]
+protected lemma connected_component.ind {β : G.connected_component → Prop}
+  (h : ∀ (v : V), β (G.connected_component_mk v)) (c : G.connected_component) : β c :=
+quot.ind h c
+
+@[elab_as_eliminator]
+protected lemma connected_component.ind₂ {β : G.connected_component → G.connected_component → Prop}
+  (h : ∀ (v w : V), β (G.connected_component_mk v) (G.connected_component_mk w))
+  (c d : G.connected_component) : β c d :=
+quot.induction_on₂ c d h
+
+protected lemma connected_component.sound {v w : V} :
+  G.reachable v w → G.connected_component_mk v = G.connected_component_mk w := quot.sound
+
+protected lemma connected_component.exact {v w : V} :
+  G.connected_component_mk v = G.connected_component_mk w → G.reachable v w :=
+@quotient.exact _ G.reachable_setoid _ _
+
+@[simp] protected lemma connected_component.eq {v w : V} :
+  G.connected_component_mk v = G.connected_component_mk w ↔ G.reachable v w :=
+@quotient.eq _ G.reachable_setoid _ _
+
+/-- The `connected_component` specialization of `quot.lift`. Provides the stronger
+assumption that the vertices are connected by a path. -/
+protected def connected_component.lift {β : Sort*} (f : V → β)
+  (h : ∀ (v w : V) (p : G.walk v w), p.is_path → f v = f w) : G.connected_component → β :=
+quot.lift f (λ v w (h' : G.reachable v w), h'.elim_path (λ hp, h v w hp hp.2))
+
+@[simp] protected lemma connected_component.lift_mk {β : Sort*} {f : V → β}
+  {h : ∀ (v w : V) (p : G.walk v w), p.is_path → f v = f w} {v : V} :
+  connected_component.lift f h (G.connected_component_mk v) = f v := rfl
+
+protected lemma connected_component.«exists» {p : G.connected_component → Prop} :
+  (∃ (c : G.connected_component), p c) ↔ ∃ v, p (G.connected_component_mk v) :=
+(surjective_quot_mk G.reachable).exists
+
+protected lemma connected_component.«forall» {p : G.connected_component → Prop} :
+  (∀ (c : G.connected_component), p c) ↔ ∀ v, p (G.connected_component_mk v) :=
+(surjective_quot_mk G.reachable).forall
+
+lemma preconnected.subsingleton_connected_component (h : G.preconnected) :
+  subsingleton G.connected_component :=
+⟨connected_component.ind₂ (λ v w, connected_component.sound (h v w))⟩
+
+end connected_component
+
+variables {G}
+
+/-- A subgraph is connected if it is connected as a simple graph. -/
+abbreviation subgraph.connected (H : G.subgraph) : Prop := H.coe.connected
+
 lemma preconnected.set_univ_walk_nonempty (hconn : G.preconnected) (u v : V) :
   (set.univ : set (G.walk u v)).nonempty :=
 by { rw ← set.nonempty_iff_univ_nonempty, exact hconn u v }