Menger's theorem for vertex-disjoint paths in multigraphs

Let G : Graph α β be a multigraph and let s ≠ t be points that no edge of G joins. Two walks of G from s to t are internally disjoint when they share no vertex other than s and t. A vertex separator is a set X of actual vertices, avoiding s and t, such that s and t are not reachable in G.deleteVerts X. With a capacity c v : ℕ on every vertex, a packing is a finite indexed family of s–t paths, repetitions allowed, in which every vertex v other than s and t lies on at most c v members, and the weight of a vertex separator X is ∑ v ∈ X, c v.

This file proves the local vertex form of Menger's theorem for multigraphs with finitely many actual vertices: the largest number of pairwise internally disjoint s–t paths equals the least size of a vertex separator. More generally, the largest packing has as many members as the least weight of a vertex separator. The edge set may be infinite: loops and parallel edges change neither side, since the statements concern only the vertices that walks visit. Weak duality needs no finiteness: each member of a packing visits a vertex of the separator other than s and t. Without the hypothesis that no edge joins s and t, no vertex separator exists, and a single edge from s to t could be repeated arbitrarily often in a packing.

Main results

• Graph.card_le_sum_of_not_reachable_deleteVerts: weak duality for vertex-capacitated packings.

• Graph.exists_paths_vertexSeparator_sum_eq: vertex-capacitated Menger's theorem, a packing and a vertex separator of equal size and weight.

• Graph.card_le_encard_of_not_reachable_deleteVerts: weak duality for families of pairwise internally disjoint walks.

• Graph.exists_paths_vertexSeparator_card_eq: Menger's theorem for internally vertex-disjoint paths in a multigraph, in witness form.

• Graph.forall_reachable_deleteVerts_iff_exists_paths: its predicate form: s and t stay reachable after deleting any fewer than k vertices other than s and t exactly when there are k pairwise internally disjoint s–t paths.

• Graph.isVertexReachable_iff_exists_paths: the same equivalence stated through the vertex-reachability predicate of the underlying simple graph, for arbitrary actual vertices s and t.

• Graph.isVertexConnected_iff_forall_exists_paths: the global form of Menger's theorem: a multigraph with finitely many actual vertices, more than k of them, is k-vertex-connected exactly when every two distinct actual vertices, adjacent or not, are joined by k distinct internally disjoint paths.

Implementation notes

Attainment is transported from the corresponding theorems for directed walks of an arrow family (TauCeti.exists_paths_vertexSeparator_sum_eq and TauCeti.exists_paths_vertexSeparator_card_eq) applied to the bidirected arrow family Graph.BidirectedHom G on the actual vertices of G. Its directed walks are the walks of G with the same vertex sequences (Graph.Walk.bidirectedEquiv), it has no arrow from s to t exactly when no edge joins them, and reachability avoiding a vertex set is reachability after deleting it (Graph.reachableAvoiding_bidirectedHom_iff). The directed theorems allow infinite arrow types, so no finiteness of the edge set is needed.

The global form is inherited from SimpleGraph.isVertexConnected_iff_forall_exists_paths for the underlying simple graph G.toSimpleGraph, which defines vertex connectivity. Its paths are lifted to G by choosing an actual edge for each adjacency (SimpleGraph.Walk.liftToGraph); the lift keeps vertex sequences, so it is injective and preserves internal disjointness. For adjacent vertices this avoids counting the possibly infinitely many parallel edges joining them.

References

• K. Menger, Zur allgemeinen Kurventheorie, Fund. Math. 10 (1927).
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer, 2003, Section 9.1.

@[simp]

theorem SimpleGraph.Walk.internallyDisjoint_liftToGraph_iff {α : Type u} {β : Type v} {G : Graph α β} {s t : ↑G.vertexSet} {p q : G.toSimpleGraph.Walk s t} : p.liftToGraph.InternallyDisjoint q.liftToGraph ↔ p.InternallyDisjoint q

Lifting walks of the underlying simple graph preserves and reflects internal disjointness, since the lift keeps every vertex sequence.

Weak duality

theorem Graph.card_le_sum_of_not_reachable_deleteVerts {α : Type u} {β : Type v} {G : Graph α β} {s t : α} [DecidableEq α] {ι : Type u_1} [Fintype ι] {P : ι → G.Walk s t} {c : α → ℕ} (hP : ∀ (v : α), v ≠ s → v ≠ t → {i : ι | v ∈ (P i).support}.card ≤ c v) (hs : s ∈ G.vertexSet) {X : Finset α} (hsX : s ∉ X) (htX : t ∉ X) (hX : ¬(G.deleteVerts ↑X).Reachable s t) : Fintype.card ι ≤ ∑ v ∈ X, c v

Weak duality for vertex-capacitated packings. A family of s–t walks, from an actual vertex s, in which every vertex v other than s and t lies on at most c v members has at most ∑ v ∈ X, c v members, for every set X of vertices avoiding s and t whose deletion leaves s and t unreachable.

theorem Graph.card_le_encard_of_not_reachable_deleteVerts {α : Type u} {β : Type v} {G : Graph α β} {s t : α} {ι : Type u_1} {P : ι → G.Walk s t} (hP : Pairwise fun (i j : ι) => (P i).InternallyDisjoint (P j)) (hs : s ∈ G.vertexSet) {X : Set α} (hsX : s ∉ X) (htX : t ∉ X) (hX : ¬(G.deleteVerts X).Reachable s t) : ENat.card ι ≤ X.encard

Weak duality for internally vertex-disjoint walks. A family of s–t walks, from an actual vertex s, pairwise sharing no vertex other than s and t has at most as many members as any set of vertices avoiding s and t whose deletion leaves s and t unreachable.

Attainment

theorem Graph.exists_paths_vertexSeparator_sum_eq {α : Type u} {β : Type v} {G : Graph α β} {s t : α} [Finite ↑G.vertexSet] [DecidableEq α] (c : α → ℕ) (hst : s ≠ t) (hadj : ¬G.Adj s t) : ∃ (k : ℕ) (P : Fin k → G.Walk s t) (X : Finset α), (∀ (i : Fin k), (P i).IsPath) ∧ (∀ (v : α), v ≠ s → v ≠ t → {i : Fin k | v ∈ (P i).support}.card ≤ c v) ∧ ↑X ⊆ G.vertexSet ∧ s ∉ X ∧ t ∉ X ∧ ¬(G.deleteVerts ↑X).Reachable s t ∧ ∑ v ∈ X, c v = k

Vertex-capacitated Menger's theorem for multigraphs. Let s ≠ t be points of a multigraph with finitely many actual vertices, joined by no edge, and let c v be a capacity on every vertex. Some family of k paths from s to t, in which every vertex v other than s and t lies on at most c v members, and some set X of actual vertices avoiding s and t, whose deletion leaves s and t unreachable, satisfy ∑ v ∈ X, c v = k. By Graph.card_le_sum_of_not_reachable_deleteVerts, the family is then largest and the separator of least weight.

theorem Graph.exists_paths_vertexSeparator_card_eq {α : Type u} {β : Type v} {G : Graph α β} {s t : α} [Finite ↑G.vertexSet] (hst : s ≠ t) (hadj : ¬G.Adj s t) : ∃ (k : ℕ) (P : Fin k → G.Walk s t) (X : Finset α), Function.Injective P ∧ (∀ (i : Fin k), (P i).IsPath) ∧ (Pairwise fun (i j : Fin k) => (P i).InternallyDisjoint (P j)) ∧ ↑X ⊆ G.vertexSet ∧ s ∉ X ∧ t ∉ X ∧ ¬(G.deleteVerts ↑X).Reachable s t ∧ X.card = k

Menger's theorem for internally vertex-disjoint paths in a multigraph. Let s ≠ t be points of a multigraph with finitely many actual vertices, joined by no edge. Some family of k distinct paths from s to t, pairwise sharing no vertex other than s and t, and some set of k actual vertices avoiding s and t, whose deletion leaves s and t unreachable, exist. By Graph.card_le_encard_of_not_reachable_deleteVerts, the family is then largest and the separator smallest.

theorem Graph.forall_reachable_deleteVerts_iff_exists_paths {α : Type u} {β : Type v} {G : Graph α β} {s t : α} [Finite ↑G.vertexSet] (hst : s ≠ t) (hadj : ¬G.Adj s t) (k : ℕ) : (∀ (X : Finset α), s ∉ X → t ∉ X → X.card < k → (G.deleteVerts ↑X).Reachable s t) ↔ ∃ (P : Fin k → G.Walk s t), (∀ (i : Fin k), (P i).IsPath) ∧ Pairwise fun (i j : Fin k) => (P i).InternallyDisjoint (P j)

Menger's theorem for internally vertex-disjoint paths in a multigraph, predicate form. Let s ≠ t be points of a multigraph with finitely many actual vertices, joined by no edge. Then s and t stay reachable after deleting any fewer than k vertices other than s and t exactly when there are k paths from s to t pairwise sharing no vertex other than s and t.

theorem Graph.isVertexReachable_of_pairwise_internallyDisjoint {α : Type u} {β : Type v} {G : Graph α β} {s t : ↑G.vertexSet} {n : ℕ} {P : Fin n → G.Walk ↑s ↑t} (hP : Pairwise fun (i j : Fin n) => (P i).InternallyDisjoint (P j)) : G.IsVertexReachable n s t

Weak duality for vertex reachability. Internally vertex-disjoint native walks make their actual endpoints vertex-reachable, without finiteness or nonadjacency assumptions.

theorem Graph.isVertexReachable_iff_exists_paths {α : Type u} {β : Type v} {G : Graph α β} [Finite ↑G.vertexSet] {s t : ↑G.vertexSet} (k : ℕ) : G.IsVertexReachable k s t ↔ ∃ (P : Fin k → G.Walk ↑s ↑t), (∀ (i : Fin k), (P i).IsPath) ∧ Pairwise fun (i j : Fin k) => (P i).InternallyDisjoint (P j)

Menger's theorem for the vertex-reachability predicate. For actual vertices s and t of a multigraph with finitely many actual vertices, k-vertex-reachability is equivalent to the existence of k internally vertex-disjoint native paths. For s = t, and for adjacent s and t, both sides hold. No finite-edge assumption is needed.

The global form

theorem Graph.isVertexConnected_iff_forall_exists_paths {α : Type u} {β : Type v} {G : Graph α β} [Finite ↑G.vertexSet] {k : ℕ} (hk : k < Nat.card ↑G.vertexSet) : G.IsVertexConnected k ↔ ∀ (s t : ↑G.vertexSet), s ≠ t → ∃ (P : Fin k → G.Walk ↑s ↑t), Function.Injective P ∧ (∀ (i : Fin k), (P i).IsPath) ∧ Pairwise fun (i j : Fin k) => (P i).InternallyDisjoint (P j)

The global form of Menger's theorem for multigraphs. A multigraph with finitely many actual vertices, more than k of them, is k-vertex-connected exactly when every two distinct actual vertices s and t, adjacent or not, are joined by k distinct paths pairwise sharing no vertex other than s and t. The edge set may be infinite.