# Documentation

Mathlib.Combinatorics.Quiver.ConnectedComponent

## 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) [inst : ] :

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

Equations
def Quiver.WeaklyConnectedComponent (V : Type u_1) [inst : ] :
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
def Quiver.WeaklyConnectedComponent.mk {V : Type u_1} [inst : ] :

The weakly connected component corresponding to a vertex.

Equations
• Quiver.WeaklyConnectedComponent.mk = Quotient.mk'
Equations
• Quiver.WeaklyConnectedComponent.instCoeTCWeaklyConnectedComponent = { coe := Quiver.WeaklyConnectedComponent.mk }
Equations
• Quiver.WeaklyConnectedComponent.instInhabitedWeaklyConnectedComponent = { default := let_fun this := default; }
theorem Quiver.WeaklyConnectedComponent.eq {V : Type u_1} [inst : ] (a : V) (b : V) :
def Quiver.wideSubquiverSymmetrify {V : Type u_1} [inst : ] (H : ) :

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

Equations
• = { e | H x x () H x x () }