Tutte's theorem

Main definitions

• SimpleGraph.TutteViolator G u is a set of vertices u such that the amount of odd components left after deleting u from G is larger than the number of vertices in u. This certifies non-existence of a perfect matching.

Main results

• SimpleGraph.tutte states Tutte's theorem: A graph has a perfect matching, if and only if no Tutte violators exist.

def SimpleGraph.IsTutteViolator {V : Type u_1} (G : SimpleGraph V) (u : Set V) : Prop

A set certifying non-existence of a perfect matching

Equations

• G.IsTutteViolator u = (u.ncard < (⊤.deleteVerts u).coe.oddComponents.ncard)

theorem SimpleGraph.IsTutteViolator.mono {V : Type u_1} {G G' : SimpleGraph V} [Finite V] {u : Set V} (h : G ≤ G') (ht : G'.IsTutteViolator u) : G.IsTutteViolator u

theorem SimpleGraph.Subgraph.IsPerfectMatching.exists_of_isClique_supp {V : Type u_1} {G : SimpleGraph V} [Finite V] (hveven : Even (Nat.card V)) (h : ¬G.IsTutteViolator G.universalVerts) (h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp) : ∃ (M : G.Subgraph), M.IsPerfectMatching

If the universal vertices of a graph G decompose G into cliques such that the Tutte isn't violated, then G has a perfect matching.

theorem SimpleGraph.IsTutteViolator.empty {V : Type u_1} {G : SimpleGraph V} [Finite V] (hodd : Odd (Nat.card V)) : G.IsTutteViolator ∅

theorem SimpleGraph.not_isTutteViolator_of_isPerfectMatching {V : Type u_1} {G : SimpleGraph V} [Finite V] {M : G.Subgraph} (hM : M.IsPerfectMatching) (u : Set V) : ¬G.IsTutteViolator u

Proves the necessity part of Tutte's theorem

theorem SimpleGraph.exists_isTutteViolator {V : Type u_1} {G : SimpleGraph V} [Finite V] (h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching) (hvEven : Even (Nat.card V)) : ∃ (u : Set V), G.IsTutteViolator u

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 SimpleGraph.tutte {V : Type u_1} {G : SimpleGraph V} [Finite V] : (∃ (M : G.Subgraph), M.IsPerfectMatching) ↔ ∀ (u : Set V), ¬G.IsTutteViolator u

Tutte's theorem

A graph has a perfect matching if and only if: For every subset u of vertices, removing this subset induces at most u.ncard components of odd size. This is formally stated using the predicate IsTutteViolator, which is satisfied exactly when this condition does not hold.