feat(Combinatorics/SimpleGraph/Matching): add IsCycles and IsAlternating with basic results (#19250)

add `SimpleGraph.IsCycles` and `SimpleGraph.IsAlternating` with some basic results involving matchings. These are defined on `SimpleGraph`, because we want to use the `symmDiff` defined on there.
This is in preparation for Tutte's theorem.



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

Author: pimotte

Mathlib/Combinatorics/SimpleGraph/Matching.lean

@@ -27,6 +27,14 @@ one edge, and the edges of the subgraph represent the paired vertices.
 * `SimpleGraph.Subgraph.IsPerfectMatching` defines when a subgraph `M` of a simple graph is a
   perfect matching, denoted `M.IsPerfectMatching`.
 
+* `SimpleGraph.IsMatchingFree` means that a graph `G` has no perfect matchings.
+
+* `SimpleGraph.IsCycles` means that a graph consists of cycles (including cycles of length 0,
+  also known as isolated vertices)
+
+* `SimpleGraph.IsAlternating` means that edges in a graph `G` are alternatingly
+  included and not included in some other graph `G'`
+
 ## TODO
 
 * Define an `other` function and prove useful results about it (https://leanprover.zulipchat.com/#narrow/stream/252551-graph-theory/topic/matchings/near/266205863)
@@ -309,4 +317,83 @@ lemma exists_maximal_isMatchingFree [Finite V] (h : G.IsMatchingFree) :
   obtain ⟨Gmax, hGmax⟩ := Finite.exists_le_maximal h
   exact ⟨Gmax, ⟨hGmax.1, ⟨hGmax.2.prop, fun _ h' ↦ hGmax.2.not_prop_of_gt h'⟩⟩⟩
 
+/-- A graph `G` consists of a set of cycles, if each vertex is either isolated or connected to
+exactly two vertices. This is used to create new matchings by taking the `symmDiff` with cycles.
+The definition of `symmDiff` that makes sense is the one for `SimpleGraph`. The `symmDiff`
+for `SimpleGraph.Subgraph` deriving from the lattice structure also affects the vertices included,
+which we do not want in this case. This is why this property is defined for `SimpleGraph`, rather
+than `SimpleGraph.Subgraph`.
+-/
+def IsCycles (G : SimpleGraph V) := ∀ ⦃v⦄, (G.neighborSet v).Nonempty → (G.neighborSet v).ncard = 2
+
+/--
+Given a vertex with one edge in a graph of cycles this gives the other edge incident
+to the same vertex.
+-/
+lemma IsCycles.other_adj_of_adj (h : G.IsCycles) (hadj : G.Adj v w) :
+    ∃ w', w ≠ w' ∧ G.Adj v w' := by
+  simp_rw [← SimpleGraph.mem_neighborSet] at hadj ⊢
+  cases' (G.neighborSet v).eq_empty_or_nonempty with hl hr
+  · exact ((Set.eq_empty_iff_forall_not_mem.mp hl) _ hadj).elim
+  · have := h hr
+    obtain ⟨w', hww'⟩ := (G.neighborSet v).exists_ne_of_one_lt_ncard (by omega) w
+    exact ⟨w', ⟨hww'.2.symm, hww'.1⟩⟩
+
+open scoped symmDiff
+
+lemma Subgraph.IsPerfectMatching.symmDiff_spanningCoe_IsCycles
+    {M : Subgraph G} {M' : Subgraph G'} (hM : M.IsPerfectMatching)
+    (hM' : M'.IsPerfectMatching) : (M.spanningCoe ∆ M'.spanningCoe).IsCycles := by
+  intro v
+  obtain ⟨w, hw⟩ := hM.1 (hM.2 v)
+  obtain ⟨w', hw'⟩ := hM'.1 (hM'.2 v)
+  simp only [symmDiff_def, Set.ncard_eq_two, ne_eq, imp_iff_not_or, Set.not_nonempty_iff_eq_empty,
+    Set.eq_empty_iff_forall_not_mem, SimpleGraph.mem_neighborSet, SimpleGraph.sup_adj, sdiff_adj,
+    spanningCoe_adj, not_or, not_and, not_not]
+  by_cases hww' : w = w'
+  · simp_all [← imp_iff_not_or, hww']
+  · right
+    use w, w'
+    aesop
+
+/--
+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
+possible. This property is used to create new matchings using `symmDiff`.
+The definition of `symmDiff` that makes sense is the one for `SimpleGraph`. The `symmDiff`
+for `SimpleGraph.Subgraph` deriving from the lattice structure also affects the vertices included,
+which we do not want in this case. This is why this property, just like `IsCycles`, is defined
+for `SimpleGraph` rather than `SimpleGraph.Subgraph`.
+-/
+def IsAlternating (G G' : SimpleGraph V) :=
+  ∀ ⦃v w w': V⦄, w ≠ w' → G.Adj v w → G.Adj v w' → (G'.Adj v w ↔ ¬ G'.Adj v w')
+
+lemma IsPerfectMatching.symmDiff_spanningCoe_of_isAlternating {M : Subgraph G}
+    (hM : M.IsPerfectMatching) (hG' : G'.IsAlternating M.spanningCoe) (hG'cyc : G'.IsCycles)  :
+    (SimpleGraph.toSubgraph (M.spanningCoe ∆ G')
+      (by rfl)).IsPerfectMatching := by
+  rw [Subgraph.isPerfectMatching_iff]
+  intro v
+  simp only [toSubgraph_adj, symmDiff_def, sup_adj, sdiff_adj, Subgraph.spanningCoe_adj]
+  obtain ⟨w, hw⟩ := hM.1 (hM.2 v)
+  by_cases h : G'.Adj v w
+  · obtain ⟨w', hw'⟩ := hG'cyc.other_adj_of_adj h
+    have hmadj :  M.Adj v w ↔ ¬M.Adj v w' := by simpa using hG' hw'.1 h hw'.2
+    use w'
+    simp only [hmadj.mp hw.1, hw'.2, not_true_eq_false, and_self, not_false_eq_true, or_true,
+      true_and]
+    rintro y (hl | hr)
+    · aesop
+    · obtain ⟨w'', hw''⟩ := hG'cyc.other_adj_of_adj hr.1
+      by_contra! hc
+      simp_all only [show M.Adj v y ↔ ¬M.Adj v w' from by simpa using hG' hc hr.1 hw'.2,
+        not_false_eq_true, ne_eq, iff_true, not_true_eq_false, and_false]
+  · use w
+    simp only [hw.1, h, not_false_eq_true, and_self, not_true_eq_false, or_false, true_and]
+    rintro y (hl | hr)
+    · exact hw.2 _ hl.1
+    · have ⟨w', hw'⟩ := hG'cyc.other_adj_of_adj hr.1
+      simp_all only [show M.Adj v y ↔ ¬M.Adj v w' from by simpa using hG' hw'.1 hr.1 hw'.2, not_not,
+        ne_eq, and_false]
+
 end SimpleGraph