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.

source
def quiver.zigzag_setoid (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
source
def quiver.weakly_connected_component (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
Instances for quiver.weakly_connected_component
source
@[protected]
def quiver.weakly_connected_component.mk {V : Type u_1} [quiver V] :
V → quiver.weakly_connected_component V

The weakly connected component corresponding to a vertex.

Equations
source
@[protected, instance]
def quiver.weakly_connected_component.has_coe_t {V : Type u_1} [quiver V] :
has_coe_t V (quiver.weakly_connected_component V)
Equations
source
@[protected, instance]
def quiver.weakly_connected_component.inhabited {V : Type u_1} [quiver V] [inhabited V] :
inhabited (quiver.weakly_connected_component V)
Equations
source
@[protected]
theorem quiver.weakly_connected_component.eq {V : Type u_1} [quiver V] (a b : V) :
↑a = ↑b ↔ nonempty (quiver.path a b)
source
def quiver.wide_subquiver_symmetrify {V : Type u_1} [quiver V] (H : wide_subquiver (quiver.symmetrify V)) :
wide_subquiver 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