feat(Combinatorics/SimpleGraph): Characterizing SimpleGraph.IsCycles (#20830)

Shows that IsCycles is appropriately named. The core result is `IsCycles.exists_cycle_toSubgraph_verts_eq_connectedComponent_supp`, which shows that for an edge in a nontrivial component a cycle can be constructed that has exactly the edges of the component.

In order to get this some API is included:

- Coercions of walks in graphs that are the result of coerced subgraphs
- NeighborSets of `toSubgraph` for paths
- Supporting results for `IsCycles`
- Some miscellaneous supporting lemma's

This is all in preparation for Tutte's theorem. 



Co-authored-by: Pim Otte <otte.pim@gmail.com>

Author: pimotte

Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean

@@ -103,6 +103,22 @@ protected lemma Connected.sup {H K : G.Subgraph}
   rintro ⟨v, (hv|hv)⟩
   · exact Reachable.map (Subgraph.inclusion (le_sup_left : H ≤ H ⊔ K)) (hH ⟨u, hu⟩ ⟨v, hv⟩)
   · exact Reachable.map (Subgraph.inclusion (le_sup_right : K ≤ H ⊔ K)) (hK ⟨u, hu'⟩ ⟨v, hv⟩)
+
+/--
+  This lemma establishes a condition under which a subgraph is the same as a connected component.
+  Note the asymmetry in the hypothesis `h`: `v` is in `H.verts`, but `w` is not required to be.
+-/
+lemma Connected.exists_verts_eq_connectedComponentSupp {H : Subgraph G}
+    (hc : H.Connected) (h : ∀ v ∈ H.verts, ∀ w, G.Adj v w → H.Adj v w) :
+    ∃ c : G.ConnectedComponent, H.verts = c.supp := by
+  rw [SimpleGraph.ConnectedComponent.exists]
+  obtain ⟨v, hv⟩ := hc.nonempty
+  use v
+  ext w
+  simp only [ConnectedComponent.mem_supp_iff, ConnectedComponent.eq]
+  exact ⟨fun hw ↦ by simpa using (hc ⟨w, hw⟩ ⟨v, hv⟩).map H.hom,
+    fun a ↦ a.symm.mem_subgraphVerts h hv⟩
+
 end Subgraph
 
 /-! ### Walks as subgraphs -/
@@ -240,6 +256,71 @@ theorem toSubgraph_adj_iff {u v u' v'} (w : G.Walk u v) :
     rw [← Subgraph.mem_edgeSet, ← hi.1, Subgraph.mem_edgeSet]
     exact toSubgraph_adj_getVert _ hi.2
 
+namespace IsPath
+
+lemma neighborSet_toSubgraph_startpoint {u v} {p : G.Walk u v}
+    (hp : p.IsPath) (hnp : ¬ p.Nil) : p.toSubgraph.neighborSet u = {p.snd} := by
+  have hadj1 := p.toSubgraph_adj_snd hnp
+  ext v
+  simp_all only [Subgraph.mem_neighborSet, Set.mem_insert_iff, Set.mem_singleton_iff,
+    SimpleGraph.Walk.toSubgraph_adj_iff, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk]
+  refine ⟨?_, by aesop⟩
+  rintro ⟨i, hl | hr⟩
+  · have : i = 0 := by
+      apply hp.getVert_injOn (by rw [Set.mem_setOf]; omega) (by rw [Set.mem_setOf]; omega)
+      aesop
+    aesop
+  · have : i + 1 = 0 := by
+      apply hp.getVert_injOn (by rw [Set.mem_setOf]; omega) (by rw [Set.mem_setOf]; omega)
+      aesop
+    contradiction
+
+lemma neighborSet_toSubgraph_endpoint {u v} {p : G.Walk u v}
+    (hp : p.IsPath) (hnp : ¬ p.Nil) : p.toSubgraph.neighborSet v = {p.penultimate} := by
+  simpa using IsPath.neighborSet_toSubgraph_startpoint hp.reverse
+      (by rw [Walk.not_nil_iff_lt_length, Walk.length_reverse]; exact
+        Walk.not_nil_iff_lt_length.mp hnp)
+
+lemma neighborSet_toSubgraph_internal {u} {i : ℕ} {p : G.Walk u v} (hp : p.IsPath)
+    (h : i ≠ 0) (h' : i < p.length) :
+    p.toSubgraph.neighborSet (p.getVert i) = {p.getVert (i - 1), p.getVert (i + 1)} := by
+  have hadj1 := ((show i - 1 + 1 = i from by omega) ▸
+    p.toSubgraph_adj_getVert (by omega : (i - 1) < p.length)).symm
+  ext v
+  simp_all only [ne_eq, Subgraph.mem_neighborSet, Set.mem_insert_iff, Set.mem_singleton_iff,
+    SimpleGraph.Walk.toSubgraph_adj_iff, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq,
+    Prod.swap_prod_mk]
+  refine ⟨?_, by aesop⟩
+  rintro ⟨i', ⟨hl, _⟩ | ⟨_, hl⟩⟩ <;>
+    apply hp.getVert_injOn (by rw [Set.mem_setOf_eq]; omega)
+      (by rw [Set.mem_setOf_eq]; omega) at hl <;> aesop
+
+lemma ncard_neighborSet_toSubgraph_internal_eq_two {u} {i : ℕ} {p : G.Walk u v} (hp : p.IsPath)
+    (h : i ≠ 0) (h' : i < p.length) :
+    (p.toSubgraph.neighborSet (p.getVert i)).ncard = 2 := by
+  rw [hp.neighborSet_toSubgraph_internal h h']
+  have : p.getVert (i - 1) ≠ p.getVert (i + 1) := by
+    intro h
+    have := hp.getVert_injOn (by rw [Set.mem_setOf_eq]; omega) (by rw [Set.mem_setOf_eq]; omega) h
+    omega
+  simp_all
+
+lemma snd_of_toSubgraph_adj {u v v'} {p : G.Walk u v} (hp : p.IsPath)
+    (hadj : p.toSubgraph.Adj u v') : p.snd = v' := by
+  have ⟨i, hi⟩ := p.toSubgraph_adj_iff.mp hadj
+  simp only [Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk] at hi
+  rcases hi.1 with ⟨hl1, rfl⟩|⟨hr1, hr2⟩
+  · have : i = 0 := by
+      apply hp.getVert_injOn (by rw [Set.mem_setOf]; omega) (by rw [Set.mem_setOf]; omega)
+      rw [p.getVert_zero, hl1]
+    simp [this]
+  · have : i + 1 = 0 := by
+      apply hp.getVert_injOn (by rw [Set.mem_setOf]; omega) (by rw [Set.mem_setOf]; omega)
+      rw [p.getVert_zero, hr2]
+    contradiction
+
+end IsPath
+
 namespace IsCycle
 
 lemma neighborSet_toSubgraph_endpoint {u} {p : G.Walk u u} (hpc : p.IsCycle) :
@@ -250,7 +331,7 @@ lemma neighborSet_toSubgraph_endpoint {u} {p : G.Walk u u} (hpc : p.IsCycle) :
   simp_all only [Subgraph.mem_neighborSet, Set.mem_insert_iff, Set.mem_singleton_iff,
     SimpleGraph.Walk.toSubgraph_adj_iff, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk]
   refine ⟨?_, by aesop⟩
-  rintro ⟨i, (hl | hr)⟩
+  rintro ⟨i, hl | hr⟩
   · rw [hpc.getVert_endpoint_iff (by omega)] at hl
     cases hl.1 <;> aesop
   · rcases (hpc.getVert_endpoint_iff (by omega)).mp hr.2 with h1 | h2
@@ -269,7 +350,7 @@ lemma neighborSet_toSubgraph_internal {u} {i : ℕ} {p : G.Walk u u} (hpc : p.Is
     SimpleGraph.Walk.toSubgraph_adj_iff, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq,
     Prod.swap_prod_mk]
   refine ⟨?_, by aesop⟩
-  rintro ⟨i', (⟨hl1, hl2⟩ | ⟨hr1, hr2⟩)⟩
+  rintro ⟨i', ⟨hl1, hl2⟩ | ⟨hr1, hr2⟩⟩
   · apply hpc.getVert_injOn' (by rw [Set.mem_setOf_eq]; omega)
       (by rw [Set.mem_setOf_eq]; omega) at hl1
     aesop

Mathlib/Combinatorics/SimpleGraph/Matching.lean

@@ -3,8 +3,9 @@ Copyright (c) 2020 Alena Gusakov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alena Gusakov, Arthur Paulino, Kyle Miller, Pim Otte
 -/
-import Mathlib.Combinatorics.SimpleGraph.DegreeSum
+import Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
 import Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting
+import Mathlib.Combinatorics.SimpleGraph.DegreeSum
 import Mathlib.Data.Fintype.Order
 import Mathlib.Data.Set.Functor
 
@@ -334,6 +335,16 @@ lemma IsCycles.other_adj_of_adj (h : G.IsCycles) (hadj : G.Adj v w) :
   obtain ⟨w', hww'⟩ := (G.neighborSet v).exists_ne_of_one_lt_ncard (by omega) w
   exact ⟨w', ⟨hww'.2.symm, hww'.1⟩⟩
 
+lemma IsCycles.existsUnique_ne_adj (h : G.IsCycles) (hadj : G.Adj v w) :
+    ∃! w', w ≠ w' ∧ G.Adj v w' := by
+  obtain ⟨w', ⟨hww, hww'⟩⟩ := h.other_adj_of_adj hadj
+  use w'
+  refine ⟨⟨hww, hww'⟩, ?_⟩
+  intro y ⟨hwy, hwy'⟩
+  obtain ⟨x, y', hxy'⟩ := Set.ncard_eq_two.mp (h ⟨w, hadj⟩)
+  simp_rw [← SimpleGraph.mem_neighborSet] at *
+  aesop
+
 lemma IsCycles.induce_supp (c : G.ConnectedComponent) (h : G.IsCycles) :
     (G.induce c.supp).spanningCoe.IsCycles := by
   intro v ⟨w, hw⟩
@@ -360,6 +371,110 @@ lemma Subgraph.IsPerfectMatching.symmDiff_isCycles
     use w, w'
     aesop
 
+lemma IsCycles.snd_of_mem_support_of_isPath_of_adj [Finite V] {v w w' : V}
+    (hcyc : G.IsCycles) (p : G.Walk v w) (hw : w ≠ w') (hw' : w' ∈ p.support) (hp : p.IsPath)
+    (hadj : G.Adj v w') : p.snd = w' := by
+  classical
+  apply hp.snd_of_toSubgraph_adj
+  rw [Walk.mem_support_iff_exists_getVert] at hw'
+  obtain ⟨n, ⟨rfl, hnl⟩⟩ := hw'
+  by_cases hn : n = 0 ∨ n = p.length
+  · aesop
+  have e : G.neighborSet (p.getVert n) ≃ p.toSubgraph.neighborSet (p.getVert n) := by
+    refine @Classical.ofNonempty _ ?_
+    rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
+        hp.ncard_neighborSet_toSubgraph_internal_eq_two (by omega) (by omega),
+        hcyc (Set.nonempty_of_mem hadj.symm)]
+  rw [Subgraph.adj_comm, Subgraph.adj_iff_of_neighborSet_equiv e (Set.toFinite _).fintype]
+  exact hadj.symm
+
+private lemma IsCycles.reachable_sdiff_toSubgraph_spanningCoe_aux [Fintype V] {v w : V}
+    (hcyc : G.IsCycles) (p : G.Walk v w) (hp : p.IsPath) :
+    (G \ p.toSubgraph.spanningCoe).Reachable w v := by
+  classical
+  -- Consider the case when p is nil
+  by_cases hvw : v = w
+  · subst hvw
+    use .nil
+  have hpn : ¬p.Nil := Walk.not_nil_of_ne hvw
+  obtain ⟨w', ⟨hw'1, hw'2⟩, hwu⟩ := hcyc.existsUnique_ne_adj
+    (p.toSubgraph_adj_snd hpn).adj_sub
+  -- The edge (v, w) can't be in p, because then it would be the second node
+  have hnpvw' : ¬ p.toSubgraph.Adj v w' := by
+    intro h
+    exact hw'1 (hp.snd_of_toSubgraph_adj h)
+  -- If w = w', then then the reachability can be proved with just one edge
+  by_cases hww' : w = w'
+  · subst hww'
+    have : (G \  p.toSubgraph.spanningCoe).Adj w v := by
+      simp only [sdiff_adj, Subgraph.spanningCoe_adj]
+      exact ⟨hw'2.symm, fun h ↦ hnpvw' h.symm⟩
+    exact this.reachable
+  -- Construct the walk needed recursively by extending p
+  have hle : (G \ (p.cons hw'2.symm).toSubgraph.spanningCoe) ≤ (G \ p.toSubgraph.spanningCoe) := by
+    apply sdiff_le_sdiff (by rfl) ?hcd
+    aesop
+  have hp'p : (p.cons hw'2.symm).IsPath := by
+    rw [Walk.cons_isPath_iff]
+    refine ⟨hp, fun hw' ↦ ?_⟩
+    exact hw'1 (hcyc.snd_of_mem_support_of_isPath_of_adj _ hww' hw' hp hw'2)
+  have : (G \ p.toSubgraph.spanningCoe).Adj w' v := by
+    simp only [sdiff_adj, Subgraph.spanningCoe_adj]
+    refine ⟨hw'2.symm, fun h ↦ ?_⟩
+    exact hnpvw' h.symm
+  use (((hcyc.reachable_sdiff_toSubgraph_spanningCoe_aux
+    (p.cons hw'2.symm) hp'p).some).mapLe hle).append this.toWalk
+termination_by Fintype.card V + 1 - p.length
+decreasing_by
+  simp_wf
+  have := Walk.IsPath.length_lt hp
+  omega
+
+lemma IsCycles.reachable_sdiff_toSubgraph_spanningCoe [Finite V] {v w : V} (hcyc : G.IsCycles)
+    (p : G.Walk v w) (hp : p.IsPath) : (G \ p.toSubgraph.spanningCoe).Reachable w v := by
+  have : Fintype V := Fintype.ofFinite V
+  exact reachable_sdiff_toSubgraph_spanningCoe_aux hcyc p hp
+
+lemma IsCycles.reachable_deleteEdges [Finite V] (hadj : G.Adj v w)
+    (hcyc : G.IsCycles) : (G.deleteEdges {s(v, w)}).Reachable v w := by
+  have : fromEdgeSet {s(v, w)} = hadj.toWalk.toSubgraph.spanningCoe := by
+    simp only [Walk.toSubgraph, singletonSubgraph_le_iff, subgraphOfAdj_verts, Set.mem_insert_iff,
+      Set.mem_singleton_iff, or_true, sup_of_le_left]
+    exact (Subgraph.spanningCoe_subgraphOfAdj hadj).symm
+  rw [show G.deleteEdges {s(v, w)} = G \ fromEdgeSet {s(v, w)} from by rfl]
+  exact this ▸ (hcyc.reachable_sdiff_toSubgraph_spanningCoe hadj.toWalk
+    (Walk.IsPath.of_adj hadj)).symm
+
+lemma IsCycles.exists_cycle_toSubgraph_verts_eq_connectedComponentSupp [Finite V]
+    {c : G.ConnectedComponent} (h : G.IsCycles) (hv : v ∈ c.supp)
+    (hn : (G.neighborSet v).Nonempty) :
+    ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp := by
+  classical
+  obtain ⟨w, hw⟩ := hn
+  obtain ⟨u, p, hp⟩ := SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle.mp
+    ⟨hw, h.reachable_deleteEdges hw⟩
+  have hvp : v ∈ p.support := SimpleGraph.Walk.fst_mem_support_of_mem_edges _ hp.2
+  have : p.toSubgraph.verts = c.supp := by
+    obtain ⟨c', hc'⟩ := p.toSubgraph_connected.exists_verts_eq_connectedComponentSupp (by
+      intro v hv w hadj
+      refine (Subgraph.adj_iff_of_neighborSet_equiv ?_ (Set.toFinite _).fintype).mpr hadj
+      have : (G.neighborSet v).Nonempty := by
+        rw [Walk.mem_verts_toSubgraph] at hv
+        refine (Set.nonempty_of_ncard_ne_zero ?_).mono (p.toSubgraph.neighborSet_subset v)
+        rw [hp.1.ncard_neighborSet_toSubgraph_eq_two hv]
+        omega
+      refine @Classical.ofNonempty _ ?_
+      rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
+        h this, hp.1.ncard_neighborSet_toSubgraph_eq_two (p.mem_verts_toSubgraph.mp hv)])
+    rw [hc']
+    have : v ∈ c'.supp := by
+      rw [← hc', Walk.mem_verts_toSubgraph]
+      exact hvp
+    simp_all
+  use p.rotate hvp
+  rw [← this]
+  exact ⟨hp.1.rotate _, by simp_all⟩
+
 /--
 A graph `G` is alternating with respect to some other graph `G'`, if exactly every other edge in
 `G` is in `G'`. Note that the degree of each vertex needs to be at most 2 for this to be

Mathlib/Combinatorics/SimpleGraph/Path.lean

@@ -227,6 +227,9 @@ theorem IsPath.of_append_right {u v w : V} {p : G.Walk u v} {q : G.Walk v w}
   rw [reverse_append] at h
   apply h.of_append_left
 
+lemma IsPath.of_adj {G : SimpleGraph V} {u v : V} (h : G.Adj u v) : h.toWalk.IsPath := by
+  aesop
+
 @[simp]
 theorem IsCycle.not_of_nil {u : V} : ¬(nil : G.Walk u u).IsCycle := fun h => h.ne_nil rfl
 
@@ -799,6 +802,21 @@ theorem Iso.symm_apply_reachable {G : SimpleGraph V} {G' : SimpleGraph V'} {φ :
     {v : V'} : G.Reachable (φ.symm v) u ↔ G'.Reachable v (φ u) := by
   rw [← Iso.reachable_iff, RelIso.apply_symm_apply]
 
+lemma Reachable.mem_subgraphVerts {u v} {H : G.Subgraph} (hr : G.Reachable u v)
+    (h : ∀ v ∈ H.verts, ∀ w, G.Adj v w → H.Adj v w)
+    (hu : u ∈ H.verts) : v ∈ H.verts := by
+  let rec aux {v' : V} (hv' : v' ∈ H.verts) (p : G.Walk v' v) : v ∈ H.verts := by
+    by_cases hnp : p.Nil
+    · exact hnp.eq ▸ hv'
+    exact aux (H.edge_vert (h _ hv' _ (Walk.adj_snd hnp)).symm) p.tail
+  termination_by p.length
+  decreasing_by {
+    simp_wf
+    rw [← Walk.length_tail_add_one hnp]
+    omega
+  }
+  exact aux hu hr.some
+
 variable (G)
 
 theorem reachable_is_equivalence : Equivalence G.Reachable :=
@@ -1179,8 +1197,8 @@ def IsBridge (G : SimpleGraph V) (e : Sym2 V) : Prop :=
 theorem isBridge_iff {u v : V} :
     G.IsBridge s(u, v) ↔ G.Adj u v ∧ ¬(G \ fromEdgeSet {s(u, v)}).Reachable u v := Iff.rfl
 
-theorem reachable_delete_edges_iff_exists_walk {v w : V} :
-    (G \ fromEdgeSet {s(v, w)}).Reachable v w ↔ ∃ p : G.Walk v w, ¬s(v, w) ∈ p.edges := by
+theorem reachable_delete_edges_iff_exists_walk {v w v' w': V} :
+    (G \ fromEdgeSet {s(v, w)}).Reachable v' w' ↔ ∃ p : G.Walk v' w', ¬s(v, w) ∈ p.edges := by
   constructor
   · rintro ⟨p⟩
     use p.map (Hom.mapSpanningSubgraphs (by simp))

Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

@@ -174,6 +174,12 @@ theorem spanningCoe_inj : G₁.spanningCoe = G₂.spanningCoe ↔ G₁.Adj = G
 lemma mem_of_adj_spanningCoe {v w : V} {s : Set V} (G : SimpleGraph s)
     (hadj : G.spanningCoe.Adj v w) : v ∈ s := by aesop
 
+@[simp]
+lemma spanningCoe_subgraphOfAdj {v w : V} (hadj : G.Adj v w) :
+    (G.subgraphOfAdj hadj).spanningCoe = fromEdgeSet {s(v, w)} := by
+  ext v w
+  aesop
+
 /-- `spanningCoe` is equivalent to `coe` for a subgraph that `IsSpanning`. -/
 @[simps]
 def spanningCoeEquivCoeOfSpanning (G' : Subgraph G) (h : G'.IsSpanning) :
@@ -566,6 +572,10 @@ theorem _root_.SimpleGraph.toSubgraph.isSpanning (H : SimpleGraph V) (h : H ≤
 theorem spanningCoe_le_of_le {H H' : Subgraph G} (h : H ≤ H') : H.spanningCoe ≤ H'.spanningCoe :=
   h.2
 
+@[simp]
+lemma sup_spanningCoe (H H' : Subgraph G) :
+    (H ⊔ H').spanningCoe = H.spanningCoe ⊔ H'.spanningCoe := rfl
+
 /-- The top of the `Subgraph G` lattice is equivalent to the graph itself. -/
 def topEquiv : (⊤ : Subgraph G).coe ≃g G where
   toFun v := ↑v
@@ -764,6 +774,22 @@ theorem degree_eq_one_iff_unique_adj {G' : Subgraph G} {v : V} [Fintype (G'.neig
   rw [← finset_card_neighborSet_eq_degree, Finset.card_eq_one, Finset.singleton_iff_unique_mem]
   simp only [Set.mem_toFinset, mem_neighborSet]
 
+lemma adj_iff_of_neighborSet_equiv {v : V} {H : Subgraph G}
+    (h : G.neighborSet v ≃ H.neighborSet v) (hfin : Fintype (G.neighborSet v)) :
+    ∀ {w}, H.Adj v w ↔ G.Adj v w := by
+  classical
+  intro w
+  refine ⟨fun a => a.adj_sub, ?_⟩
+  have : Fintype (H.neighborSet v) := (h.set_finite_iff.mp hfin.finite).fintype
+  let f : H.neighborSet v → G.neighborSet v := fun a => ⟨a, a.coe_prop.adj_sub⟩
+  have hfinj : f.Injective := fun w w' hww' ↦ by aesop
+  have hfbij : f.Bijective := ⟨hfinj, hfinj.surjective_of_fintype h.symm⟩
+  intro h
+  have hv := (Fintype.bijInv hfbij ⟨w, h⟩).coe_prop
+  obtain ⟨v', hv'⟩ : ∃ v', f v' = ⟨w, h⟩ := hfbij.surjective ⟨w, h⟩
+  have : (f v') = w := by simpa using congrArg Subtype.val hv'
+  aesop
+
 end Subgraph
 
 section MkProperties

Mathlib/Combinatorics/SimpleGraph/Walk.lean

@@ -890,6 +890,14 @@ lemma adj_penultimate {p : G.Walk v w} (hp : ¬ p.Nil) :
   rw [nil_iff_length_eq] at hp
   convert adj_getVert_succ _ _ <;> omega
 
+@[simp]
+lemma snd_reverse (p : G.Walk u v) : p.reverse.snd = p.penultimate := by
+  simpa using getVert_reverse p 1
+
+@[simp]
+lemma penultimate_reverse (p : G.Walk u v) : p.reverse.penultimate = p.snd := by
+  cases p <;> simp [snd, penultimate, getVert_append]
+
 /-- The walk obtained by removing the first dart of a walk. A nil walk stays nil. -/
 def tail (p : G.Walk u v) : G.Walk (p.snd) v := p.drop 1