Berge's lemma

A matching M of a graph is maximum when no matching has more edges. An M-augmenting path is a path between two distinct vertices not covered by M whose edges alternate between edges outside and inside M. Exchanging the edges of M along such a path gives a matching covering two more vertices. Berge's lemma states the converse for finite graphs: a matching with no augmenting path is maximum. The proof is the standard one ([Sch17], Theorem 3.2). If a matching M' covers more vertices than M, then in M ∆ M' every vertex has degree at most two. The component of a vertex covered by M' only has a second odd-degree vertex. That vertex is covered by M only, since otherwise the path between them would be M-augmenting. So M' covers at most as many vertices as M.

Matchings are Mathlib's SimpleGraph.Subgraph.IsMatching and alternation is Mathlib's SimpleGraph.IsAlternating.

The results about maximum matchings assume a finite vertex type, as in the source.

Main definitions

• SimpleGraph.Subgraph.IsAugmentingPath M p: p is an M-augmenting path.
• SimpleGraph.Subgraph.augment M p: the symmetric difference of M and the edges of p.
• SimpleGraph.Subgraph.IsMaximumMatching M: M is a matching with at least as many edges as every matching.

Main results

• SimpleGraph.Subgraph.IsAugmentingPath.isMatching_augment, SimpleGraph.Subgraph.IsAugmentingPath.ncard_verts_augment: augmenting along an augmenting path gives a matching covering two more vertices.
• SimpleGraph.Subgraph.IsMatching.exists_isAugmentingPath_of_ncard_lt: if a matching covers more vertices than M, there is an M-augmenting path.
• SimpleGraph.Subgraph.IsMatching.isMaximumMatching_iff_forall_not_isAugmentingPath: Berge's lemma. A matching of a finite graph is maximum iff it has no augmenting path.
• SimpleGraph.exists_isMaximumMatching: every finite graph has a maximum matching.

References

• C. Berge, Two Theorems in Graph Theory
• A. Schrijver, A Course in Combinatorial Optimization

theorem SimpleGraph.Walk.IsPath.exists_ne_adj_toSubgraph {V : Type u_1} {G : SimpleGraph V} {u v x a : V} {p : G.Walk u v} (hp : p.IsPath) (hxu : x ≠ u) (hxv : x ≠ v) (ha : p.toSubgraph.Adj x a) : ∃ (b : V), b ≠ a ∧ p.toSubgraph.Adj x b

A vertex of a path other than its two ends has two distinct neighbours on the path.

structure SimpleGraph.Subgraph.IsAugmentingPath {V : Type u_1} {G : SimpleGraph V} (M : G.Subgraph) {u v : V} (p : G.Walk u v) : Prop

p is an M-augmenting path: a path between two distinct vertices not covered by M whose edges alternate between edges outside and inside M ([Ber57]; [Sch17], Section 3.2). Alternation is Mathlib's SimpleGraph.IsAlternating: of two distinct edges of p at a vertex, exactly one lies in M. Since both ends are uncovered, the first and last edges lie outside M and the path has odd length.

• isPath : p.IsPath
• ne : u ≠ v
• start_notMem : u ∉ M.verts
• end_notMem : v ∉ M.verts
• isAlternating : p.toSubgraph.spanningCoe.IsAlternating M.spanningCoe

def SimpleGraph.Subgraph.augment {V : Type u_1} {G : SimpleGraph V} (M : G.Subgraph) {u v : V} (p : G.Walk u v) : G.Subgraph

The matching M ∆ E(p) obtained by augmenting M along the walk p: an edge belongs to it when it belongs to exactly one of M and p. Its vertices are those of M and of p.

theorem SimpleGraph.Subgraph.augment_adj {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} {u v x y : V} {p : G.Walk u v} : (M.augment p).Adj x y ↔ M.Adj x y ∧ ¬p.toSubgraph.Adj x y ∨ p.toSubgraph.Adj x y ∧ ¬M.Adj x y

theorem SimpleGraph.Subgraph.verts_augment {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} {u v : V} {p : G.Walk u v} : (M.augment p).verts = M.verts ∪ {x : V | x ∈ p.support}

theorem SimpleGraph.Subgraph.IsAugmentingPath.not_nil {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} {u v : V} {p : G.Walk u v} (hp : M.IsAugmentingPath p) : ¬p.Nil

theorem SimpleGraph.Subgraph.IsAugmentingPath.mem_verts_of_mem_support {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} {u v : V} {p : G.Walk u v} (hp : M.IsAugmentingPath p) {x : V} (hx : x ∈ p.support) (hxu : x ≠ u) (hxv : x ≠ v) : x ∈ M.verts

An inner vertex of an augmenting path is covered by M.

theorem SimpleGraph.Subgraph.IsAugmentingPath.isMatching_augment {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} {u v : V} {p : G.Walk u v} (hM : M.IsMatching) (hp : M.IsAugmentingPath p) : (M.augment p).IsMatching

Augmenting a matching along an augmenting path gives a matching.

theorem SimpleGraph.Subgraph.IsAugmentingPath.verts_augment_eq {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} {u v : V} {p : G.Walk u v} (hp : M.IsAugmentingPath p) : (M.augment p).verts = insert u (insert v M.verts)

theorem SimpleGraph.Subgraph.IsAugmentingPath.ncard_verts_augment {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} {u v : V} {p : G.Walk u v} [Finite V] (hp : M.IsAugmentingPath p) : (M.augment p).verts.ncard = M.verts.ncard + 2

The symmetric difference of two matchings

theorem SimpleGraph.Subgraph.IsMatching.isAlternating_symmDiff {V : Type u_1} {G : SimpleGraph V} {M M' : G.Subgraph} (hM : M.IsMatching) (hM' : M'.IsMatching) : (symmDiff M.spanningCoe M'.spanningCoe).IsAlternating M.spanningCoe

The symmetric difference of two matchings alternates with respect to the first one. For two matchings of the same graph, this generalizes Mathlib's Subgraph.IsPerfectMatching.isAlternating_symmDiff_left from perfect matchings to arbitrary matchings (Mathlib's lemma allows the second matching to live in a different graph).

theorem SimpleGraph.Subgraph.IsMatching.exists_neighborSet_symmDiff_eq_singleton {V : Type u_1} {G : SimpleGraph V} {M M' : G.Subgraph} (hM' : M'.IsMatching) {x : V} (hx : x ∉ M.verts) (hx' : x ∈ M'.verts) : ∃ (b : V), (symmDiff M.spanningCoe M'.spanningCoe).neighborSet x = {b}

A vertex covered by M' but not by M has exactly one neighbour in M ∆ M', its partner in M'.

theorem SimpleGraph.Subgraph.IsMatching.xor_of_odd_ncard_neighborSet_symmDiff {V : Type u_1} {G : SimpleGraph V} {M M' : G.Subgraph} (hM : M.IsMatching) (hM' : M'.IsMatching) {x : V} (hodd : Odd ((symmDiff M.spanningCoe M'.spanningCoe).neighborSet x).ncard) : Xor (x ∈ M.verts) (x ∈ M'.verts)

A vertex has an odd number of neighbours in M ∆ M' only if exactly one of M and M' covers it.

theorem SimpleGraph.Subgraph.IsMatching.exists_isAugmentingPath_of_ncard_lt {V : Type u_1} {G : SimpleGraph V} {M M' : G.Subgraph} [Finite V] (hM : M.IsMatching) (hM' : M'.IsMatching) (hlt : M.verts.ncard < M'.verts.ncard) : ∃ (u : V) (v : V) (p : G.Walk u v), M.IsAugmentingPath p

Berge's lemma, hard direction ([Ber57], Theorem 1; [Sch17], Theorem 3.2): if a matching M' covers more vertices than a matching M, then there is an M-augmenting path.

Maximum matchings and Berge's lemma

structure SimpleGraph.Subgraph.IsMaximumMatching {V : Type u_1} {G : SimpleGraph V} (M : G.Subgraph) : Prop

M is a maximum matching of G: a matching with at least as many edges as every matching of G. Edges are counted with Set.encard. The definition needs no finiteness hypothesis, but it is coarse on infinite graphs, where every matching with infinitely many edges is maximum. The results below assume [Finite V].

• isMatching : M.IsMatching
• maximum (M' : G.Subgraph) : M'.IsMatching → M'.edgeSet.encard ≤ M.edgeSet.encard

theorem SimpleGraph.Subgraph.IsMatching.ncard_verts_eq_two_mul {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} [Finite V] (hM : M.IsMatching) : M.verts.ncard = 2 * M.edgeSet.ncard

A matching of a finite graph covers twice as many vertices as it has edges.

theorem SimpleGraph.Subgraph.isMaximumMatching_iff_ncard {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} [Finite V] : M.IsMaximumMatching ↔ M.IsMatching ∧ ∀ (M' : G.Subgraph), M'.IsMatching → M'.edgeSet.ncard ≤ M.edgeSet.ncard

In a finite graph, maximality of a matching may be tested by comparing edge counts with Set.ncard.

theorem SimpleGraph.Subgraph.IsMatching.isMaximumMatching_iff_ncard_verts {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} [Finite V] (hM : M.IsMatching) : M.IsMaximumMatching ↔ ∀ (M' : G.Subgraph), M'.IsMatching → M'.verts.ncard ≤ M.verts.ncard

In a finite graph a matching is maximum iff it covers at least as many vertices as every matching.

theorem SimpleGraph.Subgraph.IsPerfectMatching.isMaximumMatching {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} [Finite V] (hM : M.IsPerfectMatching) : M.IsMaximumMatching

A perfect matching of a finite graph is maximum.

theorem SimpleGraph.exists_isMaximumMatching {V : Type u_1} [Finite V] (G : SimpleGraph V) : ∃ (M : G.Subgraph), M.IsMaximumMatching

A finite graph has a maximum matching.

theorem SimpleGraph.Subgraph.IsMatching.isMaximumMatching_iff_forall_not_isAugmentingPath {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} [Finite V] (hM : M.IsMatching) : M.IsMaximumMatching ↔ ∀ (u v : V) (p : G.Walk u v), ¬M.IsAugmentingPath p

Berge's lemma ([Ber57], Theorem 1; [Sch17], Theorem 3.2): a matching of a finite graph is maximum iff there is no augmenting path.