Arc connectivity and vertex strong connectivity of arrow families

Let Q be an arrow family on a vertex type V. A vertex t is k-arc-reachable from s, IsArcReachable Q k s t, when t stays reachable from s after deleting any set of fewer than k arrows; arrows are deleted as identities, so parallel arrows count separately. The family is k-arc-strong, IsArcStrong Q k, when every vertex is k-arc-reachable from every vertex, and k-vertex-strong, IsVertexStrong Q k, when it has more than k vertices and any two vertices outside a set of fewer than k deleted vertices remain reachable from each other. The invariants arcConnectivity Q and vertexStrongConnectivity Q are the suprema in ℕ∞ of the thresholds at which these predicates hold. As for undirected graphs, on at most one vertex the arc connectivity is ⊤ and the vertex strong connectivity is 0.

The threshold 1 for arc strength is strong connectivity in the sense of Mathlib's Quiver.IsStronglyConnected; for vertex strength it additionally requires at least two vertices. The predicates are the directed counterparts of the undirected edge and vertex connectivity predicates. The arrow-disjoint path form of IsArcReachable is obtained by applying TauCeti.forall_reachableWithout_iff_exists_paths from Menger/Edge through TauCeti.isArcReachable_def.

Main results

• TauCeti.isVertexStrong_iff_exists_paths: an arrow family on a finite vertex type is k-vertex-strong exactly when it has more than k vertices and any two distinct vertices are joined by k distinct, pairwise internally vertex-disjoint directed paths. Arrows s → t are allowed, and then contribute one-arrow paths.
• TauCeti.IsVertexStrong.isArcStrong and TauCeti.vertexStrongConnectivity_le_arcConnectivity: the directed Whitney inequality.
• TauCeti.arcConnectivity_le_card_out and TauCeti.arcConnectivity_le_card_in: on at least two vertices, arc connectivity is at most every out-degree and every in-degree.
• TauCeti.isArcStrong_iff_le_arcConnectivity and TauCeti.isVertexStrong_iff_le_vertexStrongConnectivity: the invariants record exactly the thresholds at which the predicates hold, the latter on a nonempty vertex type. On the empty type the vertex strong connectivity is 0 although no family on it is 0-vertex-strong.

Implementation notes

The Whitney inequality follows the standard argument: if fewer than k arrows leave a set C containing s but not t, and some u ∈ C has no arrow to some w ∉ C, deleting one endpoint of each of these arrows, other than u and w, separates w from u. Otherwise every pair in C × Cᶜ is joined by a leaving arrow, which forces at least |V| - 1 of them.

For global vertex Menger between adjacent vertices s and t, delete the arrows from s to t. After further deleting fewer than k - 1 vertices, some third vertex w survives, and the k-vertex-strong family supplies walks from s to w avoiding t and from w to t avoiding s, neither of which uses an arrow from s to t. Local vertex Menger then gives k - 1 paths, to which one arrow from s to t is added.

References

• J. Bang-Jensen, G. Gutin, Digraphs: Theory, Algorithms and Applications, 2nd ed., Springer, 2009, Sections 5.1 and 5.4.

Arc reachability

def TauCeti.IsArcReachable {V : Type u} (Q : V → V → Type v) (k : ℕ) (s t : V) : Prop

The vertex t is k-arc-reachable from s when it stays reachable from s after deleting any set of fewer than k arrows.

theorem TauCeti.isArcReachable_def {V : Type u} {Q : V → V → Type v} {k : ℕ} {s t : V} : IsArcReachable Q k s t ↔ ∀ (F : Finset ((x : V) × (y : V) × Q x y)), F.card < k → ReachableWithout (↑F) s t

@[simp]

theorem TauCeti.IsArcReachable.zero {V : Type u} {Q : V → V → Type v} {s t : V} : IsArcReachable Q 0 s t

@[simp]

theorem TauCeti.isArcReachable_one {V : Type u} {Q : V → V → Type v} {s t : V} : IsArcReachable Q 1 s t ↔ Nonempty (ArrowWalk Q s t)

Reachability is 1-arc-reachability.

theorem TauCeti.IsArcReachable.anti {V : Type u} {Q : V → V → Type v} {k l : ℕ} {s t : V} (hkl : k ≤ l) (h : IsArcReachable Q l s t) : IsArcReachable Q k s t

@[simp]

theorem TauCeti.IsArcReachable.refl {V : Type u} {Q : V → V → Type v} (k : ℕ) (s : V) : IsArcReachable Q k s s

theorem TauCeti.IsArcReachable.trans {V : Type u} {Q : V → V → Type v} {k : ℕ} {s t x : V} (h : IsArcReachable Q k s t) (h' : IsArcReachable Q k t x) : IsArcReachable Q k s x

theorem TauCeti.IsArcReachable.nonempty_arrowWalk {V : Type u} {Q : V → V → Type v} {k : ℕ} {s t : V} (hk : k ≠ 0) (h : IsArcReachable Q k s t) : Nonempty (ArrowWalk Q s t)

theorem TauCeti.IsArcReachable.le_card {V : Type u} {Q : V → V → Type v} {k : ℕ} {s t : V} {C : Set V} (h : IsArcReachable Q k s t) (hs : s ∈ C) (ht : t ∉ C) {F : Finset ((x : V) × (y : V) × Q x y)} (hF : ∀ ⦃v w : V⦄ (e : Q v w), v ∈ C → w ∉ C → ⟨v, ⟨w, e⟩⟩ ∈ F) : k ≤ F.card

If t is k-arc-reachable from s, then every finite set of arrows containing all arrows that leave a vertex set C with s ∈ C and t ∉ C has at least k members.

Arc-strong arrow families

def TauCeti.IsArcStrong {V : Type u} (Q : V → V → Type v) (k : ℕ) : Prop

An arrow family is k-arc-strong when every vertex is k-arc-reachable from every vertex.

theorem TauCeti.isArcStrong_def {V : Type u} {Q : V → V → Type v} {k : ℕ} : IsArcStrong Q k ↔ ∀ (s t : V), IsArcReachable Q k s t

theorem TauCeti.IsArcStrong.isArcReachable {V : Type u} {Q : V → V → Type v} {k : ℕ} (h : IsArcStrong Q k) (s t : V) : IsArcReachable Q k s t

@[simp]

theorem TauCeti.IsArcStrong.zero {V : Type u} {Q : V → V → Type v} : IsArcStrong Q 0

@[simp]

theorem TauCeti.isArcStrong_one {V : Type u} {Q : V → V → Type v} : IsArcStrong Q 1 ↔ Quiver.IsStronglyConnected V

An arrow family is 1-arc-strong exactly when it is strongly connected.

theorem TauCeti.IsArcStrong.anti {V : Type u} {Q : V → V → Type v} {k l : ℕ} (hkl : k ≤ l) (h : IsArcStrong Q l) : IsArcStrong Q k

theorem TauCeti.IsArcStrong.of_subsingleton {V : Type u} {Q : V → V → Type v} {k : ℕ} [Subsingleton V] : IsArcStrong Q k

An arrow family on at most one vertex is k-arc-strong for every k.

Vertex-strong arrow families

def TauCeti.IsVertexStrong {V : Type u} (Q : V → V → Type v) (k : ℕ) : Prop

An arrow family is k-vertex-strong when it has more than k vertices, and after deleting any set of fewer than k vertices, every remaining vertex is reachable from every other.

theorem TauCeti.isVertexStrong_def {V : Type u} {Q : V → V → Type v} {k : ℕ} : IsVertexStrong Q k ↔ ↑k < ENat.card V ∧ ∀ (X : Finset V), X.card < k → ∀ ⦃s : V⦄, s ∉ X → ∀ ⦃t : V⦄, t ∉ X → ReachableAvoiding Q (↑X) s t

theorem TauCeti.IsVertexStrong.lt_card {V : Type u} {Q : V → V → Type v} {k : ℕ} (h : IsVertexStrong Q k) : ↑k < ENat.card V

theorem TauCeti.IsVertexStrong.lt_natCard {V : Type u} {Q : V → V → Type v} {k : ℕ} [Finite V] (h : IsVertexStrong Q k) : k < Nat.card V

On a finite vertex type, a vertex-strong threshold is less than the number of vertices.

theorem TauCeti.IsVertexStrong.reachableAvoiding {V : Type u} {Q : V → V → Type v} {k : ℕ} {s t : V} (h : IsVertexStrong Q k) {X : Finset V} (hX : X.card < k) (hs : s ∉ X) (ht : t ∉ X) : ReachableAvoiding Q (↑X) s t

@[simp]

theorem TauCeti.isVertexStrong_zero {V : Type u} {Q : V → V → Type v} : IsVertexStrong Q 0 ↔ Nonempty V

An arrow family is 0-vertex-strong exactly when it has a vertex.

@[simp]

theorem TauCeti.isVertexStrong_one {V : Type u} {Q : V → V → Type v} : IsVertexStrong Q 1 ↔ Nontrivial V ∧ Quiver.IsStronglyConnected V

An arrow family is 1-vertex-strong exactly when it has two distinct vertices and is strongly connected.

theorem TauCeti.IsVertexStrong.anti {V : Type u} {Q : V → V → Type v} {k l : ℕ} (hkl : k ≤ l) (h : IsVertexStrong Q l) : IsVertexStrong Q k

theorem TauCeti.IsVertexStrong.le_card {V : Type u} {Q : V → V → Type v} {k : ℕ} {s t : V} {C : Set V} (h : IsVertexStrong Q k) (hs : s ∈ C) (ht : t ∉ C) {F : Finset ((x : V) × (y : V) × Q x y)} (hF : ∀ ⦃v w : V⦄ (e : Q v w), v ∈ C → w ∉ C → ⟨v, ⟨w, e⟩⟩ ∈ F) : k ≤ F.card

In a k-vertex-strong arrow family, at least k arrows leave every vertex set C containing s but not t: every finite set of arrows containing them all has at least k members.

theorem TauCeti.IsVertexStrong.isArcStrong {V : Type u} {Q : V → V → Type v} {k : ℕ} (h : IsVertexStrong Q k) : IsArcStrong Q k

The directed Whitney inequality. A k-vertex-strong arrow family is k-arc-strong.

theorem TauCeti.isVertexStrong_iff_exists_paths {V : Type u} {Q : V → V → Type v} {k : ℕ} [Finite V] : IsVertexStrong Q k ↔ ↑k < ENat.card V ∧ ∀ ⦃s t : V⦄, s ≠ t → ∃ (P : Fin k → ArrowWalk Q s t), Function.Injective P ∧ (∀ (i : Fin k), (P i).IsPath) ∧ Pairwise fun (i j : Fin k) => (P i).InternallyDisjoint (P j)

Menger's theorem for vertex-strong arrow families. An arrow family on a finite vertex type is k-vertex-strong exactly when it has more than k vertices and any two distinct vertices s and t are joined by k distinct directed paths pairwise sharing no vertex other than s and t. When there are arrows from s to t, one of these paths may be a single arrow.

Numerical invariants

noncomputable def TauCeti.arcConnectivity {V : Type u} (Q : V → V → Type v) : ℕ∞

The arc connectivity of an arrow family: the supremum in ℕ∞ of the natural thresholds k at which it is k-arc-strong. It is ⊤ when there is at most one vertex.

noncomputable def TauCeti.vertexStrongConnectivity {V : Type u} (Q : V → V → Type v) : ℕ∞

The vertex strong connectivity of an arrow family: the supremum in ℕ∞ of the natural thresholds k at which it is k-vertex-strong. It is 0 when there is at most one vertex.

theorem TauCeti.isArcStrong_iff_le_arcConnectivity {V : Type u} {Q : V → V → Type v} (k : ℕ) : IsArcStrong Q k ↔ ↑k ≤ arcConnectivity Q

Arc connectivity records exactly the thresholds at which the arrow family is arc-strong.

theorem TauCeti.isVertexStrong_iff_le_vertexStrongConnectivity {V : Type u} {Q : V → V → Type v} [Nonempty V] (k : ℕ) : IsVertexStrong Q k ↔ ↑k ≤ vertexStrongConnectivity Q

On a nonempty vertex type, vertex strong connectivity records exactly the thresholds at which the arrow family is vertex-strong.

@[simp]

theorem TauCeti.arcConnectivity_eq_top_of_subsingleton {V : Type u} {Q : V → V → Type v} [Subsingleton V] : arcConnectivity Q = ⊤

An arrow family on at most one vertex has arc connectivity ⊤.

@[simp]

theorem TauCeti.vertexStrongConnectivity_eq_zero_of_subsingleton {V : Type u} {Q : V → V → Type v} [Subsingleton V] : vertexStrongConnectivity Q = 0

An arrow family on at most one vertex has vertex strong connectivity 0.

theorem TauCeti.vertexStrongConnectivity_lt_card {V : Type u} {Q : V → V → Type v} [Finite V] [Nonempty V] : vertexStrongConnectivity Q < ENat.card V

On a finite nonempty vertex type, the vertex strong connectivity is less than the number of vertices; in particular it is finite.

theorem TauCeti.vertexStrongConnectivity_le_arcConnectivity {V : Type u} {Q : V → V → Type v} : vertexStrongConnectivity Q ≤ arcConnectivity Q

The directed Whitney inequality, numerical form: the vertex strong connectivity is at most the arc connectivity.

theorem TauCeti.arcConnectivity_le_card_out {V : Type u} {Q : V → V → Type v} [Nontrivial V] (v : V) [Fintype ((w : V) × Q v w)] : arcConnectivity Q ≤ ↑(Fintype.card ((w : V) × Q v w))

On at least two vertices, the arc connectivity is at most the number of arrows leaving any vertex, loops included.

theorem TauCeti.arcConnectivity_le_card_in {V : Type u} {Q : V → V → Type v} [Nontrivial V] (v : V) [Fintype ((w : V) × Q w v)] : arcConnectivity Q ≤ ↑(Fintype.card ((w : V) × Q w v))

On at least two vertices, the arc connectivity is at most the number of arrows entering any vertex, loops included.