Skip to content

Commit 5b76dec

Browse files
pimotteYaelDillies
pimotte
and
YaelDillies
committed
feat(Combinatorics/SimpleGraph): part of Tutte's theorem (#22119)
Adds three key parts of the proof of Tutte's theorem, with some supporting lemma's: - necessity of the Tutte condition (`not_isTutteViolator`) - the fact that the empty set violates the Tutte condition if the number of vertices is odd (`IsTutteViolator.empty`) - the construction of a perfect matching in a graph that decomposes into cliques (`Subgraph.IsPerfectMatching.exists_of_isClique_supp`) Definitions added: `IsTutteViolator`. Co-authored-by: Pim Otte <otte.pim@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
1 parent d8c00d3 commit 5b76dec

File tree

6 files changed

+195
-11
lines changed

6 files changed

+195
-11
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2667,6 +2667,7 @@ import Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
26672667
import Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
26682668
import Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
26692669
import Mathlib.Combinatorics.SimpleGraph.Turan
2670+
import Mathlib.Combinatorics.SimpleGraph.Tutte
26702671
import Mathlib.Combinatorics.SimpleGraph.UniversalVerts
26712672
import Mathlib.Combinatorics.SimpleGraph.Walk
26722673
import Mathlib.Combinatorics.Young.SemistandardTableau

‎Mathlib/Combinatorics/SimpleGraph/Connectivity/Represents.lean‎

Lines changed: 17 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Pim Otte
55
-/
66

7-
import Mathlib.Combinatorics.SimpleGraph.Path
7+
import Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting
88
import Mathlib.Data.Set.Card
99

1010
/-!
@@ -60,6 +60,9 @@ lemma ncard_inter (hrep : Represents s C) (h : c ∈ C) : (s ∩ c.supp).ncard =
6060
rw [Set.ncard_eq_one]
6161
exact exists_inter_eq_singleton hrep h
6262

63+
lemma ncard_eq (hrep : Represents s C) : s.ncard = C.ncard :=
64+
hrep.image_eq ▸ (Set.ncard_image_of_injOn hrep.injOn).symm
65+
6366
lemma ncard_sdiff_of_mem (hrep : Represents s C) (h : c ∈ C) :
6467
(c.supp \ s).ncard = c.supp.ncard - 1 := by
6568
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) :
7073
(c.supp \ s).ncard = c.supp.ncard := by
7174
rw [(disjoint_supp_of_not_mem hrep h).sdiff_eq_right]
7275

73-
end SimpleGraph.ConnectedComponent.Represents
76+
end ConnectedComponent.Represents
77+
78+
lemma ConnectedComponent.even_ncard_supp_sdiff_rep {s : Set V} (K : G.ConnectedComponent)
79+
(hrep : ConnectedComponent.Represents s G.oddComponents) :
80+
Even (K.supp \ s).ncard := by
81+
by_cases h : Even K.supp.ncard
82+
· simpa [hrep.ncard_sdiff_of_not_mem
83+
(by simpa [Set.ncard_image_of_injective, ← Nat.not_odd_iff_even] using h)] using h
84+
· have : K.supp.ncard ≠ 0 := Nat.ne_of_odd_add (Nat.not_even_iff_odd.mp h)
85+
rw [hrep.ncard_sdiff_of_mem (Nat.not_even_iff_odd.mp h), Nat.even_sub (by omega)]
86+
simpa [Nat.even_sub] using Nat.not_even_iff_odd.mp h
87+
88+
end SimpleGraph

‎Mathlib/Combinatorics/SimpleGraph/Matching.lean‎

Lines changed: 27 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,13 @@ Copyright (c) 2020 Alena Gusakov. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Alena Gusakov, Arthur Paulino, Kyle Miller, Pim Otte
55
-/
6+
import Mathlib.Combinatorics.SimpleGraph.Clique
67
import Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
78
import Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting
89
import Mathlib.Combinatorics.SimpleGraph.DegreeSum
910
import Mathlib.Combinatorics.SimpleGraph.Operations
1011
import Mathlib.Data.Fintype.Order
12+
import Mathlib.Data.Set.Card.Arithmetic
1113
import Mathlib.Data.Set.Functor
1214

1315
/-!
@@ -53,7 +55,7 @@ assert_not_exists Field TwoSidedIdeal
5355
open Function
5456

5557
namespace SimpleGraph
56-
variable {V W : Type*} {G G' : SimpleGraph V} {M M' : Subgraph G} {v w : V}
58+
variable {V W : Type*} {G G' : SimpleGraph V} {M M' : Subgraph G} {u v w : V}
5759

5860
namespace Subgraph
5961

@@ -90,15 +92,17 @@ lemma IsMatching.map_ofLE (h : M.IsMatching) (hGG' : G ≤ G') :
9092
use w
9193
simpa using hv' ▸ hw
9294

93-
lemma IsMatching.not_adj_left_of_ne {M : Subgraph G} {u v w : V} (hM : M.IsMatching) (huv : v ≠ w)
94-
(hadj : M.Adj u v) : ¬M.Adj u w := by
95-
intro hadj'
96-
obtain ⟨x, hx⟩ := hM (M.edge_vert hadj)
97-
exact huv (hx.2 _ hadj ▸ (hx.2 _ hadj').symm)
95+
lemma IsMatching.eq_of_adj_left (hM : M.IsMatching) (huv : M.Adj u v) (huw : M.Adj u w) : v = w :=
96+
(hM <| M.edge_vert huv).unique huv huw
9897

99-
lemma IsMatching.not_adj_right_of_ne {M : Subgraph G} {u v w : V} (hM : M.IsMatching) (huw : u ≠ w)
100-
(hadj : M.Adj u v) : ¬M.Adj w v :=
101-
fun hadj' ↦ hM.not_adj_left_of_ne huw hadj.symm hadj'.symm
98+
lemma IsMatching.eq_of_adj_right (hM : M.IsMatching) (huw : M.Adj u w) (hvw : M.Adj v w) : u = v :=
99+
hM.eq_of_adj_left huw.symm hvw.symm
100+
101+
lemma IsMatching.not_adj_left_of_ne (hM : M.IsMatching) (hvw : v ≠ w) (huv : M.Adj u v) :
102+
¬M.Adj u w := fun huw ↦ hvw <| hM.eq_of_adj_left huv huw
103+
104+
lemma IsMatching.not_adj_right_of_ne (hM : M.IsMatching) (huv : u ≠ v) (huw : M.Adj u w) :
105+
¬M.Adj v w := fun hvw ↦ huv <| hM.eq_of_adj_right huw hvw
102106

103107
lemma IsMatching.sup (hM : M.IsMatching) (hM' : M'.IsMatching)
104108
(hd : Disjoint M.support M'.support) : (M ⊔ M').IsMatching := by
@@ -260,6 +264,20 @@ lemma IsPerfectMatching.toSubgraph_iff (h : M.spanningCoe ≤ G') :
260264

261265
end Subgraph
262266

267+
lemma IsClique.even_iff_exists_isMatching {u : Set V} (hc : G.IsClique u)
268+
(hu : u.Finite) : Even u.ncard ↔ ∃ (M : Subgraph G), M.verts = u ∧ M.IsMatching := by
269+
refine ⟨fun h ↦ ?_, by
270+
rintro ⟨M, rfl, hMr⟩
271+
simpa [Set.ncard_eq_toFinset_card _ hu, Set.toFinite_toFinset,
272+
← Set.toFinset_card] using @hMr.even_card _ _ _ hu.fintype⟩
273+
obtain ⟨t, u, rfl, hd, hcard⟩ := Set.exists_union_disjoint_ncard_eq_of_even h
274+
obtain ⟨f⟩ : Nonempty (t ≃ u) := by
275+
rw [← Cardinal.eq, ← t.cast_ncard (Set.finite_union.mp hu).1,
276+
← u.cast_ncard (Set.finite_union.mp hu).2]
277+
exact congrArg Nat.cast hcard
278+
exact Subgraph.IsMatching.exists_of_disjoint_sets_of_equiv hd f
279+
fun v ↦ hc (by simp) (by simp) <| hd.ne_of_mem (by simp) (by simp)
280+
263281
namespace ConnectedComponent
264282

265283
section Finite

‎Mathlib/Combinatorics/SimpleGraph/Tutte.lean‎

Lines changed: 119 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,119 @@
1+
/-
2+
Copyright (c) 2024 Pim Otte. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Pim Otte
5+
-/
6+
7+
import Mathlib.Combinatorics.SimpleGraph.Matching
8+
import Mathlib.Combinatorics.SimpleGraph.Operations
9+
import Mathlib.Combinatorics.SimpleGraph.UniversalVerts
10+
import Mathlib.Data.Fintype.Card
11+
12+
/-!
13+
# Tutte's theorem (work in progress)
14+
15+
## Main definitions
16+
* `SimpleGraph.TutteViolator G u` is a set of vertices `u` which certifies non-existence of a
17+
perfect matching.
18+
-/
19+
20+
namespace SimpleGraph
21+
22+
universe u
23+
variable {V : Type u} {G G' : SimpleGraph V} {u x v' w : V} [Fintype V]
24+
25+
/-- A set certifying non-existence of a perfect matching. -/
26+
def IsTutteViolator (G : SimpleGraph V) (u : Set V) : Prop :=
27+
u.ncard < ((⊤ : G.Subgraph).deleteVerts u).coe.oddComponents.ncard
28+
29+
/-- Given a graph in which the universal vertices do not violate Tutte's condition,
30+
if the graph decomposes into cliques, there exists a matching that covers
31+
everything except some universal vertices.
32+
33+
This lemma is marked private, because
34+
it is strictly weaker than `IsPerfectMatching.exists_of_isClique_supp`. -/
35+
private lemma Subgraph.IsMatching.exists_verts_compl_subset_universalVerts
36+
(h : ¬IsTutteViolator G G.universalVerts)
37+
(h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent),
38+
G.deleteUniversalVerts.coe.IsClique K.supp) :
39+
∃ M : Subgraph G, M.IsMatching ∧ M.vertsᶜ ⊆ G.universalVerts := by
40+
classical
41+
have hrep := ConnectedComponent.Represents.image_out
42+
G.deleteUniversalVerts.coe.oddComponents
43+
-- First we match one node from each odd component to a universal vertex
44+
obtain ⟨t, ht, M1, hM1⟩ := Subgraph.IsMatching.exists_of_universalVerts
45+
(disjoint_image_val_universalVerts _).symm (by
46+
simp only [IsTutteViolator, not_lt] at h
47+
rwa [Set.ncard_image_of_injective _ Subtype.val_injective, hrep.ncard_eq])
48+
-- Then we match all other nodes in components internally
49+
have exists_complMatch (K : G.deleteUniversalVerts.coe.ConnectedComponent) :
50+
∃ M : Subgraph G, M.verts = Subtype.val '' K.supp \ M1.verts ∧ M.IsMatching := by
51+
have : G.IsClique (Subtype.val '' K.supp \ M1.verts) :=
52+
((h' K).of_induce).subset Set.diff_subset
53+
rw [← this.even_iff_exists_isMatching (Set.toFinite _), hM1.1]
54+
exact even_ncard_image_val_supp_sdiff_image_val_rep_union _ ht hrep
55+
choose complMatch hcomplMatch_compl hcomplMatch_match using exists_complMatch
56+
let M2 : Subgraph G := ⨆ K, complMatch K
57+
have hM2 : M2.IsMatching := by
58+
refine .iSup hcomplMatch_match fun i j hij ↦ (?_ : Disjoint _ _)
59+
rw [(hcomplMatch_match i).support_eq_verts, hcomplMatch_compl i,
60+
(hcomplMatch_match j).support_eq_verts, hcomplMatch_compl j]
61+
exact Set.disjoint_of_subset Set.diff_subset Set.diff_subset <|
62+
Set.disjoint_image_of_injective Subtype.val_injective <|
63+
SimpleGraph.pairwise_disjoint_supp_connectedComponent _ hij
64+
have disjointM12 : Disjoint M1.support M2.support := by
65+
rw [hM1.2.support_eq_verts, hM2.support_eq_verts, Subgraph.verts_iSup,
66+
Set.disjoint_iUnion_right]
67+
exact fun K ↦ hcomplMatch_compl K ▸ Set.disjoint_sdiff_right
68+
-- The only vertices left are indeed contained in universalVerts
69+
have : (M1.verts ∪ M2.verts)ᶜ ⊆ G.universalVerts := by
70+
rw [Set.compl_subset_comm, Set.compl_eq_univ_diff]
71+
intro v hv
72+
by_cases h : v ∈ M1.verts
73+
· exact M1.verts.mem_union_left _ h
74+
right
75+
simp only [deleteUniversalVerts_verts, Subgraph.verts_iSup, Set.mem_iUnion, M2,
76+
hcomplMatch_compl]
77+
use G.deleteUniversalVerts.coe.connectedComponentMk ⟨v, hv⟩
78+
aesop
79+
exact ⟨M1 ⊔ M2, hM1.2.sup hM2 disjointM12, this⟩
80+
81+
/-- Given a graph in which the universal vertices do not violate Tutte's condition,
82+
if the graph decomposes into cliques, it has a perfect matching. -/
83+
theorem Subgraph.IsPerfectMatching.exists_of_isClique_supp
84+
(hveven : Even (Nat.card V)) (h : ¬G.IsTutteViolator G.universalVerts)
85+
(h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent),
86+
G.deleteUniversalVerts.coe.IsClique K.supp) : ∃ (M : Subgraph G), M.IsPerfectMatching := by
87+
classical
88+
obtain ⟨M, hM, hsub⟩ := IsMatching.exists_verts_compl_subset_universalVerts h h'
89+
obtain ⟨M', hM'⟩ := ((G.isClique_universalVerts.subset hsub).even_iff_exists_isMatching
90+
(Set.toFinite _)).mp (by simpa [Set.even_ncard_compl_iff hveven, -Set.toFinset_card,
91+
← Set.ncard_eq_toFinset_card'] using hM.even_card)
92+
use M ⊔ M'
93+
have hspan : (M ⊔ M').IsSpanning := by
94+
rw [Subgraph.isSpanning_iff, Subgraph.verts_sup, hM'.1]
95+
exact M.verts.union_compl_self
96+
exact ⟨hM.sup hM'.2 (by
97+
simp only [hM.support_eq_verts, hM'.2.support_eq_verts, hM'.1, Subgraph.verts_sup]
98+
exact (Set.disjoint_compl_left_iff_subset.mpr fun ⦃a⦄ a ↦ a).symm), hspan⟩
99+
100+
theorem IsTutteViolator.empty (hodd : Odd (Fintype.card V)) : G.IsTutteViolator ∅ := by
101+
have c :=
102+
Finite.card_pos_iff.mp
103+
((odd_ncard_oddComponents ((⊤ : Subgraph G).deleteVerts ∅).coe).mpr (by
104+
simpa [Fintype.card_congr (Equiv.Set.univ V)] using hodd)).pos
105+
rw [IsTutteViolator, Set.ncard_empty, Set.ncard_pos]
106+
exact Set.Nonempty.of_subtype
107+
108+
/-- Proves the necessity part of Tutte's theorem -/
109+
lemma not_isTutteViolator_of_isPerfectMatching {M : Subgraph G} (hM : M.IsPerfectMatching)
110+
(u : Set V) :
111+
¬G.IsTutteViolator u := by
112+
choose f hf g hgf hg using ConnectedComponent.odd_matches_node_outside hM (u := u)
113+
have hfinj : f.Injective := fun c d hcd ↦ by
114+
replace hcd : g c = g d := Subtype.val_injective <| hM.1.eq_of_adj_right (hgf c) (hcd ▸ hgf d)
115+
exact Subtype.val_injective <| ConnectedComponent.eq_of_common_vertex (hg c) (hcd ▸ hg d)
116+
simpa [IsTutteViolator] using
117+
Finite.card_le_of_injective (fun c ↦ ⟨f c, hf c⟩) (fun c d ↦ by simp [hfinj.eq_iff])
118+
119+
end SimpleGraph

‎Mathlib/Combinatorics/SimpleGraph/UniversalVerts.lean‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Pim Otte
55
-/
66
import Mathlib.Combinatorics.SimpleGraph.Clique
7+
import Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
78
import Mathlib.Combinatorics.SimpleGraph.Matching
89

910
/-!
@@ -51,4 +52,24 @@ lemma Subgraph.IsMatching.exists_of_universalVerts [Finite V] {s : Set V}
5152
have hadj (v : s) : G.Adj v (f v) := ht.1 (f v).2 (hd.ne_of_mem (f v).2 v.2)
5253
exact Subgraph.IsMatching.exists_of_disjoint_sets_of_equiv hd.symm f hadj
5354

55+
lemma disjoint_image_val_universalVerts (s : Set G.deleteUniversalVerts.verts) :
56+
Disjoint (Subtype.val '' s) G.universalVerts := by
57+
simpa [← Set.disjoint_compl_right_iff_subset, Set.compl_eq_univ_diff] using
58+
Subtype.coe_image_subset _ s
59+
60+
/-- A component of the graph with universal vertices is even if we remove a set of representatives
61+
of odd components and a subset of universal vertices.
62+
63+
This is because the number of vertices in the even components is not affected, and from odd
64+
components exactly one vertex is removed. -/
65+
lemma even_ncard_image_val_supp_sdiff_image_val_rep_union {t : Set V}
66+
{s : Set G.deleteUniversalVerts.verts} (K : G.deleteUniversalVerts.coe.ConnectedComponent)
67+
(h : t ⊆ G.universalVerts)
68+
(hrep : ConnectedComponent.Represents s G.deleteUniversalVerts.coe.oddComponents) :
69+
Even (Subtype.val '' K.supp \ (Subtype.val '' s ∪ t)).ncard := by
70+
simp [-deleteUniversalVerts_verts, ← Set.diff_inter_diff, ← Set.image_diff Subtype.val_injective,
71+
sdiff_eq_left.mpr <| Set.disjoint_of_subset_right h (disjoint_image_val_universalVerts _),
72+
Set.inter_diff_distrib_right, ← Set.image_inter Subtype.val_injective,
73+
Set.ncard_image_of_injective _ Subtype.val_injective, K.even_ncard_supp_sdiff_rep hrep]
74+
5475
end SimpleGraph

‎Mathlib/Data/Set/Card.lean‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -936,6 +936,16 @@ theorem eq_univ_iff_ncard [Finite α] (s : Set α) :
936936
s = univ ↔ ncard s = Nat.card α := by
937937
rw [← compl_empty_iff, ← ncard_eq_zero, ← ncard_add_ncard_compl s, left_eq_add]
938938

939+
lemma even_ncard_compl_iff [Finite α] (heven : Even (Nat.card α)) (s : Set α) :
940+
Even sᶜ.ncard ↔ Even s.ncard := by
941+
simp [compl_eq_univ_diff, ncard_diff (subset_univ _ : s ⊆ Set.univ),
942+
Nat.even_sub (ncard_le_ncard (subset_univ _ : s ⊆ Set.univ)),
943+
(ncard_univ _).symm ▸ heven]
944+
945+
lemma odd_ncard_compl_iff [Finite α] (heven : Even (Nat.card α)) (s : Set α) :
946+
Odd sᶜ.ncard ↔ Odd s.ncard := by
947+
rw [← Nat.not_even_iff_odd, even_ncard_compl_iff heven, Nat.not_even_iff_odd]
948+
939949
end Lattice
940950

941951
/-- Given a subset `s` of a set `t`, of sizes at most and at least `n` respectively, there exists a

0 commit comments

Comments
 (0)
⚡