Menger's theorem for digraphs

A digraph is an arrow family with at most one arrow between each ordered pair of vertices. This file specializes local vertex Menger to the adjacency arrow family Digraph.AdjHom D, translating the nonadjacency hypothesis IsEmpty (D.AdjHom s t) into ¬D.Adj s t. Paths are TauCeti.ArrowWalks in that family, so their vertex sequences are exactly chains for D.Adj by Digraph.arrowWalkEquiv.

The other directed forms of Menger's theorem need no translation and apply to D.AdjHom directly: the correction for possibly adjacent terminals (TauCeti.exists_paths_isMixedSeparator_card_eq), the set-to-set forms (TauCeti.exists_paths_setSeparator_card_eq) and the arc forms (TauCeti.exists_paths_arrowSeparator_card_eq, TauCeti.exists_paths_setArrowSeparator_card_eq), together with their capacitated and threshold variants. Instantiate them with Q := D.AdjHom. Their finiteness hypotheses on arrows are found by instance search: Decidable (D.Adj s t) gives Fintype (D.AdjHom s t), and every D.AdjHom v w is a subsingleton, so it is Finite.

Main results

• Digraph.exists_paths_vertexSeparator_card_eq: local vertex Menger for nonadjacent terminals.
• Digraph.exists_paths_vertexSeparator_sum_eq: its vertex-capacitated version.
• Digraph.forall_reachableAvoiding_iff_exists_paths: its threshold form, which holds for arbitrary s and t.

References

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

Vertex-disjoint paths between two vertices

theorem Digraph.exists_paths_vertexSeparator_sum_eq {V : Type u} {D : Digraph V} {s t : V} [Finite V] [DecidableEq V] (c : V → ℕ) (hst : s ≠ t) (hadj : ¬D.Adj s t) : ∃ (k : ℕ) (P : Fin k → TauCeti.ArrowWalk D.AdjHom s t) (X : Finset V), (∀ (i : Fin k), (P i).IsPath) ∧ (∀ (v : V), v ≠ s → v ≠ t → {i : Fin k | v ∈ (P i).vertices}.card ≤ c v) ∧ s ∉ X ∧ t ∉ X ∧ ¬TauCeti.ReachableAvoiding D.AdjHom (↑X) s t ∧ ∑ v ∈ X, c v = k

Vertex-capacitated Menger's theorem for a digraph. Let s and t be distinct vertices with no arrow from s to t, and let c v be the capacity of vertex v. Some family of k directed s-to-t paths respects every nonterminal vertex capacity, and some terminal-excluding vertex separator has total capacity k.

theorem Digraph.exists_paths_vertexSeparator_card_eq {V : Type u} {D : Digraph V} {s t : V} [Finite V] (hst : s ≠ t) (hadj : ¬D.Adj s t) : ∃ (k : ℕ) (P : Fin k → TauCeti.ArrowWalk D.AdjHom 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)) ∧ s ∉ X ∧ t ∉ X ∧ ¬TauCeti.ReachableAvoiding D.AdjHom (↑X) s t ∧ X.card = k

Menger's theorem for internally vertex-disjoint paths in a digraph. Between distinct nonadjacent vertices of a finite digraph, some family of pairwise internally vertex-disjoint directed paths has the same cardinality as a terminal-excluding vertex separator.

theorem Digraph.forall_reachableAvoiding_iff_exists_paths {V : Type u} {D : Digraph V} {s t : V} [Finite V] (k : ℕ) : (∀ (X : Finset V), s ∉ X → t ∉ X → X.card < k → TauCeti.ReachableAvoiding D.AdjHom (↑X) s t) ↔ ∃ (P : Fin k → TauCeti.ArrowWalk D.AdjHom s t), (∀ (i : Fin k), (P i).IsPath) ∧ Pairwise fun (i j : Fin k) => (P i).InternallyDisjoint (P j)

Menger's theorem for vertex deletion in a digraph, predicate form. Vertices remain joined after deleting any fewer than k other vertices exactly when there are k pairwise internally vertex-disjoint directed paths between them.