Weakly 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.)

Strongly connected components have not yet been defined.

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 → Quiver.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 (Quiver.WeaklyConnectedComponent V)

Equations

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

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

Equations

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

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

def Quiver.wideSubquiverSymmetrify {V : Type u_1} [Quiver V] (H : WideSubquiver (Quiver.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)}