[Merged by Bors] - feat(Combinatorics/SimpleGraph): part of Tutte's theorem

Mathlib.lean

@@ -2490,6 +2490,7 @@ import Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
 import Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
 import Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
 import Mathlib.Combinatorics.SimpleGraph.Turan
+import Mathlib.Combinatorics.SimpleGraph.Tutte
 import Mathlib.Combinatorics.SimpleGraph.UniversalVerts
 import Mathlib.Combinatorics.SimpleGraph.Walk
 import Mathlib.Combinatorics.Young.SemistandardTableau

Mathlib/Combinatorics/SimpleGraph/Connectivity/Represents.lean

@@ -14,6 +14,7 @@ import Mathlib.Data.Set.Card
 
 * `SimpleGraph.ConnectedComponent.Represents` says that a set of vertices represents a set of
   components if it contains exactly one vertex from each component.
+* `SimpleGraph.oddComponents` is the set of connected components of odd cardinality.
 -/
 
 universe u
@@ -60,6 +61,9 @@ lemma ncard_inter (hrep : Represents s C) (h : c ∈ C) : (s ∩ c.supp).ncard =
   rw [Set.ncard_eq_one]
   exact exists_inter_eq_singleton hrep h
 
+lemma ncard_eq (hrep : Represents s C) : s.ncard = C.ncard :=
+  hrep.image_eq.symm ▸ (Set.ncard_image_of_injOn hrep.injOn).symm
+
 lemma ncard_sdiff_of_mem (hrep : Represents s C) (h : c ∈ C) :
     (c.supp \ s).ncard = c.supp.ncard - 1 := by
   obtain ⟨a, ha⟩ := exists_inter_eq_singleton hrep h
@@ -70,4 +74,20 @@ lemma ncard_sdiff_of_not_mem (hrep : Represents s C) (h : c ∉ C) :
     (c.supp \ s).ncard = c.supp.ncard := by
   rw [(disjoint_supp_of_not_mem hrep h).sdiff_eq_right]
 
-end SimpleGraph.ConnectedComponent.Represents
+end ConnectedComponent.Represents
+
+/-- The odd components are the connected components of odd cardinality. This definition excludes
+infinite components. -/
+def oddComponents : Set G.ConnectedComponent := {c : G.ConnectedComponent | Odd c.supp.ncard}
+
+lemma ConnectedComponent.even_ncard_supp_sdiff_rep {s : Set V} (K : G.ConnectedComponent)
+    (hrep : ConnectedComponent.Represents s G.oddComponents) :
+  Even (K.supp \ s).ncard := by
+  by_cases h : Even K.supp.ncard
+  · simpa [hrep.ncard_sdiff_of_not_mem
+      (by simpa [Set.ncard_image_of_injective, ← Nat.not_odd_iff_even] using h)] using h
+  · have : K.supp.ncard ≠ 0 := Nat.ne_of_odd_add (Nat.not_even_iff_odd.mp h)
+    rw [hrep.ncard_sdiff_of_mem (Nat.not_even_iff_odd.mp h), Nat.even_sub (by omega)]
+    simpa [Nat.even_sub] using Nat.not_even_iff_odd.mp h
+
+end SimpleGraph

Mathlib/Combinatorics/SimpleGraph/Matching.lean

@@ -3,13 +3,16 @@ 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.Clique
 import Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
 import Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting
 import Mathlib.Combinatorics.SimpleGraph.DegreeSum
 import Mathlib.Combinatorics.SimpleGraph.Operations
 import Mathlib.Data.Fintype.Order
+import Mathlib.Data.Set.Card.Arithmetic
 import Mathlib.Data.Set.Functor
 
+
 /-!
 # Matchings
 
@@ -260,6 +263,20 @@ lemma IsPerfectMatching.toSubgraph_iff (h : M.spanningCoe ≤ G') :
 
 end Subgraph
 
+lemma IsClique.even_iff_exists_isMatching {u : Set V} (hc : G.IsClique u)
+    (hu : Set.Finite u) : Even u.ncard ↔ ∃ (M : Subgraph G), M.verts = u ∧ M.IsMatching := by
+  refine ⟨fun h ↦ ?_, by
+    rintro ⟨M, ⟨rfl, hMr⟩⟩
+    simpa [Set.ncard_eq_toFinset_card _ hu, Set.toFinite_toFinset,
+      ← Set.toFinset_card] using @hMr.even_card _ _ _ hu.fintype⟩
+  obtain ⟨t, u, rfl, hd, hcard⟩ := Set.exists_union_disjoint_ncard_eq_of_even h
+  obtain ⟨f⟩ : Nonempty (t ≃ u) := by
+    rw [← Cardinal.eq, ← t.cast_ncard (Set.finite_union.mp hu).1,
+      ← u.cast_ncard (Set.finite_union.mp hu).2]
+    exact congrArg Nat.cast hcard
+  exact Subgraph.IsMatching.exists_of_disjoint_sets_of_equiv hd f
+    (fun v ↦ hc (by simp) (by simp) <| hd.ne_of_mem (by simp) (by simp))
+
 namespace ConnectedComponent
 
 section Finite

Mathlib/Combinatorics/SimpleGraph/Tutte.lean

@@ -0,0 +1,121 @@
+/-
+Copyright (c) 2024 Pim Otte. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Pim Otte
+-/
+
+import Mathlib.Combinatorics.SimpleGraph.Matching
+import Mathlib.Combinatorics.SimpleGraph.Operations
+import Mathlib.Combinatorics.SimpleGraph.UniversalVerts
+import Mathlib.Data.Fintype.Card
+
+/-!
+# Tutte's theorem (work in progress)
+
+## Main definitions
+* `SimpleGraph.TutteViolator G u` is a set of vertices `u` which certifies non-existance of a
+  perfect matching.
+-/
+namespace SimpleGraph
+
+universe u
+variable {V : Type u} {G G' : SimpleGraph V} {u x v' w : V} [Fintype V]
+
+/-- A set certifying non-existance of a perfect matching -/
+def TutteViolator (G: SimpleGraph V) (u : Set V) : Prop :=
+  u.ncard < {c : ((⊤ : G.Subgraph).deleteVerts u).coe.ConnectedComponent | Odd (c.supp.ncard)}.ncard
+
+/-- This lemma states that a graph in which the universal vertices do not violate the
+Tutte-condition, if the graph decomposes into cliques, there exists a matching that covers
+everything except some universal vertices. It is marked private, because
+it is strictly weaker than `IsPerfectMatching.exists_of_isClique_supp` -/
+private lemma Subgraph.IsMatching.exists_verts_compl_subset_universalVerts
+    (h : ¬TutteViolator G G.universalVerts)
+    (h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent),
+    G.deleteUniversalVerts.coe.IsClique K.supp) :
+    ∃ M : Subgraph G, M.IsMatching ∧ M.vertsᶜ ⊆ G.universalVerts := by
+  classical
+  have hrep := ConnectedComponent.Represents.image_out
+      G.deleteUniversalVerts.coe.oddComponents
+  -- First we match one node from each odd component to a universal vertex
+  obtain ⟨t, ht, M1, hM1⟩ := Subgraph.IsMatching.exists_of_universalVerts
+      (disjoint_image_val_universalVerts _).symm (by
+        simp only [TutteViolator, not_lt] at h
+        rwa [Set.ncard_image_of_injective _ Subtype.val_injective, hrep.ncard_eq])
+  -- Then we match all other nodes in components internally
+  have compMatching (K : G.deleteUniversalVerts.coe.ConnectedComponent) :
+      ∃ M : Subgraph G, M.verts = Subtype.val '' K.supp \ M1.verts ∧ M.IsMatching := by
+    have : G.IsClique (Subtype.val '' K.supp \ M1.verts) :=
+      ((h' K).of_induce).subset Set.diff_subset
+    rw [← this.even_iff_exists_isMatching (Set.toFinite _), hM1.1]
+    exact even_ncard_image_val_supp_sdiff_image_val_rep_union _ ht hrep
+  let M2 : Subgraph G := ⨆ (K : G.deleteUniversalVerts.coe.ConnectedComponent),
+    (compMatching K).choose
+  have hM2 : M2.IsMatching := by
+    apply Subgraph.IsMatching.iSup (fun c ↦ (compMatching c).choose_spec.2) (fun i j hij ↦ ?_)
+    rw [(compMatching i).choose_spec.2.support_eq_verts,
+        (compMatching j).choose_spec.2.support_eq_verts,
+        (compMatching i).choose_spec.1, (compMatching j).choose_spec.1]
+    exact Set.disjoint_of_subset Set.diff_subset Set.diff_subset <|
+      Set.disjoint_image_of_injective Subtype.val_injective <|
+        SimpleGraph.pairwise_disjoint_supp_connectedComponent _ hij
+  have disjointM12 : Disjoint M1.support M2.support := by
+    rw [hM1.2.support_eq_verts, hM2.support_eq_verts, Subgraph.verts_iSup,
+      Set.disjoint_iUnion_right]
+    exact fun K ↦ (compMatching K).choose_spec.1.symm ▸ Set.disjoint_sdiff_right
+  -- The only vertices left are indeed contained in universalVerts
+  have : (M1.verts ∪ M2.verts)ᶜ ⊆ G.universalVerts := by
+    rw [Set.compl_subset_comm, Set.compl_eq_univ_diff]
+    intro v hv
+    by_cases h : v ∈ M1.verts
+    · exact M1.verts.mem_union_left _ h
+    right
+    simp only [deleteUniversalVerts_verts, Subgraph.verts_iSup, Set.mem_iUnion, M2,
+      (compMatching _).choose_spec.1]
+    use (G.deleteUniversalVerts.coe.connectedComponentMk ⟨v, hv⟩)
+    aesop
+  exact ⟨M1 ⊔ M2, hM1.2.sup hM2 disjointM12, this⟩
+
+/-- This lemma states that a graph in which the universal vertices do not violate the
+Tutte-condition, if the graph decomposes into cliques, it has a perfect matching -/
+theorem Subgraph.IsPerfectMatching.exists_of_isClique_supp
+    (hveven : Even (Fintype.card V)) (h : ¬G.TutteViolator G.universalVerts)
+    (h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent),
+    G.deleteUniversalVerts.coe.IsClique K.supp) : ∃ (M : Subgraph G), M.IsPerfectMatching := by
+  classical
+  obtain ⟨M, ⟨hM, hsub⟩⟩ := IsMatching.exists_verts_compl_subset_universalVerts h h'
+  obtain ⟨M', hM'⟩ := ((G.isClique_universalVerts.subset hsub).even_iff_exists_isMatching
+    (Set.toFinite _)).mp (by simpa [Set.even_ncard_compl_iff hveven, -Set.toFinset_card,
+      ← Set.ncard_eq_toFinset_card'] using hM.even_card)
+  use M ⊔ M'
+  have hspan : (M ⊔ M').IsSpanning := by
+    rw [Subgraph.isSpanning_iff, Subgraph.verts_sup, hM'.1]
+    exact M.verts.union_compl_self
+  exact ⟨hM.sup hM'.2 (by
+    simp only [hM.support_eq_verts, hM'.2.support_eq_verts, hM'.1, Subgraph.verts_sup]
+    exact (Set.disjoint_compl_left_iff_subset.mpr fun ⦃a⦄ a ↦ a).symm), hspan⟩
+
+theorem tutteViolator_empty (hodd : Odd (Fintype.card V)) : G.TutteViolator ∅ := by
+  classical
+  have ⟨c, hc⟩ := Classical.inhabited_of_nonempty
+    (Finite.card_pos_iff.mp <| Odd.pos <|
+    (odd_card_iff_odd_components ((⊤ : Subgraph G).deleteVerts ∅).coe).mp (by
+    simpa [Fintype.card_congr (Equiv.Set.univ V)] using hodd))
+  rw [TutteViolator, Set.ncard_empty, Set.ncard_pos]
+  use c
+
+/-- Proves the necessity part of Tutte's theorem -/
+lemma not_tutteViolator {M : Subgraph G} (hM : M.IsPerfectMatching) (u : Set V) :
+    ¬G.TutteViolator u := by
+  simpa [TutteViolator, Set.Nat.card_coe_set_eq] using Finite.card_le_of_injective
+      (fun c => ⟨(c.1.odd_matches_node_outside hM c.2).choose,
+        (c.1.odd_matches_node_outside hM c.2).choose_spec.1⟩) (by
+    intro x y hxy
+    obtain ⟨v, hv⟩ := (x.1.odd_matches_node_outside hM x.2).choose_spec.2
+    obtain ⟨w, hw⟩ := (y.1.odd_matches_node_outside hM y.2).choose_spec.2
+    obtain ⟨v', hv'⟩ := (M.isPerfectMatching_iff).mp hM _
+    rw [Subtype.mk_eq_mk.mp hxy,
+      (Subtype.val_injective (hv'.2 _ hw.1.symm ▸ hv'.2 _ hv.1.symm) : v = w)] at hv
+    exact Subtype.mk_eq_mk.mpr <| ConnectedComponent.eq_of_common_vertex hv.2 hw.2)
+
+end SimpleGraph

Mathlib/Combinatorics/SimpleGraph/UniversalVerts.lean

@@ -5,6 +5,7 @@ Authors: Pim Otte
 -/
 import Mathlib.Combinatorics.SimpleGraph.Clique
 import Mathlib.Combinatorics.SimpleGraph.Matching
+import Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
 
 /-!
 # Universal Vertices
@@ -51,4 +52,25 @@ lemma Subgraph.IsMatching.exists_of_universalVerts [Finite V] {s : Set V}
   have hadj (v : s) : G.Adj v (f v) := ht.1 (f v).2 (hd.ne_of_mem (f v).2 v.2)
   exact Subgraph.IsMatching.exists_of_disjoint_sets_of_equiv hd.symm f hadj
 
+lemma disjoint_image_val_universalVerts (s : Set G.deleteUniversalVerts.verts) :
+    Disjoint (Subtype.val '' s) G.universalVerts := by
+  simpa [deleteUniversalVerts, Subgraph.deleteVerts_verts, ← Set.disjoint_compl_right_iff_subset,
+    Set.compl_eq_univ_diff] using Subtype.coe_image_subset _ s
+
+/-- In this lemma we consider components after deleting universal vertices. If we take
+one such component and remove both a set of representatives of odd components and a subset
+of universal vertices, then an even number of vertices remain. -/
+lemma even_ncard_image_val_supp_sdiff_image_val_rep_union {t : Set V}
+    {s : Set G.deleteUniversalVerts.verts} (K : G.deleteUniversalVerts.coe.ConnectedComponent)
+    (h : t ⊆ G.universalVerts)
+    (hrep : ConnectedComponent.Represents s G.deleteUniversalVerts.coe.oddComponents) :
+    Even (Subtype.val '' K.supp \ (Subtype.val '' s ∪ t)).ncard := by
+  simp only [← Set.diff_inter_diff, ← Set.image_diff Subtype.val_injective,
+    sdiff_eq_left.mpr <| Set.disjoint_of_subset_right h (disjoint_image_val_universalVerts _),
+    Set.inter_diff_distrib_right, Set.inter_self, Set.diff_inter_self_eq_diff,
+    ← Set.image_inter Subtype.val_injective, Set.ncard_image_of_injective _ Subtype.val_injective,
+    K.even_ncard_supp_sdiff_rep hrep]
+
+
+
 end SimpleGraph

Mathlib/Data/Set/Card.lean

@@ -902,6 +902,16 @@ theorem eq_univ_iff_ncard [Finite α] (s : Set α) :
     s = univ ↔ ncard s = Nat.card α := by
   rw [← compl_empty_iff, ← ncard_eq_zero, ← ncard_add_ncard_compl s, self_eq_add_right]
 
+lemma even_ncard_compl_iff [Fintype α] (heven : Even (Fintype.card α)) (s : Set α) :
+  Even sᶜ.ncard ↔ Even s.ncard := by
+  simp [compl_eq_univ_diff, ncard_diff (subset_univ _ : s ⊆ Set.univ),
+    Nat.even_sub (ncard_le_ncard (subset_univ _ : s ⊆ Set.univ)),
+    (ncard_univ _).symm ▸ (Fintype.card_eq_nat_card ▸ heven)]
+
+lemma odd_ncard_compl_iff [Fintype α] (heven : Even (Fintype.card α)) (s : Set α) :
+  Odd sᶜ.ncard ↔ Odd s.ncard := by
+  rw [← Nat.not_even_iff_odd, even_ncard_compl_iff heven, Nat.not_even_iff_odd]
+
 end Lattice
 
 /-- Given a subset `s` of a set `t`, of sizes at most and at least `n` respectively, there exists a