Symmetric quivers and arrow reversal #
This file contains constructions related to symmetric quivers:
Symmetrify Vadds formal inverses to each arrow of
HasReverseis the class of quivers where each arrow has an assigned formal inverse.
HasReverseby requiring that the reverse of the reverse is equal to the original arrow.
Prefunctor.PreserveReverseis the class of prefunctors mapping reverses to reverses.
Symmetrify.lift, and the associated lemmas witness the universal property of
HasInvolutiveReverse if reversing twice is the identity.
The image of a reverse is the reverse of the image.
A prefunctor preserving reversal of arrows
Reverse the direction of a path.
lift φ is the only prefunctor extending
φ and preserving reverses.
A quiver is preconnected iff there exists a path between any pair of
Note that if
HasReverse, then the definition is stronger than
simply having a preconnected underlying
SimpleGraph, since a path in one
direction doesn't induce one in the other.