Matchings in multigraphs

A matching in a multigraph is a set of actual edge identities with no loops and no two distinct members incident to a common vertex. Thus parallel edges remain distinct choices, but at most one of them can belong to a matching. A perfect matching is incident to every actual vertex.

The graph Graph.matchingSubgraph G M has exactly the edges selected by M and exactly their endpoints as vertices. It has no isolated vertices, and Graph.IsMatching is equivalent to this subgraph being loopless with exactly one incident edge at every one of its vertices. Perfectness is equivalently the assertion that this canonical subgraph is spanning. This connects the edge-set representation, convenient for deleting and partitioning multigraph edges, with the subgraph viewpoint used by Mathlib for simple-graph matchings.

A matching of a subgraph is a matching of the whole graph, and a perfect matching of a spanning subgraph is a perfect matching of the whole graph. Deleting a perfect matching lowers the incidence count of every actual vertex with finitely many incident edges by exactly one; this is the step that splits the edge set of a regular bipartite multigraph into perfect matchings.

Main definitions

• Graph.IsMatching G M: the actual edges in M form a matching.
• Graph.IsPerfectMatching G M: M is a matching incident to every actual vertex.
• Graph.matchingSubgraph G M: the subgraph containing precisely the selected edges and their endpoints.

Main results

• Graph.IsPerfectMatching.image_inclusion: a perfect matching of a spanning subgraph is a perfect matching of the whole graph.
• Graph.IsPerfectMatching.incidenceCount_deleteEdges_add_one: deleting a perfect matching lowers by one the incidence count of every actual vertex with finitely many incident edges.

def Graph.IsMatching {α : Type u} {β : Type v} (G : Graph α β) (M : Set ↑G.edgeSet) : Prop

A set of actual multigraph edges is a matching when it contains no loop and no two distinct edges in it have a common incident vertex.

def Graph.IsPerfectMatching {α : Type u} {β : Type v} (G : Graph α β) (M : Set ↑G.edgeSet) : Prop

A perfect matching is a matching incident to every actual vertex.

theorem Graph.isMatching_def {α : Type u} {β : Type v} {G : Graph α β} {M : Set ↑G.edgeSet} : G.IsMatching M ↔ (∀ e ∈ M, ∀ (x : α), ¬G.IsLoopAt (↑e) x) ∧ ∀ e ∈ M, ∀ f ∈ M, e ≠ f → ∀ (x : α), ¬(G.Inc (↑e) x ∧ G.Inc (↑f) x)

theorem Graph.isPerfectMatching_def {α : Type u} {β : Type v} {G : Graph α β} {M : Set ↑G.edgeSet} : G.IsPerfectMatching M ↔ G.IsMatching M ∧ ∀ (x : ↑G.vertexSet), ∃ e ∈ M, G.Inc ↑e ↑x

@[simp]

theorem Graph.isMatching_empty {α : Type u} {β : Type v} (G : Graph α β) : G.IsMatching ∅

The empty set of edges is a matching.

theorem Graph.IsMatching.mono {α : Type u} {β : Type v} {G : Graph α β} {M N : Set ↑G.edgeSet} (hM : G.IsMatching M) (hNM : N ⊆ M) : G.IsMatching N

A subset of a matching is a matching.

theorem Graph.IsMatching.not_isLoopAt {α : Type u} {β : Type v} {G : Graph α β} {M : Set ↑G.edgeSet} (hM : G.IsMatching M) {e : ↑G.edgeSet} (he : e ∈ M) (x : α) : ¬G.IsLoopAt (↑e) x

Every edge in a matching is a nonloop edge.

theorem Graph.IsMatching.eq_of_inc {α : Type u} {β : Type v} {G : Graph α β} {M : Set ↑G.edgeSet} (hM : G.IsMatching M) {e f : ↑G.edgeSet} (he : e ∈ M) (hf : f ∈ M) {x : α} (hex : G.Inc (↑e) x) (hfx : G.Inc (↑f) x) : e = f

Two edges of a matching incident to the same vertex are equal.

theorem Graph.IsMatching.existsUnique_of_exists_inc {α : Type u} {β : Type v} {G : Graph α β} {M : Set ↑G.edgeSet} (hM : G.IsMatching M) {x : α} (h : ∃ e ∈ M, G.Inc (↑e) x) : ∃! e : ↑G.edgeSet, e ∈ M ∧ G.Inc (↑e) x

At most one edge of a matching is incident to any given vertex.

theorem Graph.IsPerfectMatching.existsUnique_inc {α : Type u} {β : Type v} {G : Graph α β} {M : Set ↑G.edgeSet} (hM : G.IsPerfectMatching M) (x : ↑G.vertexSet) : ∃! e : ↑G.edgeSet, e ∈ M ∧ G.Inc ↑e ↑x

In a perfect matching, every actual vertex is incident to a unique selected edge.

theorem Graph.IsMatching.isPerfectMatching_iff {α : Type u} {β : Type v} {G : Graph α β} {M : Set ↑G.edgeSet} (hM : G.IsMatching M) : G.IsPerfectMatching M ↔ ∀ (x : ↑G.vertexSet), ∃! e : ↑G.edgeSet, e ∈ M ∧ G.Inc ↑e ↑x

A matching is perfect exactly when every actual vertex is incident to a unique selected edge.

def Graph.matchingSupport {α : Type u} {β : Type v} (G : Graph α β) (M : Set ↑G.edgeSet) : Set α

The vertices incident to a selected set of actual edges.

@[simp]

theorem Graph.mem_matchingSupport {α : Type u} {β : Type v} {G : Graph α β} {M : Set ↑G.edgeSet} {x : α} : x ∈ G.matchingSupport M ↔ ∃ e ∈ M, G.Inc (↑e) x

theorem Graph.matchingSupport_subset_vertexSet {α : Type u} {β : Type v} {G : Graph α β} {M : Set ↑G.edgeSet} : G.matchingSupport M ⊆ G.vertexSet

Every endpoint of a selected actual edge is an actual vertex.

theorem Graph.matchingSupport_mono {α : Type u} {β : Type v} {G : Graph α β} {M N : Set ↑G.edgeSet} (hMN : M ⊆ N) : G.matchingSupport M ⊆ G.matchingSupport N

Enlarging the selected edge set enlarges its vertex support.

@[simp]

theorem Graph.matchingSupport_empty {α : Type u} {β : Type v} (G : Graph α β) : G.matchingSupport ∅ = ∅

The empty edge set has empty vertex support.

def Graph.matchingSubgraph {α : Type u} {β : Type v} (G : Graph α β) (M : Set ↑G.edgeSet) : Graph α β

The subgraph whose edges are exactly M and whose vertices are exactly their endpoints.

@[simp]

theorem Graph.vertexSet_matchingSubgraph {α : Type u} {β : Type v} {G : Graph α β} {M : Set ↑G.edgeSet} : (G.matchingSubgraph M).vertexSet = G.matchingSupport M

@[simp]

theorem Graph.edgeSet_matchingSubgraph {α : Type u} {β : Type v} {G : Graph α β} {M : Set ↑G.edgeSet} : (G.matchingSubgraph M).edgeSet = Subtype.val '' M

@[simp]

theorem Graph.matchingSubgraph_isLink {α : Type u} {β : Type v} {G : Graph α β} {M : Set ↑G.edgeSet} {e : β} {x y : α} : (G.matchingSubgraph M).IsLink e x y ↔ ∃ (he : e ∈ G.edgeSet), ⟨e, he⟩ ∈ M ∧ G.IsLink e x y

@[simp]

theorem Graph.matchingSubgraph_inc {α : Type u} {β : Type v} {G : Graph α β} {M : Set ↑G.edgeSet} {e : β} {x : α} : (G.matchingSubgraph M).Inc e x ↔ ∃ (he : e ∈ G.edgeSet), ⟨e, he⟩ ∈ M ∧ G.Inc e x

Incidence in the canonical subgraph is incidence in G by a selected edge.

@[simp]

theorem Graph.matchingSubgraph_isLoopAt {α : Type u} {β : Type v} {G : Graph α β} {M : Set ↑G.edgeSet} {e : β} {x : α} : (G.matchingSubgraph M).IsLoopAt e x ↔ ∃ (he : e ∈ G.edgeSet), ⟨e, he⟩ ∈ M ∧ G.IsLoopAt e x

A loop of the canonical subgraph is precisely a selected loop of G.

theorem Graph.matchingSubgraph_injective {α : Type u} {β : Type v} (G : Graph α β) : Function.Injective G.matchingSubgraph

The canonical subgraph construction remembers the selected set of actual edges.

theorem Graph.matchingSubgraph_le {α : Type u} {β : Type v} (G : Graph α β) (M : Set ↑G.edgeSet) : G.matchingSubgraph M ≤ G

The canonical graph of selected edges is a subgraph of the original graph.

theorem Graph.matchingSubgraph_eq_of_le_of_exists_inc {α : Type u} {β : Type v} {G H : Graph α β} (hHG : H ≤ G) (hH : ∀ x ∈ H.vertexSet, ∃ (e : β), H.Inc e x) : G.matchingSubgraph {e : ↑G.edgeSet | ↑e ∈ H.edgeSet} = H

A subgraph with no isolated vertices is reconstructed from its set of actual edges.

theorem Graph.matchingSubgraph_mono {α : Type u} {β : Type v} {G : Graph α β} {M N : Set ↑G.edgeSet} (hMN : M ⊆ N) : G.matchingSubgraph M ≤ G.matchingSubgraph N

Enlarging the selected edge set enlarges its canonical subgraph.

@[simp]

theorem Graph.matchingSubgraph_empty {α : Type u} {β : Type v} (G : Graph α β) : G.matchingSubgraph ∅ = ⊥

Selecting no edges gives the empty graph.

theorem Graph.matchingSubgraph_exists_inc {α : Type u} {β : Type v} {G : Graph α β} {M : Set ↑G.edgeSet} {x : α} (hx : x ∈ (G.matchingSubgraph M).vertexSet) : ∃ (e : β), (G.matchingSubgraph M).Inc e x

Every vertex of the canonical graph of selected edges is incident to one of its edges.

theorem Graph.IsMatching.matchingSubgraph_loopless {α : Type u} {β : Type v} {G : Graph α β} {M : Set ↑G.edgeSet} (hM : G.IsMatching M) : (G.matchingSubgraph M).Loopless

A matching gives a loopless canonical subgraph.

theorem Graph.IsMatching.matchingSubgraph_existsUnique_inc {α : Type u} {β : Type v} {G : Graph α β} {M : Set ↑G.edgeSet} (hM : G.IsMatching M) {x : α} (hx : x ∈ (G.matchingSubgraph M).vertexSet) : ∃! e : β, (G.matchingSubgraph M).Inc e x

In the canonical subgraph of a matching, every vertex has a unique incident edge.

theorem Graph.isMatching_iff_matchingSubgraph {α : Type u} {β : Type v} {G : Graph α β} {M : Set ↑G.edgeSet} : G.IsMatching M ↔ (G.matchingSubgraph M).Loopless ∧ ∀ x ∈ (G.matchingSubgraph M).vertexSet, ∃! e : β, (G.matchingSubgraph M).Inc e x

The edge-set definition of a matching is equivalent to saying that its canonical subgraph is loopless and has exactly one incident edge at every vertex.

theorem Graph.IsMatching.isPerfectMatching_iff_matchingSubgraph_spanning {α : Type u} {β : Type v} {G : Graph α β} {M : Set ↑G.edgeSet} (hM : G.IsMatching M) : G.IsPerfectMatching M ↔ G.matchingSubgraph M ≤s G

A matching is perfect exactly when its canonical subgraph is spanning.

@[simp]

theorem Graph.isPerfectMatching_empty_iff {α : Type u} {β : Type v} {G : Graph α β} : G.IsPerfectMatching ∅ ↔ G.vertexSet = ∅

The empty matching is perfect exactly when the graph has no actual vertices.

theorem Graph.isPerfectMatching_univ_banana_singleton {α : Type u} {β : Type v} {u v : α} {e : β} (huv : u ≠ v) : (banana u v {e}).IsPerfectMatching Set.univ

The unique edge of a two-vertex single-edge multigraph is a perfect matching.

Subgraphs and edge deletion

theorem Graph.IsMatching.image_inclusion {α : Type u} {β : Type v} {G H : Graph α β} (hHG : H ≤ G) {M : Set ↑H.edgeSet} (hM : H.IsMatching M) : G.IsMatching (Set.inclusion ⋯ '' M)

A matching of a subgraph is a matching of the whole graph.

theorem Graph.IsPerfectMatching.image_inclusion {α : Type u} {β : Type v} {G H : Graph α β} (hHG : H ≤s G) {M : Set ↑H.edgeSet} (hM : H.IsPerfectMatching M) : G.IsPerfectMatching (Set.inclusion ⋯ '' M)

A perfect matching of a spanning subgraph is a perfect matching of the whole graph.

theorem Graph.IsPerfectMatching.ncard_incidenceSet_inter {α : Type u} {β : Type v} {G : Graph α β} {M : Set ↑G.edgeSet} (hM : G.IsPerfectMatching M) (x : ↑G.vertexSet) : (incidenceSet ↑x ∩ Subtype.val '' M).ncard = 1

Exactly one edge of a perfect matching is incident with each actual vertex.

theorem Graph.IsPerfectMatching.incidenceCount_deleteEdges_add_one {α : Type u} {β : Type v} {G : Graph α β} {M : Set ↑G.edgeSet} (hM : G.IsPerfectMatching M) (x : ↑G.vertexSet) (hfin : (incidenceSet ↑x).Finite) : (G.deleteEdges (Subtype.val '' M)).incidenceCount ↑x + 1 = G.incidenceCount ↑x

Deleting a perfect matching lowers the incidence count of every actual vertex with finitely many incident edges by exactly one.