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.
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
- quiver.symmetrify V = V
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
Equations
- quiver.symmetrify.has_reverse V = {reverse' := λ (a b : quiver.symmetrify V) (e : a ⟶ b), sum.swap e}
Reverse the direction of an arrow.
Equations
Reverse the direction of a path.
Equations
- (p.cons e).reverse = (quiver.reverse e).to_path.comp p.reverse
- quiver.path.nil.reverse = quiver.path.nil
Two vertices are related in the zigzag setoid if there is a zigzag of arrows from one to the other.
Equations
- quiver.zigzag_setoid V = {r := λ (a b : V), nonempty (quiver.path a b), iseqv := _}
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
The weakly connected component corresponding to a vertex.
Equations
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
.