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.

• 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 Mathlib.Combinatorics.Hall.Basic)

def SimpleGraph.Subgraph.IsMatching {V : Type u_1} {G : SimpleGraph 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.IsMatching = ∀ ⦃v : V⦄, v ∈ M.verts → ∃! w : V, M.Adj v w

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

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

Equations

• h.toEdge v = ⟨s(↑v, Exists.choose ⋯), ⋯⟩

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

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

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

theorem SimpleGraph.Subgraph.IsMatching.map_ofLE {V : Type u_1} {G : SimpleGraph V} {G' : SimpleGraph V} {M : G.Subgraph} (h : M.IsMatching) (hGG' : G ≤ G') : (SimpleGraph.Subgraph.map (SimpleGraph.Hom.ofLE hGG') M).IsMatching

theorem SimpleGraph.Subgraph.IsMatching.sup {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} {M' : G.Subgraph} (hM : M.IsMatching) (hM' : M'.IsMatching) (hd : Disjoint M.support M'.support) : (M ⊔ M').IsMatching

theorem SimpleGraph.Subgraph.IsMatching.iSup {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} {f : ι → G.Subgraph} (hM : ∀ (i : ι), (f i).IsMatching) (hd : Pairwise fun (i j : ι) => Disjoint (f i).support (f j).support) : (⨆ (i : ι), f i).IsMatching

theorem SimpleGraph.Subgraph.IsMatching.subgraphOfAdj {V : Type u_1} {G : SimpleGraph V} {v : V} {w : V} (h : G.Adj v w) : (G.subgraphOfAdj h).IsMatching

theorem SimpleGraph.Subgraph.IsMatching.coeSubgraph {V : Type u_1} {G : SimpleGraph V} {G' : G.Subgraph} {M : G'.coe.Subgraph} (hM : M.IsMatching) : (SimpleGraph.Subgraph.coeSubgraph M).IsMatching

def SimpleGraph.Subgraph.IsPerfectMatching {V : Type u_1} {G : SimpleGraph 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.IsPerfectMatching = (M.IsMatching ∧ M.IsSpanning)

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

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

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

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

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

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

theorem SimpleGraph.Subgraph.IsMatching.induce_connectedComponent {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} (h : M.IsMatching) (c : G.ConnectedComponent) : (M.induce (M.verts ∩ c.supp)).IsMatching

theorem SimpleGraph.Subgraph.IsPerfectMatching.induce_connectedComponent_isMatching {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} (h : M.IsPerfectMatching) (c : G.ConnectedComponent) : (M.induce c.supp).IsMatching

theorem SimpleGraph.ConnectedComponent.even_card_of_isPerfectMatching {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} [Fintype V] [DecidableEq V] [DecidableRel G.Adj] (c : G.ConnectedComponent) (hM : M.IsPerfectMatching) : Even (Fintype.card ↑c.supp)

theorem SimpleGraph.ConnectedComponent.odd_matches_node_outside {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} [Finite V] {u : Set V} {c : (⊤.deleteVerts u).coe.ConnectedComponent} (hM : M.IsPerfectMatching) (codd : Odd (Nat.card ↑c.supp)) : ∃ w ∈ u, ∃ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w ∧ v ∈ c.supp

def SimpleGraph.IsMatchingFree {V : Type u_1} (G : SimpleGraph V) : Prop

A graph is matching free if it has no perfect matching. It does not make much sense to consider a graph being free of just matchings, because any non-trivial graph has those.

Equations

• G.IsMatchingFree = ∀ (M : G.Subgraph), ¬M.IsPerfectMatching

theorem SimpleGraph.IsMatchingFree.mono {V : Type u_1} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G ≤ G') (hmf : G'.IsMatchingFree) : G.IsMatchingFree

theorem SimpleGraph.exists_maximal_isMatchingFree {V : Type u_1} {G : SimpleGraph V} [Finite V] (h : G.IsMatchingFree) : ∃ (Gmax : SimpleGraph V), G ≤ Gmax ∧ Gmax.IsMatchingFree ∧ ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching