Multiset capacitated matchings and Kőnig's theorem

Let G : Graph α β be a multigraph with finitely many actual edges and let b v : ℕ be a capacity on every actual vertex. A multiset capacitated matching assigns a multiplicity x e : ℕ to every actual edge so that, at every actual vertex v, the edges incident with v have total multiplicity at most b v; its size is ∑ e, x e. An edge may be used repeatedly, whether or not the graph has parallel edges, and a loop at v counts once towards the usage of v. A vertex cover is a set of actual vertices meeting every edge, and the weight of a finite cover C is ∑ v ∈ C, b v. At b = 1 a multiset capacitated matching uses every edge at most once and no two edges with a common end, so it is an ordinary matching, and the weight of a cover is its size.

This file proves the multiset capacitated form of Kőnig's theorem for bipartite multigraphs: some multiset capacitated matching has size equal to the weight of some vertex cover. Every multiset capacitated matching has size at most the weight of every vertex cover, so this matching is then largest and this cover of least weight. Weak duality holds in every multigraph, with loops; only attainment needs the bipartition. Zero capacities, isolated vertices, empty sides and the empty graph are all allowed.

Main definitions

• Graph.IsCapacitatedMatching G b x: the edge multiplicities x form a multiset capacitated matching for the vertex capacities b.
• Graph.matchingEquivUnitCapacitated: in a loopless multigraph, ordinary matchings correspond to unit-capacity multiset matchings through their characteristic functions.

Main results

• Graph.IsCapacitatedMatching.sum_le_sum_of_isVertexCover: weak duality, the size of a multiset capacitated matching is at most the weight of any vertex cover.
• Graph.IsCapacitatedMatching.isMatching: in a loopless multigraph, the edges used by a multiset capacitated matching for unit capacities form a matching, and a perfect one when every actual vertex is used exactly once (Graph.isPerfectMatching_of_sum_incidentEdges_eq_one).
• Graph.IsBipartition.exists_isCapacitatedMatching_isVertexCover_sum_eq: Kőnig's theorem for multiset capacitated matchings in bipartite multigraphs, in witness form.

Implementation notes

Attainment is the vertex-capacitated set-to-set form of Menger's theorem (TauCeti.exists_paths_setSeparator_sum_eq) for the arrow family on the actual vertices with one arrow for every actual edge, from its end in L to its end in R, between the vertex sets L and R and with the capacities b. Every member of a packing joins a vertex of L to a vertex of R, so it traverses an arrow, and the edge of such an arrow has both ends among the vertices of the member. Counting the members through each edge therefore gives a multiset capacitated matching of size the number of members. A separator meets every one-arrow walk, so it is a vertex cover.

References

• D. Kőnig, Gráfok és mátrixok, Mat. Fiz. Lapok 38 (1931).
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer, 2003, Section 21.1.

Multiset capacitated matchings

def Graph.IsCapacitatedMatching {α : Type u} {β : Type v} (G : Graph α β) [Fintype ↑G.edgeSet] (b : ↑G.vertexSet → ℕ) (x : ↑G.edgeSet → ℕ) : Prop

The edge multiplicities x form a multiset capacitated matching for the vertex capacities b: at every actual vertex v, the actual edges incident with v have total multiplicity at most b v. A loop at v counts once towards this total.

theorem Graph.isCapacitatedMatching_def {α : Type u} {β : Type v} {G : Graph α β} [Fintype ↑G.edgeSet] {b : ↑G.vertexSet → ℕ} {x : ↑G.edgeSet → ℕ} : G.IsCapacitatedMatching b x ↔ ∀ (v : ↑G.vertexSet), ∑ e ∈ G.incidentEdges {v}, x e ≤ b v

@[simp]

theorem Graph.isCapacitatedMatching_zero {α : Type u} {β : Type v} {G : Graph α β} [Fintype ↑G.edgeSet] {b : ↑G.vertexSet → ℕ} : G.IsCapacitatedMatching b 0

Using no edge at all is a multiset capacitated matching.

Ordinary matchings as unit-capacity matchings

theorem Graph.isMatching_iff_isCapacitatedMatching_indicator {α : Type u} {β : Type v} {G : Graph α β} [Fintype ↑G.edgeSet] [G.Loopless] (M : Set ↑G.edgeSet) : G.IsMatching M ↔ G.IsCapacitatedMatching 1 (M.indicator 1)

In a loopless multigraph, ordinary matchings are exactly unit-capacity multiset matchings whose multiplicities are the characteristic function of the selected edges.

theorem Graph.IsCapacitatedMatching.apply_le_one {α : Type u} {β : Type v} {G : Graph α β} [Fintype ↑G.edgeSet] {x : ↑G.edgeSet → ℕ} (hx : G.IsCapacitatedMatching 1 x) (e : ↑G.edgeSet) : x e ≤ 1

In a unit-capacity multiset matching, every actual edge has multiplicity at most one.

theorem Graph.IsCapacitatedMatching.indicator_setOf_eq_one {α : Type u} {β : Type v} {G : Graph α β} [Fintype ↑G.edgeSet] {x : ↑G.edgeSet → ℕ} (hx : G.IsCapacitatedMatching 1 x) : {e : ↑G.edgeSet | x e = 1}.indicator 1 = x

The indicator of the edges of multiplicity one in a unit-capacity multiset matching recovers its multiplicities.

theorem Graph.IsCapacitatedMatching.isMatching_setOf_eq_one {α : Type u} {β : Type v} {G : Graph α β} [Fintype ↑G.edgeSet] {x : ↑G.edgeSet → ℕ} [G.Loopless] (hx : G.IsCapacitatedMatching 1 x) : G.IsMatching {e : ↑G.edgeSet | x e = 1}

A unit-capacity multiset matching on a loopless graph determines an ordinary matching by taking the edges of multiplicity one.

noncomputable def Graph.matchingEquivUnitCapacitated {α : Type u} {β : Type v} {G : Graph α β} [Fintype ↑G.edgeSet] [G.Loopless] : { M : Set ↑G.edgeSet // G.IsMatching M } ≃ { x : ↑G.edgeSet → ℕ // G.IsCapacitatedMatching 1 x }

Ordinary matchings in a finite loopless multigraph are equivalent to unit-capacity multiset matchings. The equivalence retains each selected edge identity as multiplicity one.

@[simp]

theorem Graph.matchingEquivUnitCapacitated_apply {α : Type u} {β : Type v} {G : Graph α β} [Fintype ↑G.edgeSet] [G.Loopless] (M : { M : Set ↑G.edgeSet // G.IsMatching M }) : ↑(matchingEquivUnitCapacitated M) = (↑M).indicator 1

@[simp]

theorem Graph.matchingEquivUnitCapacitated_symm_apply {α : Type u} {β : Type v} {G : Graph α β} [Fintype ↑G.edgeSet] [G.Loopless] (x : { x : ↑G.edgeSet → ℕ // G.IsCapacitatedMatching 1 x }) : ↑(matchingEquivUnitCapacitated.symm x) = {e : ↑G.edgeSet | ↑x e = 1}

theorem Graph.IsCapacitatedMatching.mono {α : Type u} {β : Type v} {G : Graph α β} [Fintype ↑G.edgeSet] {b b' : ↑G.vertexSet → ℕ} {x y : ↑G.edgeSet → ℕ} (hx : G.IsCapacitatedMatching b x) (hyx : y ≤ x) (hb : b ≤ b') : G.IsCapacitatedMatching b' y

Lowering the multiplicities or raising the capacities preserves multiset capacitated matchings. In particular, restricting a multiset capacitated matching to a set of edges gives one.

theorem Graph.IsCapacitatedMatching.add {α : Type u} {β : Type v} {G : Graph α β} [Fintype ↑G.edgeSet] {b b' : ↑G.vertexSet → ℕ} {x y : ↑G.edgeSet → ℕ} (hx : G.IsCapacitatedMatching b x) (hy : G.IsCapacitatedMatching b' y) : G.IsCapacitatedMatching (b + b') (x + y)

The sum of two multiset capacitated matchings is one for the sum of their capacities.

theorem Graph.IsCapacitatedMatching.sum_eq_sum_left_iff {α : Type u} {β : Type v} {G : Graph α β} [Fintype ↑G.edgeSet] {b : ↑G.vertexSet → ℕ} {x : ↑G.edgeSet → ℕ} (hx : G.IsCapacitatedMatching b x) {L R : Finset ↑G.vertexSet} (hLR : G.IsBipartition L R) : ∑ e : ↑G.edgeSet, x e = ∑ v ∈ L, b v ↔ ∀ v ∈ L, ∑ e ∈ G.incidentEdges {v}, x e = b v

A multiset capacitated matching in a bipartite multigraph has size b(L) exactly when it saturates every vertex of L.

theorem Graph.IsCapacitatedMatching.sum_le_sum_of_isVertexCover {α : Type u} {β : Type v} {G : Graph α β} [Fintype ↑G.edgeSet] {b : ↑G.vertexSet → ℕ} {x : ↑G.edgeSet → ℕ} (hx : G.IsCapacitatedMatching b x) {C : Finset ↑G.vertexSet} (hC : G.IsVertexCover ↑C) : ∑ e : ↑G.edgeSet, x e ≤ ∑ v ∈ C, b v

Weak duality for multiset capacitated matchings. The size of a multiset capacitated matching is at most the weight of any vertex cover.

theorem Graph.IsCapacitatedMatching.isMatching {α : Type u} {β : Type v} {G : Graph α β} [Fintype ↑G.edgeSet] {x : ↑G.edgeSet → ℕ} [G.Loopless] (hx : G.IsCapacitatedMatching 1 x) : G.IsMatching {e : ↑G.edgeSet | x e ≠ 0}

In a loopless multigraph, the edges used by a multiset capacitated matching for the unit capacities form a matching.

theorem Graph.isPerfectMatching_of_sum_incidentEdges_eq_one {α : Type u} {β : Type v} {G : Graph α β} [Fintype ↑G.edgeSet] {x : ↑G.edgeSet → ℕ} [G.Loopless] (hx : ∀ (v : ↑G.vertexSet), ∑ e ∈ G.incidentEdges {v}, x e = 1) : G.IsPerfectMatching {e : ↑G.edgeSet | x e ≠ 0}

In a loopless multigraph, if edge multiplicities x use every actual vertex exactly once, then the edges they use form a perfect matching.

Unit capacities and ordinary matchings

theorem Graph.IsMatching.isCapacitatedMatching_indicator {α : Type u} {β : Type v} {G : Graph α β} [Fintype ↑G.edgeSet] {M : Finset ↑G.edgeSet} (hM : G.IsMatching ↑M) : G.IsCapacitatedMatching (fun (x : ↑G.vertexSet) => 1) ((↑M).indicator fun (x : ↑G.edgeSet) => 1)

An ordinary matching, represented by a finite set of actual edges, is a multiset capacitated matching for unit vertex capacities when its selected edges have multiplicity one.

theorem Graph.IsCapacitatedMatching.sum_eq_card_support {α : Type u} {β : Type v} {G : Graph α β} [Fintype ↑G.edgeSet] {x : ↑G.edgeSet → ℕ} (hx : G.IsCapacitatedMatching (fun (x : ↑G.vertexSet) => 1) x) : ∑ e : ↑G.edgeSet, x e = {e : ↑G.edgeSet | x e ≠ 0}.card

The sum of the multiplicities in a unit-capacitated matching is the cardinality of its positive support.

theorem Graph.IsCapacitatedMatching.support_isMatching {α : Type u} {β : Type v} {G : Graph α β} [Fintype ↑G.edgeSet] {x : ↑G.edgeSet → ℕ} (hx : G.IsCapacitatedMatching (fun (x : ↑G.vertexSet) => 1) x) (hG : G.Loopless) : G.IsMatching {e : ↑G.edgeSet | x e ≠ 0}

In a loopless graph, the positive support of a unit-capacitated matching is an ordinary matching.

theorem Graph.IsCapacitatedMatching.supportFinset_isMatching {α : Type u} {β : Type v} {G : Graph α β} [Fintype ↑G.edgeSet] {x : ↑G.edgeSet → ℕ} (hx : G.IsCapacitatedMatching (fun (x : ↑G.vertexSet) => 1) x) (hG : G.Loopless) : G.IsMatching ↑{e : ↑G.edgeSet | x e ≠ 0}

The finite positive support of a unit-capacitated matching in a loopless graph is an ordinary matching.

Kőnig's theorem

theorem Graph.IsBipartition.exists_isCapacitatedMatching_isVertexCover_sum_eq {α : Type u} {β : Type v} {G : Graph α β} [Fintype ↑G.edgeSet] {L R : Finset ↑G.vertexSet} (hLR : G.IsBipartition L R) (b : ↑G.vertexSet → ℕ) : ∃ (x : ↑G.edgeSet → ℕ) (C : Finset ↑G.vertexSet), G.IsCapacitatedMatching b x ∧ G.IsVertexCover ↑C ∧ ∑ e : ↑G.edgeSet, x e = ∑ v ∈ C, b v

Kőnig's theorem for multiset capacitated matchings. Let L and R form a bipartition of a multigraph with finitely many actual edges, and let b v : ℕ be a capacity on every actual vertex. Some multiset capacitated matching x and some vertex cover C satisfy ∑ e, x e = ∑ v ∈ C, b v. By Graph.IsCapacitatedMatching.sum_le_sum_of_isVertexCover, the matching is then largest and the cover of least weight.