Menger's theorem for vertex-disjoint paths in simple graphs

Let G be a simple graph on a finite vertex type V. This file proves the vertex forms of Menger's theorem for G, with path witnesses in SimpleGraph.Walk and separators given by deleting vertices.

• Local form. For distinct nonadjacent vertices s and t, the largest number of s–t paths pairwise sharing no vertex other than s and t equals the least number of vertices, other than s and t, whose deletion separates s from t. Deletion of a set X of vertices is expressed through the subgraph G.induce (↑X)ᶜ induced on the remaining vertices.
• Adjacent vertices. No set of vertices other than s and t separates adjacent vertices s and t, so the edge s(s, t) is deleted as well and counted separately: for some k, there are k + 1 such paths, one of them the edge itself, and k vertices whose deletion together with that of the edge separates s from t.
• Vertex-capacitated form. With a capacity c v : ℕ on every vertex, a packing is a family of s–t paths, repetitions allowed, in which every vertex v other than s and t lies on at most c v members. The largest packing has as many members as the least weight ∑ v ∈ X, c v of a separator X.
• Set-to-set form. For vertex sets A and B, possibly overlapping, an A–B path runs from a vertex of A to a vertex of B and has no other vertex in A or B. The largest number of pairwise vertex-disjoint A–B paths equals the least number of vertices meeting every walk from a vertex of A to a vertex of B; such a separator may meet A and B, and a vertex of A ∩ B is a path of length zero. The vertex-capacitated version counts every vertex, endpoints included, against its capacity.

Each form comes with weak duality, which needs no finiteness, and a witness form giving a path family and a separator of equal size. The local form and the set-to-set form also have predicate forms; the predicate form of the local form holds for arbitrary vertices s and t.

Main definitions

• SimpleGraph.Walk.InternallyDisjoint: two walks from s to t sharing no vertex other than s and t.

Main results

• SimpleGraph.card_le_card_of_not_reachable_induce: weak duality for internally disjoint walks.
• SimpleGraph.exists_paths_vertexSeparator_card_eq: Menger's theorem for internally vertex-disjoint paths, in witness form.
• SimpleGraph.forall_reachable_induce_iff_exists_paths: its predicate form: t stays reachable from s after deleting any fewer than k vertices other than s and t exactly when there are k internally vertex-disjoint s–t paths.
• SimpleGraph.card_le_card_add_one_of_not_reachable_induce_deleteEdges and SimpleGraph.exists_paths_vertexSeparator_card_add_one_eq: the form for adjacent vertices.
• SimpleGraph.card_le_sum_of_not_reachable_induce and SimpleGraph.exists_paths_vertexSeparator_sum_eq: the vertex-capacitated form.
• SimpleGraph.card_le_card_of_forall_exists_mem_support, SimpleGraph.exists_paths_setSeparator_card_eq and SimpleGraph.forall_exists_walk_iff_exists_paths: the set-to-set form.
• SimpleGraph.card_le_sum_of_forall_exists_mem_support and SimpleGraph.exists_paths_setSeparator_sum_eq: the vertex-capacitated set-to-set form.

Implementation notes

Apart from the form for adjacent vertices, every statement is transported from the corresponding theorem for directed walks of an arrow family (TauCeti.exists_paths_vertexSeparator_card_eq and its companions) applied to the adjacency arrow family SimpleGraph.AdjHom G. Its directed walks are the walks of G with the same vertex sequences (SimpleGraph.Walk.arrowWalkEquiv), and reachability after deleting X is reachability avoiding X (SimpleGraph.reachable_induce_compl_iff). The form for adjacent vertices applies the nonadjacent form to the graph G.deleteEdges {s(s, t)}; a path from s to t traversing the edge s(s, t) is that edge (SimpleGraph.Walk.IsPath.eq_adj_toWalk_of_mem_edges).

References

• K. Menger, Zur allgemeinen Kurventheorie, Fund. Math. 10 (1927).
• R. Diestel, Graph Theory, 5th ed., Graduate Texts in Mathematics 173, Springer, 2017, Section 3.3.

Internally disjoint walks

def SimpleGraph.Walk.InternallyDisjoint {V : Type u} {G : SimpleGraph V} {s t : V} (p q : G.Walk s t) : Prop

Two walks from s to t are internally disjoint when they share no vertex other than s and t.

theorem SimpleGraph.Walk.internallyDisjoint_def {V : Type u} {G : SimpleGraph V} {s t : V} {p q : G.Walk s t} : p.InternallyDisjoint q ↔ ∀ v ∈ p.support, v ∈ q.support → v = s ∨ v = t

theorem SimpleGraph.Walk.InternallyDisjoint.symm {V : Type u} {G : SimpleGraph V} {s t : V} {p q : G.Walk s t} (h : p.InternallyDisjoint q) : q.InternallyDisjoint p

theorem SimpleGraph.Walk.internallyDisjoint_comm {V : Type u} {G : SimpleGraph V} {s t : V} {p q : G.Walk s t} : p.InternallyDisjoint q ↔ q.InternallyDisjoint p

theorem SimpleGraph.Walk.InternallyDisjoint.isCycle_append_reverse {V : Type u} {G : SimpleGraph V} {s t : V} {p q : G.Walk s t} (h : p.InternallyDisjoint q) (hp : p.IsPath) (hq : q.IsPath) (hpq : p ≠ q) : (p.append q.reverse).IsCycle

Two distinct internally disjoint paths form a cycle when one is traversed in reverse.

theorem SimpleGraph.Walk.IsCycle.takeUntil_internallyDisjoint_dropUntil_reverse {V : Type u} {G : SimpleGraph V} {s t : V} [DecidableEq V] {c : G.Walk s s} (hc : c.IsCycle) (ht : t ∈ c.support) : (c.takeUntil t ht).InternallyDisjoint (c.dropUntil t ht).reverse

The two arcs obtained by splitting a cycle at a vertex are internally disjoint walks with the same endpoints.

@[simp]

theorem SimpleGraph.Walk.internallyDisjoint_toArrowWalk_iff {V : Type u} {G : SimpleGraph V} {s t : V} {p q : G.Walk s t} : p.toArrowWalk.InternallyDisjoint q.toArrowWalk ↔ p.InternallyDisjoint q

@[simp]

theorem TauCeti.ArrowWalk.internallyDisjoint_toWalk_iff {V : Type u} {G : SimpleGraph V} {s t : V} {p q : ArrowWalk G.AdjHom s t} : p.toWalk.InternallyDisjoint q.toWalk ↔ p.InternallyDisjoint q

Paths between two vertices

theorem SimpleGraph.card_le_sum_of_not_reachable_induce {V : Type u} {G : SimpleGraph V} {s t : V} [DecidableEq V] {ι : Type u_1} [Fintype ι] {P : ι → G.Walk s t} {c : V → ℕ} (hP : ∀ (v : V), v ≠ s → v ≠ t → {i : ι | v ∈ (P i).support}.card ≤ c v) {X : Finset V} (hs : s ∉ X) (ht : t ∉ X) (hX : ¬(induce (↑X)ᶜ G).Reachable ⟨s, hs⟩ ⟨t, ht⟩) : Fintype.card ι ≤ ∑ v ∈ X, c v

Weak duality for vertex-capacitated packings. A family of s–t walks 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 other than s and t whose deletion separates s from t.

theorem SimpleGraph.exists_paths_vertexSeparator_sum_eq {V : Type u} {G : SimpleGraph V} {s t : V} [Finite V] [DecidableEq V] (c : V → ℕ) (hst : s ≠ t) (hadj : ¬G.Adj s t) : ∃ (k : ℕ) (P : Fin k → G.Walk s t) (X : Finset V), (∀ (i : Fin k), (P i).IsPath) ∧ (∀ (v : V), v ≠ s → v ≠ t → {i : Fin k | v ∈ (P i).support}.card ≤ c v) ∧ ∃ (hs : s ∉ X) (ht : t ∉ X), ¬(induce (↑X)ᶜ G).Reachable ⟨s, hs⟩ ⟨t, ht⟩ ∧ ∑ v ∈ X, c v = k

Vertex-capacitated Menger's theorem. Let s and t be distinct nonadjacent vertices of a simple graph on a finite vertex type, 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 vertices other than s and t, whose deletion separates s from t, satisfy ∑ v ∈ X, c v = k. By SimpleGraph.card_le_sum_of_not_reachable_induce, the family is then largest and the separator of least weight.

theorem SimpleGraph.card_le_card_of_not_reachable_induce {V : Type u} {G : SimpleGraph V} {s t : V} {ι : Type u_1} [Fintype ι] {P : ι → G.Walk s t} (hP : Pairwise fun (i j : ι) => (P i).InternallyDisjoint (P j)) {X : Finset V} (hs : s ∉ X) (ht : t ∉ X) (hX : ¬(induce (↑X)ᶜ G).Reachable ⟨s, hs⟩ ⟨t, ht⟩) : Fintype.card ι ≤ X.card

Weak duality for internally vertex-disjoint walks. A family of s–t walks pairwise sharing no vertex other than s and t has at most #X members, for every set X of vertices other than s and t whose deletion separates s from t.

theorem SimpleGraph.exists_paths_vertexSeparator_card_eq {V : Type u} {G : SimpleGraph V} {s t : V} [Finite V] (hst : s ≠ t) (hadj : ¬G.Adj s t) : ∃ (k : ℕ) (P : Fin k → G.Walk s t) (X : Finset V), Function.Injective P ∧ (∀ (i : Fin k), (P i).IsPath) ∧ (Pairwise fun (i j : Fin k) => (P i).InternallyDisjoint (P j)) ∧ ∃ (hs : s ∉ X) (ht : t ∉ X), ¬(induce (↑X)ᶜ G).Reachable ⟨s, hs⟩ ⟨t, ht⟩ ∧ X.card = k

Menger's theorem for internally vertex-disjoint paths. Let s and t be distinct nonadjacent vertices of a simple graph on a finite vertex type. Some family of k distinct paths from s to t, pairwise sharing no vertex other than s and t, and some set of k vertices other than s and t, whose deletion separates s from t, exist. By SimpleGraph.card_le_card_of_not_reachable_induce, the family is then largest and the separator smallest.

theorem SimpleGraph.forall_reachable_induce_iff_exists_paths {V : Type u} {G : SimpleGraph V} {s t : V} [Finite V] (k : ℕ) : (∀ (X : Finset V) (hs : s ∉ X) (ht : t ∉ X), X.card < k → (induce (↑X)ᶜ G).Reachable ⟨s, hs⟩ ⟨t, ht⟩) ↔ ∃ (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, predicate form. Let s and t be vertices of a simple graph on a finite vertex type. Then t stays reachable from s 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 SimpleGraph.Walk.exists_mem_support_ne_ne {V : Type u} {G : SimpleGraph V} {s t : V} (hst : s ≠ t) (hadj : ¬G.Adj s t) (p : G.Walk s t) : ∃ v ∈ p.support, v ≠ s ∧ v ≠ t

A walk between distinct nonadjacent vertices visits a vertex other than its endpoints.

Paths between adjacent vertices

theorem SimpleGraph.card_le_card_add_one_of_not_reachable_induce_deleteEdges {V : Type u} {G : SimpleGraph V} {s t : V} {ι : Type u_1} [Fintype ι] {P : ι → G.Walk s t} (hinj : Function.Injective P) (hP : ∀ (i : ι), (P i).IsPath) (hdisj : Pairwise fun (i j : ι) => (P i).InternallyDisjoint (P j)) {X : Finset V} (hs : s ∉ X) (ht : t ∉ X) (hX : ¬(induce (↑X)ᶜ (G.deleteEdges {s(s, t)})).Reachable ⟨s, hs⟩ ⟨t, ht⟩) : Fintype.card ι ≤ X.card + 1

Weak duality for internally vertex-disjoint paths between possibly adjacent vertices. Let X be a set of vertices other than s and t whose deletion, together with that of the edge s(s, t), separates s from t. A family of distinct paths from s to t, pairwise sharing no vertex other than s and t, has at most #X + 1 members.

theorem SimpleGraph.exists_paths_vertexSeparator_card_add_one_eq {V : Type u} {G : SimpleGraph V} {s t : V} [Finite V] (h : G.Adj s t) : ∃ (k : ℕ) (P : Fin (k + 1) → G.Walk s t) (X : Finset V), Function.Injective P ∧ (∀ (i : Fin (k + 1)), (P i).IsPath) ∧ (Pairwise fun (i j : Fin (k + 1)) => (P i).InternallyDisjoint (P j)) ∧ P (Fin.last k) = h.toWalk ∧ ∃ (hs : s ∉ X) (ht : t ∉ X), ¬(induce (↑X)ᶜ (G.deleteEdges {s(s, t)})).Reachable ⟨s, hs⟩ ⟨t, ht⟩ ∧ X.card = k

Menger's theorem for internally vertex-disjoint paths between adjacent vertices. Let s and t be adjacent vertices of a simple graph on a finite vertex type. For some k, there are a family of k + 1 distinct paths from s to t, pairwise sharing no vertex other than s and t, whose last member is the path consisting of the edge s(s, t), and a set of k vertices other than s and t whose deletion, together with that of the edge s(s, t), separates s from t. By SimpleGraph.card_le_card_add_one_of_not_reachable_induce_deleteEdges, the family is then largest and the separator smallest.

Paths between two vertex sets

theorem SimpleGraph.card_le_sum_of_forall_exists_mem_support {V : Type u} {G : SimpleGraph V} [DecidableEq V] {A B : Finset V} {ι : Type u_1} [Fintype ι] {a b : ι → V} {P : (i : ι) → G.Walk (a i) (b i)} (ha : ∀ (i : ι), a i ∈ A) (hb : ∀ (i : ι), b i ∈ B) {c : V → ℕ} (hP : ∀ (v : V), {i : ι | v ∈ (P i).support}.card ≤ c v) {X : Finset V} (hX : ∀ a ∈ A, ∀ b ∈ B, ∀ (p : G.Walk a b), ∃ v ∈ p.support, v ∈ X) : Fintype.card ι ≤ ∑ v ∈ X, c v

Weak duality for vertex-capacitated set-to-set packings. A family of walks, each from a vertex of A to a vertex of B, in which every vertex v lies on at most c v members, has at most ∑ v ∈ X, c v members, for every set X of vertices meeting every walk from a vertex of A to a vertex of B.

theorem SimpleGraph.exists_paths_setSeparator_sum_eq {V : Type u} {G : SimpleGraph V} [Finite V] [DecidableEq V] (c : V → ℕ) (A B : Finset V) : ∃ (k : ℕ) (a : Fin k → V) (b : Fin k → V) (P : (i : Fin k) → G.Walk (a i) (b i)) (X : Finset V), (∀ (i : Fin k), a i ∈ A) ∧ (∀ (i : Fin k), b i ∈ B) ∧ (∀ (i : Fin k), (P i).IsPath) ∧ (∀ (i : Fin k), ∀ v ∈ (P i).support, v ≠ a i → v ≠ b i → v ∉ A ∧ v ∉ B) ∧ (∀ (v : V), {i : Fin k | v ∈ (P i).support}.card ≤ c v) ∧ (∀ a ∈ A, ∀ b ∈ B, ∀ (p : G.Walk a b), ∃ v ∈ p.support, v ∈ X) ∧ ∑ v ∈ X, c v = k

Vertex-capacitated Menger's theorem between vertex sets. Let A and B be sets of vertices of a simple graph on a finite vertex type, and let c v be a capacity on every vertex. Some family of k paths, the i-th from a i ∈ A to b i ∈ B with its other vertices in neither A nor B, in which every vertex v lies on at most c v members, and some set X of vertices meeting every walk from a vertex of A to a vertex of B satisfy ∑ v ∈ X, c v = k. By SimpleGraph.card_le_sum_of_forall_exists_mem_support, the family is then largest and the separator of least weight.

theorem SimpleGraph.card_le_card_of_forall_exists_mem_support {V : Type u} {G : SimpleGraph V} {A B : Finset V} {ι : Type u_1} [Fintype ι] {a b : ι → V} {P : (i : ι) → G.Walk (a i) (b i)} (ha : ∀ (i : ι), a i ∈ A) (hb : ∀ (i : ι), b i ∈ B) (hP : Pairwise fun (i j : ι) => (P i).support.Disjoint (P j).support) {X : Finset V} (hX : ∀ a ∈ A, ∀ b ∈ B, ∀ (p : G.Walk a b), ∃ v ∈ p.support, v ∈ X) : Fintype.card ι ≤ X.card

Weak duality for vertex-disjoint set-to-set walks. A family of pairwise vertex-disjoint walks, each from a vertex of A to a vertex of B, has at most #X members, for every set X of vertices meeting every walk from a vertex of A to a vertex of B.

theorem SimpleGraph.exists_paths_setSeparator_card_eq {V : Type u} {G : SimpleGraph V} [Finite V] (A B : Finset V) : ∃ (k : ℕ) (a : Fin k → V) (b : Fin k → V) (P : (i : Fin k) → G.Walk (a i) (b i)) (X : Finset V), (∀ (i : Fin k), a i ∈ A) ∧ (∀ (i : Fin k), b i ∈ B) ∧ (∀ (i : Fin k), (P i).IsPath) ∧ (∀ (i : Fin k), ∀ v ∈ (P i).support, v ≠ a i → v ≠ b i → v ∉ A ∧ v ∉ B) ∧ (Pairwise fun (i j : Fin k) => (P i).support.Disjoint (P j).support) ∧ (∀ a ∈ A, ∀ b ∈ B, ∀ (p : G.Walk a b), ∃ v ∈ p.support, v ∈ X) ∧ X.card = k

Menger's theorem for vertex-disjoint paths between vertex sets. Let A and B be sets of vertices of a simple graph on a finite vertex type. Some family of k pairwise vertex-disjoint paths, the i-th from a i ∈ A to b i ∈ B with its other vertices in neither A nor B, and some set of k vertices meeting every walk from a vertex of A to a vertex of B exist. By SimpleGraph.card_le_card_of_forall_exists_mem_support, the family is then largest and the separator smallest.

theorem SimpleGraph.forall_exists_walk_iff_exists_paths {V : Type u} {G : SimpleGraph V} [Finite V] (A B : Finset V) (k : ℕ) : (∀ (X : Finset V), X.card < k → ∃ a ∈ A, ∃ b ∈ B, ∃ (p : G.Walk a b), ∀ v ∈ p.support, v ∉ X) ↔ ∃ (a : Fin k → V) (b : Fin k → V) (P : (i : Fin k) → G.Walk (a i) (b i)), (∀ (i : Fin k), a i ∈ A) ∧ (∀ (i : Fin k), b i ∈ B) ∧ (∀ (i : Fin k), (P i).IsPath) ∧ (∀ (i : Fin k), ∀ v ∈ (P i).support, v ≠ a i → v ≠ b i → v ∉ A ∧ v ∉ B) ∧ Pairwise fun (i j : Fin k) => (P i).support.Disjoint (P j).support

Menger's theorem for vertex-disjoint paths between vertex sets, predicate form. Let A and B be sets of vertices of a simple graph on a finite vertex type. For every set X of fewer than k vertices, some walk from a vertex of A to a vertex of B avoids X, exactly when there are k pairwise vertex-disjoint paths, each from a vertex of A to a vertex of B with its other vertices in neither A nor B.