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.

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.

Equations

• Quiver.zigzagSetoid V = { r := fun (a b : V) => Nonempty (Quiver.Path a b), iseqv := ⋯ }

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.

Equations

• Quiver.WeaklyConnectedComponent V = Quotient (Quiver.zigzagSetoid V)

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

The weakly connected component corresponding to a vertex.

Equations

• Quiver.WeaklyConnectedComponent.mk = Quotient.mk'

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

Equations

• Quiver.WeaklyConnectedComponent.instCoeTC = { coe := Quiver.WeaklyConnectedComponent.mk }

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

Equations

• Quiver.WeaklyConnectedComponent.instInhabited = { default := have this := default; Quiver.WeaklyConnectedComponent.mk this }

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.

Equations

• Quiver.wideSubquiverSymmetrify H x✝¹ x✝ = {e : x✝¹ ⟶ x✝ | H x✝¹ x✝ (Sum.inl e) ∨ H x✝ x✝¹ (Sum.inr e)}

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.

Equations

• Quiver.IsStronglyConnected V = ∀ (i j : V), Nonempty (Quiver.Path i j)

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.

Equations

• Quiver.IsSStronglyConnected V = ∀ (i j : V), ∃ (p : Quiver.Path i j), 0 < p.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

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

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

Equations

• Quiver.stronglyConnectedSetoid V = { r := fun (a b : V) => Nonempty (Quiver.Path a b) ∧ Nonempty (Quiver.Path b a), iseqv := ⋯ }

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

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

Equations

• Quiver.StronglyConnectedComponent V = Quotient (Quiver.stronglyConnectedSetoid V)

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

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

Equations

• Quiver.StronglyConnectedComponent.mk = Quotient.mk'

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

Equations

• Quiver.StronglyConnectedComponent.instCoe = { coe := Quiver.StronglyConnectedComponent.mk }

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

Equations

• Quiver.StronglyConnectedComponent.instInhabited = { default := Quiver.StronglyConnectedComponent.mk default }

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