Matchings

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

• SimpleGraph.Subgraph.IsMatching: M.IsMatching means that M is a matching of its underlying graph. denoted M.is_matching.

• SimpleGraph.Subgraph.IsPerfectMatching defines when a subgraph M of a simple graph is a perfect matching, denoted M.IsPerfectMatching.

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)

def SimpleGraph.Subgraph.IsMatching {V : Type u} {G : SimpleGraph V} (M : SimpleGraph.Subgraph G) : 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

• SimpleGraph.Subgraph.IsMatching M = ∀ ⦃v : V⦄, v ∈ M.verts → ∃! (w : V), M.Adj v w

noncomputable def SimpleGraph.Subgraph.IsMatching.toEdge {V : Type u} {G : SimpleGraph V} {M : SimpleGraph.Subgraph G} (h : SimpleGraph.Subgraph.IsMatching M) (v : ↑M.verts) : ↑(SimpleGraph.Subgraph.edgeSet M)

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

Equations

• SimpleGraph.Subgraph.IsMatching.toEdge h v = { val := s(↑v, Exists.choose ⋯), property := ⋯ }

theorem SimpleGraph.Subgraph.IsMatching.toEdge_eq_of_adj {V : Type u} {G : SimpleGraph V} {M : SimpleGraph.Subgraph G} (h : SimpleGraph.Subgraph.IsMatching M) {v : V} {w : V} (hv : v ∈ M.verts) (hvw : M.Adj v w) : SimpleGraph.Subgraph.IsMatching.toEdge h { val := v, property := hv } = { val := s(v, w), property := hvw }

theorem SimpleGraph.Subgraph.IsMatching.toEdge.surjective {V : Type u} {G : SimpleGraph V} {M : SimpleGraph.Subgraph G} (h : SimpleGraph.Subgraph.IsMatching M) : Function.Surjective (SimpleGraph.Subgraph.IsMatching.toEdge h)

theorem SimpleGraph.Subgraph.IsMatching.toEdge_eq_toEdge_of_adj {V : Type u} {G : SimpleGraph V} {M : SimpleGraph.Subgraph G} {v : V} {w : V} (h : SimpleGraph.Subgraph.IsMatching M) (hv : v ∈ M.verts) (hw : w ∈ M.verts) (ha : M.Adj v w) : SimpleGraph.Subgraph.IsMatching.toEdge h { val := v, property := hv } = SimpleGraph.Subgraph.IsMatching.toEdge h { val := w, property := hw }

def SimpleGraph.Subgraph.IsPerfectMatching {V : Type u} {G : SimpleGraph V} (M : SimpleGraph.Subgraph G) : Prop

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

Equations

• SimpleGraph.Subgraph.IsPerfectMatching M = (SimpleGraph.Subgraph.IsMatching M ∧ SimpleGraph.Subgraph.IsSpanning M)

theorem SimpleGraph.Subgraph.IsMatching.support_eq_verts {V : Type u} {G : SimpleGraph V} {M : SimpleGraph.Subgraph G} (h : SimpleGraph.Subgraph.IsMatching M) : SimpleGraph.Subgraph.support M = M.verts

theorem SimpleGraph.Subgraph.isMatching_iff_forall_degree {V : Type u} {G : SimpleGraph V} {M : SimpleGraph.Subgraph G} [(v : V) → Fintype ↑(SimpleGraph.Subgraph.neighborSet M v)] : SimpleGraph.Subgraph.IsMatching M ↔ ∀ v ∈ M.verts, SimpleGraph.Subgraph.degree M v = 1

theorem SimpleGraph.Subgraph.IsMatching.even_card {V : Type u} {G : SimpleGraph V} {M : SimpleGraph.Subgraph G} [Fintype ↑M.verts] (h : SimpleGraph.Subgraph.IsMatching M) : Even (Set.toFinset M.verts).card

theorem SimpleGraph.Subgraph.isPerfectMatching_iff {V : Type u} {G : SimpleGraph V} (M : SimpleGraph.Subgraph G) : SimpleGraph.Subgraph.IsPerfectMatching M ↔ ∀ (v : V), ∃! (w : V), M.Adj v w

theorem SimpleGraph.Subgraph.isPerfectMatching_iff_forall_degree {V : Type u} {G : SimpleGraph V} {M : SimpleGraph.Subgraph G} [(v : V) → Fintype ↑(SimpleGraph.Subgraph.neighborSet M v)] : SimpleGraph.Subgraph.IsPerfectMatching M ↔ ∀ (v : V), SimpleGraph.Subgraph.degree M v = 1

theorem SimpleGraph.Subgraph.IsPerfectMatching.even_card {V : Type u} {G : SimpleGraph V} {M : SimpleGraph.Subgraph G} [Fintype V] (h : SimpleGraph.Subgraph.IsPerfectMatching M) : Even (Fintype.card V)