Weakly and strongly connected components

For a quiver V, define the type WeaklyConnectedComponent V as the quotient of V by the relation which identifies a with b if there is a path from a to b in Symmetrify V. (These zigzags can be seen as a proof-relevant analogue of EqvGen.)

We define:

• Quiver.IsStronglyConnected V: every pair of vertices is connected by a (possibly empty) path.
• Quiver.IsSStronglyConnected V: every pair of vertices is connected by a path of positive length.
• Quiver.StronglyConnectedComponent V: the quotient by the equivalence relation “paths in both directions”.

These concepts relate strong and weak connectivity and let us reason about strongly connected components in directed graphs.

@[implicit_reducible]

def Quiver.zigzagSetoid (V : Type u_1) [Quiver V] : Setoid V

Two vertices are related in the zigzag setoid if there is a zigzag of arrows from one to the other.

def Quiver.WeaklyConnectedComponent (V : Type u_1) [Quiver V] : Type u_1

The type of weakly connected components of a directed graph. Two vertices are in the same weakly connected component if there is a zigzag of arrows from one to the other.

def Quiver.WeaklyConnectedComponent.mk {V : Type u_1} [Quiver V] : V → WeaklyConnectedComponent V

The weakly connected component corresponding to a vertex.

@[implicit_reducible]

instance Quiver.WeaklyConnectedComponent.instCoeTC {V : Type u_1} [Quiver V] : CoeTC V (WeaklyConnectedComponent V)

@[implicit_reducible]

instance Quiver.WeaklyConnectedComponent.instInhabited {V : Type u_1} [Quiver V] [Inhabited V] : Inhabited (WeaklyConnectedComponent V)

theorem Quiver.WeaklyConnectedComponent.eq {V : Type u_1} [Quiver V] (a b : V) : WeaklyConnectedComponent.mk a = WeaklyConnectedComponent.mk b ↔ Nonempty (Path a b)

def Quiver.wideSubquiverSymmetrify {V : Type u_1} [Quiver V] (H : WideSubquiver (Symmetrify V)) : WideSubquiver V

A wide subquiver H of Symmetrify V determines a wide subquiver of V, containing an arrow e if either e or its reversal is in H.

Strongly connected components (directed connectivity)

We define strong connectivity (IsStronglyConnected), its positive-length refinement (IsSStronglyConnected), and strongly connected components.

def Quiver.IsStronglyConnected (V : Type u_2) [Quiver V] : Prop

Strong connectivity: every ordered pair of vertices is joined by a (possibly empty) directed path.

def Quiver.IsSStronglyConnected (V : Type u_2) [Quiver V] : Prop

Positive strong connectivity: every ordered pair of vertices is joined by a directed path of positive length.

@[simp]

theorem Quiver.isStronglyConnected_iff (V : Type u_2) [Quiver V] : IsStronglyConnected V ↔ ∀ (i j : V), Nonempty (Path i j)

@[simp]

theorem Quiver.isSStronglyConnected_iff (V : Type u_2) [Quiver V] : IsSStronglyConnected V ↔ ∀ (i j : V), ∃ (p : Path i j), 0 < p.length

theorem Quiver.IsStronglyConnected.nonempty_path (V : Type u_2) [Quiver V] (h : IsStronglyConnected V) (i j : V) : Nonempty (Path i j)

theorem Quiver.IsSStronglyConnected.exists_pos_path (V : Type u_2) [Quiver V] (h : IsSStronglyConnected V) (i j : V) : ∃ (p : Path i j), 0 < p.length

theorem Quiver.IsSStronglyConnected.exists_pos_cycle (V : Type u_2) [Quiver V] (h : IsSStronglyConnected V) (i : V) : ∃ (p : Path i i), 0 < p.length

theorem Quiver.IsSStronglyConnected.isStronglyConnected (V : Type u_2) [Quiver V] (h : IsSStronglyConnected V) : IsStronglyConnected V

@[implicit_reducible]

def Quiver.stronglyConnectedSetoid (V : Type u_2) [Quiver V] : Setoid V

Equivalence relation identifying vertices connected by directed paths in both directions.

def Quiver.StronglyConnectedComponent (V : Type u_2) [Quiver V] : Type u_2

The type of strongly connected components (bidirectional reachability classes).

def Quiver.StronglyConnectedComponent.mk {V : Type u_2} [Quiver V] : V → StronglyConnectedComponent V

The canonical map from a vertex to its strongly connected component.

@[implicit_reducible]

instance Quiver.StronglyConnectedComponent.instCoe {V : Type u_2} [Quiver V] : Coe V (StronglyConnectedComponent V)

@[implicit_reducible]

instance Quiver.StronglyConnectedComponent.instInhabited {V : Type u_2} [Quiver V] [Inhabited V] : Inhabited (StronglyConnectedComponent V)

theorem Quiver.StronglyConnectedComponent.eq {V : Type u_2} [Quiver V] (a b : V) : StronglyConnectedComponent.mk a = StronglyConnectedComponent.mk b ↔ Nonempty (Path a b) ∧ Nonempty (Path b a)

@[simp]

theorem Quiver.StronglyConnectedComponent.mk_eq_mk {V : Type u_2} [Quiver V] {a b : V} : StronglyConnectedComponent.mk a = StronglyConnectedComponent.mk b ↔ Nonempty (Path a b) ∧ Nonempty (Path b a)

theorem Quiver.StronglyConnectedComponent.IsSStronglyConnected.pos_cycle {V : Type u_2} [Quiver V] (h : IsSStronglyConnected V) (v : V) : ∃ (p : Path v v), 0 < p.length

theorem Quiver.stronglyConnectedComponent_eq_of_path {V : Type u_2} [Quiver V] {a b : V} (hab : Nonempty (Path a b)) (hba : Nonempty (Path b a)) : StronglyConnectedComponent.mk a = StronglyConnectedComponent.mk b

theorem Quiver.exists_path_of_stronglyConnectedComponent_eq {V : Type u_2} [Quiver V] {a b : V} (h : StronglyConnectedComponent.mk a = StronglyConnectedComponent.mk b) : Nonempty (Path a b) ∧ Nonempty (Path b a)

theorem Quiver.stronglyConnectedComponent_singleton_iff {V : Type u_2} [Quiver V] (v : V) : (∀ (w : V), StronglyConnectedComponent.mk w = StronglyConnectedComponent.mk v → w = v) ↔ ∀ (w : V), w ≠ v → ¬(Nonempty (Path v w) ∧ Nonempty (Path w v))

theorem Quiver.IsStronglyConnected.isStronglyConnected_symmetrify {V : Type u_2} [Quiver V] (h : IsStronglyConnected V) : IsStronglyConnected (Symmetrify V)

theorem Quiver.IsStronglyConnected.isSStronglyConnected_of_hom {V : Type u_2} [Quiver V] (h_sc : IsStronglyConnected V) {i₀ j₀ : V} (e₀ : i₀ ⟶ j₀) : IsSStronglyConnected V