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

Mathlib.lean

@@ -2588,6 +2588,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

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Pim Otte
 -/
 
-import Mathlib.Combinatorics.SimpleGraph.Path
+import Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting
 import Mathlib.Data.Set.Card
 
 /-!
@@ -60,6 +60,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 ▸ (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 +73,16 @@ 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
+
+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,11 +3,13 @@ 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
 
 /-!
@@ -53,7 +55,7 @@ assert_not_exists Field TwoSidedIdeal
 open Function
 
 namespace SimpleGraph
-variable {V W : Type*} {G G' : SimpleGraph V} {M M' : Subgraph G} {v w : V}
+variable {V W : Type*} {G G' : SimpleGraph V} {M M' : Subgraph G} {u v w : V}
 
 namespace Subgraph
 
@@ -90,15 +92,17 @@ lemma IsMatching.map_ofLE (h : M.IsMatching) (hGG' : G ≤ G') :
   use w
   simpa using hv' ▸ hw
 
-lemma IsMatching.not_adj_left_of_ne {M : Subgraph G} {u v w : V} (hM : M.IsMatching) (huv : v ≠ w)
-    (hadj : M.Adj u v) : ¬M.Adj u w := by
-  intro hadj'
-  obtain ⟨x, hx⟩ := hM (M.edge_vert hadj)
-  exact huv (hx.2 _ hadj ▸ (hx.2 _ hadj').symm)
+lemma IsMatching.eq_of_adj_left (hM : M.IsMatching) (huv : M.Adj u v) (huw : M.Adj u w) : v = w :=
+  (hM <| M.edge_vert huv).unique huv huw
 
-lemma IsMatching.not_adj_right_of_ne {M : Subgraph G} {u v w : V} (hM : M.IsMatching) (huw : u ≠ w)
-    (hadj : M.Adj u v) : ¬M.Adj w v  :=
-  fun hadj' ↦ hM.not_adj_left_of_ne huw hadj.symm hadj'.symm
+lemma IsMatching.eq_of_adj_right (hM : M.IsMatching) (huw : M.Adj u w) (hvw : M.Adj v w) : u = v :=
+  hM.eq_of_adj_left huw.symm hvw.symm
+
+lemma IsMatching.not_adj_left_of_ne (hM : M.IsMatching) (hvw : v ≠ w) (huv : M.Adj u v) :
+    ¬M.Adj u w := fun huw ↦ hvw <| hM.eq_of_adj_left huv huw
+
+lemma IsMatching.not_adj_right_of_ne (hM : M.IsMatching) (huv : u ≠ v) (huw : M.Adj u w) :
+    ¬M.Adj v w := fun hvw ↦ huv <| hM.eq_of_adj_right huw hvw
 
 lemma IsMatching.sup (hM : M.IsMatching) (hM' : M'.IsMatching)
     (hd : Disjoint M.support M'.support) : (M ⊔ M').IsMatching := by
@@ -260,6 +264,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 : u.Finite) : 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,120 @@
+/-
+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-existence 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-existence of a perfect matching. -/
+def IsTutteViolator (G : SimpleGraph V) (u : Set V) : Prop :=
+  u.ncard < ((⊤ : G.Subgraph).deleteVerts u).coe.oddComponents.ncard
+
+/-- Given a graph in which the universal vertices do not violate Tutte's condition,
+if the graph decomposes into cliques, there exists a matching that covers
+everything except some universal vertices.
+
+This lemma is marked private, because
+it is strictly weaker than `IsPerfectMatching.exists_of_isClique_supp` -/
+private lemma Subgraph.IsMatching.exists_verts_compl_subset_universalVerts
+    (h : ¬IsTutteViolator 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 [IsTutteViolator, 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⟩
+
+/-- Given a graph in which the universal vertices do not violate Tutte's 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.IsTutteViolator 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 IsTutteViolator.empty (hodd : Odd (Fintype.card V)) : G.IsTutteViolator ∅ := by
+  have c :=
+    Finite.card_pos_iff.mp
+    ((odd_ncard_oddComponents ((⊤ : Subgraph G).deleteVerts ∅).coe).mpr (by
+    simpa [Fintype.card_congr (Equiv.Set.univ V)] using hodd)).pos
+  rw [IsTutteViolator, Set.ncard_empty, Set.ncard_pos]
+  exact Set.Nonempty.of_subtype
+
+/-- Proves the necessity part of Tutte's theorem -/
+lemma not_isTutteViolator_of_isPerfectMatching {M : Subgraph G} (hM : M.IsPerfectMatching)
+    (u : Set V) :
+    ¬G.IsTutteViolator u := by
+  choose f hf g hgf hg using ConnectedComponent.odd_matches_node_outside hM (u := u)
+  have hfinj : f.Injective := fun c d hcd ↦ by
+    replace hcd : g c = g d := Subtype.val_injective <| hM.1.eq_of_adj_right (hgf c) (hcd ▸ hgf d)
+    exact Subtype.val_injective <| ConnectedComponent.eq_of_common_vertex (hg c) (hcd ▸ hg d)
+  simpa [IsTutteViolator] using
+    Finite.card_le_of_injective (fun c ↦ ⟨f c, hf c⟩) (fun c d ↦ by simp [hfinj.eq_iff])
+
+end SimpleGraph

Mathlib/Combinatorics/SimpleGraph/UniversalVerts.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Pim Otte
 -/
 import Mathlib.Combinatorics.SimpleGraph.Clique
+import Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
 import Mathlib.Combinatorics.SimpleGraph.Matching
 
 /-!
@@ -51,4 +52,24 @@ 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 [← Set.disjoint_compl_right_iff_subset, Set.compl_eq_univ_diff] using
+    Subtype.coe_image_subset _ s
+
+/-- A component of the graph with universal vertices is even if we remove a set of representatives
+of odd components and a subset of universal vertices.
+
+This is because the number of vertices in the even components is not affected, and from odd
+components exactly one vertex is removed. -/
+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 [-deleteUniversalVerts_verts, ← 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.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

@@ -927,6 +927,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, left_eq_add]
 
+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