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.

• SimpleGraph.IsMatchingFree means that a graph G has no perfect matchings.

• SimpleGraph.IsCycles means that a graph consists of cycles (including cycles of length 0, also known as isolated vertices)

• SimpleGraph.IsAlternating means that edges in a graph G are alternatingly included and not included in some other graph G'

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.lean)

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 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 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 G' : SimpleGraph V} {M : G.Subgraph} (h : M.IsMatching) (hGG' : G ≤ G') : (Subgraph.map (Hom.ofLE hGG') M).IsMatching

theorem SimpleGraph.Subgraph.IsMatching.eq_of_adj_left {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} {u v w : V} (hM : M.IsMatching) (huv : M.Adj u v) (huw : M.Adj u w) : v = w

theorem SimpleGraph.Subgraph.IsMatching.eq_of_adj_right {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} {u v w : V} (hM : M.IsMatching) (huw : M.Adj u w) (hvw : M.Adj v w) : u = v

theorem SimpleGraph.Subgraph.IsMatching.not_adj_left_of_ne {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} {u v w : V} (hM : M.IsMatching) (hvw : v ≠ w) (huv : M.Adj u v) : ¬M.Adj u w

theorem SimpleGraph.Subgraph.IsMatching.not_adj_right_of_ne {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} {u v w : V} (hM : M.IsMatching) (huv : u ≠ v) (huw : M.Adj u w) : ¬M.Adj v w

theorem SimpleGraph.Subgraph.IsMatching.sup {V : Type u_1} {G : SimpleGraph V} {M 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_3} {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 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) : (Subgraph.coeSubgraph M).IsMatching

theorem SimpleGraph.Subgraph.IsMatching.exists_of_disjoint_sets_of_equiv {V : Type u_1} {G : SimpleGraph V} {s t : Set V} (h : Disjoint s t) (f : ↑s ≃ ↑t) (hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)) : ∃ (M : G.Subgraph), M.verts = s ∪ t ∧ M.IsMatching

theorem SimpleGraph.Subgraph.IsMatching.map {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} {M : G.Subgraph} (f : G →g G') (hf : Function.Injective ⇑f) (hM : M.IsMatching) : (Subgraph.map f M).IsMatching

@[simp]

theorem SimpleGraph.Subgraph.Iso.isMatching_map {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} {M : G.Subgraph} (f : G ≃g G') : (Subgraph.map f.toHom M).IsMatching ↔ 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

@[simp]

theorem SimpleGraph.Subgraph.IsPerfectMatching.toSubgraph_iff {V : Type u_1} {G G' : SimpleGraph V} {M : G.Subgraph} (h : M.spanningCoe ≤ G') : (toSubgraph M.spanningCoe h).IsPerfectMatching ↔ M.IsPerfectMatching

theorem SimpleGraph.IsClique.even_iff_exists_isMatching {V : Type u_1} {G : SimpleGraph V} {u : Set V} (hc : G.IsClique u) (hu : u.Finite) : Even u.ncard ↔ ∃ (M : G.Subgraph), M.verts = u ∧ M.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} (hM : M.IsPerfectMatching) (c : ↑(⊤.deleteVerts u).coe.oddComponents) : ∃ 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 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

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

A graph G consists of a set of cycles, if each vertex is either isolated or connected to exactly two vertices. This is used to create new matchings by taking the symmDiff with cycles. The definition of symmDiff that makes sense is the one for SimpleGraph. The symmDiff for SimpleGraph.Subgraph deriving from the lattice structure also affects the vertices included, which we do not want in this case. This is why this property is defined for SimpleGraph, rather than SimpleGraph.Subgraph.

Equations

• G.IsCycles = ∀ ⦃v : V⦄, (G.neighborSet v).Nonempty → (G.neighborSet v).ncard = 2

theorem SimpleGraph.IsCycles.other_adj_of_adj {V : Type u_1} {G : SimpleGraph V} {v w : V} (h : G.IsCycles) (hadj : G.Adj v w) : ∃ (w' : V), w ≠ w' ∧ G.Adj v w'

Given a vertex with one edge in a graph of cycles this gives the other edge incident to the same vertex.

theorem SimpleGraph.IsCycles.existsUnique_ne_adj {V : Type u_1} {G : SimpleGraph V} {v w : V} (h : G.IsCycles) (hadj : G.Adj v w) : ∃! w' : V, w ≠ w' ∧ G.Adj v w'

theorem SimpleGraph.IsCycles.toSimpleGraph {V : Type u_1} {G : SimpleGraph V} (c : G.ConnectedComponent) (h : G.IsCycles) : c.toSimpleGraph.spanningCoe.IsCycles

@[deprecated SimpleGraph.IsCycles.toSimpleGraph (since := "2025-06-08")]

theorem SimpleGraph.IsCycles.induce_supp {V : Type u_1} {G : SimpleGraph V} (c : G.ConnectedComponent) (h : G.IsCycles) : c.toSimpleGraph.spanningCoe.IsCycles

Alias of SimpleGraph.IsCycles.toSimpleGraph.

theorem SimpleGraph.Walk.IsCycle.isCycles_spanningCoe_toSubgraph {V : Type u_1} {G : SimpleGraph V} {u : V} {p : G.Walk u u} (hpc : p.IsCycle) : p.toSubgraph.spanningCoe.IsCycles

theorem SimpleGraph.Walk.IsPath.isCycles_spanningCoe_toSubgraph_sup_edge {V : Type u_1} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : p.IsPath) (h : u ≠ v) (hs : s(v, u) ∉ p.edges) : (p.toSubgraph.spanningCoe ⊔ edge v u).IsCycles

theorem SimpleGraph.Walk.IsCycle.adj_toSubgraph_iff_of_isCycles {V : Type u_1} {G : SimpleGraph V} {v : V} [G.LocallyFinite] {u : V} {p : G.Walk u u} (hp : p.IsCycle) (hcyc : G.IsCycles) (hv : v ∈ p.toSubgraph.verts) (w : V) : p.toSubgraph.Adj v w ↔ G.Adj v w

theorem SimpleGraph.Subgraph.IsPerfectMatching.symmDiff_isCycles {V : Type u_1} {G G' : SimpleGraph V} {M : G.Subgraph} {M' : G'.Subgraph} (hM : M.IsPerfectMatching) (hM' : M'.IsPerfectMatching) : (symmDiff M.spanningCoe M'.spanningCoe).IsCycles

theorem SimpleGraph.IsCycles.snd_of_mem_support_of_isPath_of_adj {V : Type u_1} {G : SimpleGraph V} [Finite V] {v w w' : V} (hcyc : G.IsCycles) (p : G.Walk v w) (hw : w ≠ w') (hw' : w' ∈ p.support) (hp : p.IsPath) (hadj : G.Adj v w') : p.snd = w'

theorem SimpleGraph.IsCycles.reachable_sdiff_toSubgraph_spanningCoe {V : Type u_1} {G : SimpleGraph V} [Finite V] {v w : V} (hcyc : G.IsCycles) (p : G.Walk v w) (hp : p.IsPath) : (G \ p.toSubgraph.spanningCoe).Reachable w v

theorem SimpleGraph.IsCycles.reachable_deleteEdges {V : Type u_1} {G : SimpleGraph V} {v w : V} [Finite V] (hadj : G.Adj v w) (hcyc : G.IsCycles) : (G.deleteEdges {s(v, w)}).Reachable v w

theorem SimpleGraph.IsCycles.exists_cycle_toSubgraph_verts_eq_connectedComponentSupp {V : Type u_1} {G : SimpleGraph V} {v : V} [Finite V] {c : G.ConnectedComponent} (h : G.IsCycles) (hv : v ∈ c.supp) (hn : (G.neighborSet v).Nonempty) : ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp

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

A graph G is alternating with respect to some other graph G', if exactly every other edge in G is in G'. Note that the degree of each vertex needs to be at most 2 for this to be possible. This property is used to create new matchings using symmDiff. The definition of symmDiff that makes sense is the one for SimpleGraph. The symmDiff for SimpleGraph.Subgraph deriving from the lattice structure also affects the vertices included, which we do not want in this case. This is why this property, just like IsCycles, is defined for SimpleGraph rather than SimpleGraph.Subgraph.

Equations

• G.IsAlternating G' = ∀ ⦃v w w' : V⦄, w ≠ w' → G.Adj v w → G.Adj v w' → (G'.Adj v w ↔ ¬G'.Adj v w')

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

theorem SimpleGraph.IsAlternating.spanningCoe {V : Type u_1} {G G' : SimpleGraph V} (halt : G.IsAlternating G') (H : G.Subgraph) : H.spanningCoe.IsAlternating G'

theorem SimpleGraph.IsAlternating.sup_edge {V : Type u_1} {G G' : SimpleGraph V} {u x : V} (halt : G.IsAlternating G') (hnadj : ¬G'.Adj u x) (hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u') (hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u) : (G ⊔ edge u x).IsAlternating G'

theorem SimpleGraph.Subgraph.IsPerfectMatching.symmDiff_of_isAlternating {V : Type u_1} {G G' : SimpleGraph V} {M : G.Subgraph} (hM : M.IsPerfectMatching) (hG' : G'.IsAlternating M.spanningCoe) (hG'cyc : G'.IsCycles) : ⊤.IsPerfectMatching

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

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