English
Tutte's theorem: a graph has a perfect matching iff for every subset of vertices, removing it leaves at most as many odd components as its size.
Русский
Теорема Тутты: граф имеет совершенное совпадение тогда и только тогда, когда для любой подмножности вершин удаление её не нарушает ограничение по количеству нечетных компонент.
LaTeX
$$$\exists M \subseteq G\, M.IsPerfectMatching \iff \forall u, \neg G.IsTutteViolator u$$$
Lean4
/-- From a graph on an even number of vertices with no perfect matching, we can remove an odd number
of vertices such that there are more odd components in the resulting graph than vertices we removed.
This is the sufficiency side of Tutte's theorem. -/
theorem exists_isTutteViolator (h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching) (hvEven : Even (Nat.card V)) :
∃ u, G.IsTutteViolator u := by
classical
cases nonempty_fintype V
obtain ⟨Gmax, hSubgraph, hMatchingFree, hMaximal⟩ := exists_maximal_isMatchingFree h
refine ⟨Gmax.universalVerts, .mono hSubgraph ?_⟩
by_contra! hc
simp only [IsTutteViolator, Set.ncard_eq_toFinset_card', Set.toFinset_card] at hc
by_cases h' : ∀ (K : ConnectedComponent Gmax.deleteUniversalVerts.coe), Gmax.deleteUniversalVerts.coe.IsClique K.supp
· -- Deleting universal vertices splits the graph into cliques
rw [Fintype.card_eq_nat_card] at hc
simp_rw [Fintype.card_eq_nat_card, Nat.card_coe_set_eq] at hc
push_neg at hc
obtain ⟨M, hM⟩ := Subgraph.IsPerfectMatching.exists_of_isClique_supp hvEven (by simpa [IsTutteViolator] using hc) h'
exact hMatchingFree M hM
· -- Deleting universal vertices does not result in only cliques
push_neg at h'
obtain ⟨K, hK⟩ := h'
obtain ⟨x, y, hxy⟩ := (not_isClique_iff _).mp hK
obtain ⟨p, hp⟩ := Reachable.exists_path_of_dist (K.connected_toSimpleGraph x y)
obtain ⟨x, a, b, hxa, hxb, hnadjxb, hnxb⟩ :=
Walk.exists_adj_adj_not_adj_ne hp.2 (p.reachable.one_lt_dist_of_ne_of_not_adj hxy.1 hxy.2)
simp only [ConnectedComponent.toSimpleGraph, deleteUniversalVerts, universalVerts, ne_eq, Subgraph.induce_verts,
Subgraph.verts_top, comap_adj, Function.Embedding.coe_subtype, Subgraph.coe_adj, Subgraph.induce_adj,
Subtype.coe_prop, Subgraph.top_adj, true_and] at hxa hxb hnadjxb
obtain ⟨c, hc⟩ : ∃ (c : V), (a : V) ≠ c ∧ ¬Gmax.Adj c a := by simpa [universalVerts] using a.1.2.2
have hbnec : b.val.val ≠ c := by rintro rfl; exact hc.2 hxb.symm
obtain ⟨_, hG1⟩ :=
hMaximal _ <|
left_lt_sup.mpr
(by
rw [edge_le_iff (v := x.1.1) (w := b.1.1)]
simp [hnadjxb, Subtype.val_injective.ne <| Subtype.val_injective.ne hnxb])
obtain ⟨_, hG2⟩ := hMaximal _ <| left_lt_sup.mpr (by rwa [edge_le_iff (v := a.1.1) (w := c), adj_comm, not_or])
have hcnex : c ≠ x.val.val := by rintro rfl; exact hc.2 hxa
obtain ⟨Mcon, hMcon⟩ :=
tutte_exists_isPerfectMatching_of_near_matchings hxa hxb hnadjxb (fun hadj ↦ hc.2 hadj.symm) (by aesop) hcnex.symm
hc.1 hbnec hG1 hG2
exact hMatchingFree Mcon hMcon
