mathlib documentation

combinatorics.quiver.connected_component

Weakly connected components #

For a quiver V, we build a quiver symmetrify V by adding a reversal of every edge. Informally, a path in symmetrify V corresponds to a 'zigzag' in V. This lets us 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.

@[nolint]
def quiver.symmetrify (V : Type u) :
Type u

A type synonym for the symmetrized quiver (with an arrow both ways for each original arrow). NB: this does not work for Prop-valued quivers. It requires [quiver.{v+1} V].

Equations
Instances for quiver.symmetrify
@[protected, instance]
Equations
@[class]
structure quiver.has_reverse (V : Type u) [quiver V] :
Type (max u v)
  • reverse' : Π {a b : V}, (a b)(b a)

A quiver has_reverse if we can reverse an arrow p from a to b to get an arrow p.reverse from b to a.

Instances of this typeclass
Instances of other typeclasses for quiver.has_reverse
  • quiver.has_reverse.has_sizeof_inst
@[protected, instance]
Equations
def quiver.reverse {V : Type u} [quiver V] [quiver.has_reverse V] {a b : V} :
(a b)(b a)

Reverse the direction of an arrow.

Equations
def quiver.path.reverse {V : Type u} [quiver V] [quiver.has_reverse V] {a b : V} :

Reverse the direction of a path.

Equations
def quiver.zigzag_setoid (V : Type u) [quiver V] :

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

Equations
def quiver.weakly_connected_component (V : Type u) [quiver V] :
Type u

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} [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