Matchings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A matching for a simple graph is a set of disjoint pairs of adjacent vertices, and the set of all the vertices in a matching is called its support (and sometimes the vertices in the support are said to be saturated by the matching). A perfect matching is a matching whose support contains every vertex of the graph.

In this module, we represent a matching as a subgraph whose vertices are each incident to at most one edge, and the edges of the subgraph represent the paired vertices.

Main definitions #

simple_graph.subgraph.is_matching: M.is_matching means that M is a matching of its underlying graph. denoted M.is_matching.
simple_graph.subgraph.is_perfect_matching defines when a subgraph M of a simple graph is a perfect matching, denoted M.is_perfect_matching.

TODO #

Define an other function and prove useful results about it (https://leanprover.zulipchat.com/#narrow/stream/252551-graph-theory/topic/matchings/near/266205863)
Provide a bicoloring for matchings (https://leanprover.zulipchat.com/#narrow/stream/252551-graph-theory/topic/matchings/near/265495120)
Tutte's Theorem
Hall's Marriage Theorem (see combinatorics.hall)

source

def simple_graph.subgraph.is_matching {V : Type u} {G : simple_graph V} (M : G.subgraph) :

Prop

The subgraph M of G is a matching if every vertex of M is incident to exactly one edge in M. We say that the vertices in M.support are matched or saturated.

Equations

M.is_matching = ∀ ⦃v : V⦄, v ∈ M.verts → (∃! (w : V), M.adj v w)

source

noncomputable def simple_graph.subgraph.is_matching.to_edge {V : Type u} {G : simple_graph V} {M : G.subgraph} (h : M.is_matching) (v : ↥(M.verts)) :

↥(M.edge_set)

Given a vertex, returns the unique edge of the matching it is incident to.

Equations

h.to_edge v = ⟨⟦(↑v, Exists.some _)⟧, _⟩

source

theorem simple_graph.subgraph.is_matching.to_edge_eq_of_adj {V : Type u} {G : simple_graph V} {M : G.subgraph} (h : M.is_matching) {v w : V} (hv : v ∈ M.verts) (hvw : M.adj v w) :

h.to_edge ⟨v, hv⟩ = ⟨⟦(v, w)⟧, hvw⟩

source

theorem simple_graph.subgraph.is_matching.to_edge.surjective {V : Type u} {G : simple_graph V} {M : G.subgraph} (h : M.is_matching) :

function.surjective h.to_edge

source

theorem simple_graph.subgraph.is_matching.to_edge_eq_to_edge_of_adj {V : Type u} {G : simple_graph V} {M : G.subgraph} {v w : V} (h : M.is_matching) (hv : v ∈ M.verts) (hw : w ∈ M.verts) (ha : M.adj v w) :

h.to_edge ⟨v, hv⟩ = h.to_edge ⟨w, hw⟩

source

def simple_graph.subgraph.is_perfect_matching {V : Type u} {G : simple_graph V} (M : G.subgraph) :

Prop

The subgraph M of G is a perfect matching on G if it's a matching and every vertex G is matched.

Equations

M.is_perfect_matching = (M.is_matching ∧ M.is_spanning)

source

theorem simple_graph.subgraph.is_matching.support_eq_verts {V : Type u} {G : simple_graph V} {M : G.subgraph} (h : M.is_matching) :

M.support = M.verts

source

theorem simple_graph.subgraph.is_matching_iff_forall_degree {V : Type u} {G : simple_graph V} {M : G.subgraph} [Π (v : V), fintype ↥(M.neighbor_set v)] :

M.is_matching ↔ ∀ (v : V), v ∈ M.verts → M.degree v = 1

source

theorem simple_graph.subgraph.is_matching.even_card {V : Type u} {G : simple_graph V} {M : G.subgraph} [fintype ↥(M.verts)] (h : M.is_matching) :

even M.verts.to_finset.card

source

theorem simple_graph.subgraph.is_perfect_matching_iff {V : Type u} {G : simple_graph V} (M : G.subgraph) :

M.is_perfect_matching ↔ ∀ (v : V), ∃! (w : V), M.adj v w

source

theorem simple_graph.subgraph.is_perfect_matching_iff_forall_degree {V : Type u} {G : simple_graph V} {M : G.subgraph} [Π (v : V), fintype ↥(M.neighbor_set v)] :

M.is_perfect_matching ↔ ∀ (v : V), M.degree v = 1

source

theorem simple_graph.subgraph.is_perfect_matching.even_card {V : Type u} {G : simple_graph V} {M : G.subgraph} [fintype V] (h : M.is_perfect_matching) :

even (fintype.card V)