mathlib3 documentation

combinatorics.quiver.connected_component

Weakly connected components #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

For a quiver V, we define the type weakly_connected_component 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 eqv_gen.)

Strongly connected components have not yet been defined.

def quiver.zigzag_setoid (V : Type u_1) [quiver V] :

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

Equations

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
Instances for quiver.weakly_connected_component
@[protected]

The weakly connected component corresponding to a vertex.

Equations
@[protected]
theorem quiver.weakly_connected_component.eq {V : Type u_1} [quiver V] (a b : V) :

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

Equations