Documentation

TauCeti.Combinatorics.Network.Menger.Adjacent

Menger's theorem for directed paths between adjacent terminals #

Let Q be an arrow family on a finite vertex type V, and let s ≠ t be vertices with finitely many, say m, arrows from s to t. The local vertex form of Menger's theorem (TauCeti.exists_paths_vertexSeparator_card_eq) assumes that there is no arrow from s to t: otherwise no set of vertices avoiding s and t separates t from s. This file removes that hypothesis by counting the direct arrows separately.

After deleting all m arrows from s to t, some set X of k vertices avoiding s and t separates t from s, and the original arrow family has k + m distinct directed s–t paths pairwise sharing no vertex other than s and t; this family contains the m paths consisting of a single arrow from s to t. Conversely, every such family has at most #X + m members whenever X separates t from s after the deletion of the arrows from s to t. Arrows from t to s are retained and do not contribute to m. The separation after deletion is expressed as the mixed separator TauCeti.IsMixedSeparator X (TauCeti.arrowFinset Q s t) s t.

Main definitions #

Main results #

Implementation notes #

Attainment applies TauCeti.exists_paths_vertexSeparator_card_eq to the arrow family TauCeti.WithoutHom obtained by deleting the arrows from s to t, whose walks are the walks avoiding those arrows, and adds the m single-arrow paths to the resulting family.

References #

The arrows from s to t #

source
def TauCeti.arrowFinset {V : Type u} (Q : V → V → Type v) (s t : V) [Fintype (Q s t)] :
Finset ((v : V) × (w : V) × Q v w)

The arrows from s to t, each recorded with its endpoints, as a finite set of the total arrow type.

Instances For
    source
    @[simp]
    theorem TauCeti.mem_arrowFinset {V : Type u} {Q : V → V → Type v} {s t : V} [Fintype (Q s t)] {a : (v : V) × (w : V) × Q v w} :
    a ∈ arrowFinset Q s t ↔ a.fst = s ∧ a.snd.fst = t
    source
    @[simp]
    theorem TauCeti.card_arrowFinset {V : Type u} {Q : V → V → Type v} {s t : V} [Fintype (Q s t)] :
    (arrowFinset Q s t).card = Fintype.card (Q s t)

    Weak duality #

    source
    theorem TauCeti.card_le_card_add_card_of_isMixedSeparator {V : Type u} {Q : V → V → Type v} {s t : V} [Fintype (Q s t)] {ι : Type u_1} [Fintype ι] {P : ι → ArrowWalk Q s t} (hinj : Function.Injective P) (hP : ∀ (i : ι), (P i).IsPath) (hdisj : Pairwise fun (i j : ι) => (P i).InternallyDisjoint (P j)) {X : Finset V} (hX : IsMixedSeparator X (arrowFinset Q s t) s t) :
    Fintype.card ι ≤ X.card + Fintype.card (Q s t)

    Weak duality for internally vertex-disjoint paths between possibly adjacent terminals. Let X be a set of vertices, avoiding s and t, whose deletion together with that of every arrow from s to t leaves t unreachable from s. A family of distinct directed s–t paths whose members pairwise share no vertex other than s and t has at most #X + m members, where m is the number of arrows from s to t.

    Menger's theorem for adjacent terminals #

    source
    theorem TauCeti.exists_paths_of_withoutHom {V : Type u} {Q : V → V → Type v} {s t : V} {ι : Type u_1} {F : Set ((v : V) × (w : V) × Q v w)} (hF : ∀ (e : Q s t), ⟨s, ⟨t, e⟩⟩ ∈ F) (hst : s ≠ t) (P : ι → ArrowWalk (WithoutHom F) s t) (hP : ∀ (i : ι), (P i).IsPath) (hdisj : Pairwise fun (i j : ι) => (P i).InternallyDisjoint (P j)) :
    ∃ (R : ι ⊕ Q s t → ArrowWalk Q s t), Function.Injective R ∧ (∀ (i : ι ⊕ Q s t), (R i).IsPath) ∧ (Pairwise fun (i j : ι ⊕ Q s t) => (R i).InternallyDisjoint (R j)) ∧ ∀ (e : Q s t), R (Sum.inr e) = (ArrowWalk.nil s).cons e

    Push internally disjoint paths avoiding every arrow from s to t into the original arrow family, and add the one-arrow path for each arrow from s to t.

    source
    theorem TauCeti.exists_paths_isMixedSeparator_card_eq {V : Type u} {Q : V → V → Type v} {s t : V} [Finite V] [Fintype (Q s t)] (hst : s ≠ t) :
    ∃ (k : ℕ) (P : Fin k ⊕ Q s t → ArrowWalk Q s t) (X : Finset V), Function.Injective P ∧ (∀ (i : Fin k ⊕ Q s t), (P i).IsPath) ∧ (Pairwise fun (i j : Fin k ⊕ Q s t) => (P i).InternallyDisjoint (P j)) ∧ (∀ (e : Q s t), P (Sum.inr e) = (ArrowWalk.nil s).cons e) ∧ IsMixedSeparator X (arrowFinset Q s t) s t ∧ X.card = k

    Menger's theorem for internally vertex-disjoint directed paths between possibly adjacent terminals. Let s ≠ t be vertices of an arrow family on a finite vertex type, with finitely many arrows from s to t. For some k, there are a family of distinct directed s–t paths indexed by Fin k ⊕ Q s t, pairwise sharing no vertex other than s and t, whose member indexed by an arrow e from s to t is the path consisting of e, and a set X of k vertices, avoiding s and t, whose deletion together with that of every arrow from s to t leaves t unreachable from s. By TauCeti.card_le_card_add_card_of_isMixedSeparator, the family is then largest and the separator smallest.

    source
    theorem TauCeti.forall_not_isMixedSeparator_iff_exists_paths {V : Type u} {Q : V → V → Type v} {s t : V} [Finite V] [Fintype (Q s t)] (hst : s ≠ t) (k : ℕ) :
    (∀ (X : Finset V), X.card < k → ¬IsMixedSeparator X (arrowFinset Q s t) s t) ↔ ∃ (P : Fin k ⊕ Q s t → ArrowWalk Q s t), Function.Injective P ∧ (∀ (i : Fin k ⊕ Q s t), (P i).IsPath) ∧ Pairwise fun (i j : Fin k ⊕ Q s t) => (P i).InternallyDisjoint (P j)

    Menger's theorem for internally vertex-disjoint directed paths between possibly adjacent terminals, predicate form. Let s ≠ t be vertices of an arrow family on a finite vertex type, with finitely many arrows from s to t. Then t stays reachable from s after deleting every arrow from s to t and any fewer than k vertices other than s and t exactly when there is a family of distinct directed s–t paths indexed by Fin k ⊕ Q s t, pairwise sharing no vertex other than s and t.