Symmetric quivers and arrow reversal #
This file contains constructions related to symmetric quivers:
Symmetrify V
adds formal inverses to each arrow ofV
.HasReverse
is the class of quivers where each arrow has an assigned formal inverse.HasInvolutiveReverse
extendsHasReverse
by requiring that the reverse of the reverse is equal to the original arrow.Prefunctor.PreserveReverse
is the class of prefunctors mapping reverses to reverses.Symmetrify.of
,Symmetrify.lift
, and the associated lemmas witness the universal property ofSymmetrify
.
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
Equations
- Quiver.symmetrifyQuiver V = { Hom := fun (a b : V) => (a ⟶ b) ⊕ (b ⟶ a) }
A quiver HasReverse
if we can reverse an arrow p
from a
to b
to get an arrow
p.reverse
from b
to a
.
the map which sends an arrow to its reverse
Reverse the direction of an arrow.
Equations
- Quiver.reverse = Quiver.HasReverse.reverse'
A quiver HasInvolutiveReverse
if reversing twice is the identity.
- inv' : ∀ {a b : V} (f : a ⟶ b), Quiver.reverse (Quiver.reverse f) = f
reverse
is involutive
A prefunctor preserving reversal of arrows
- map_reverse' : ∀ {u v : U} (e : u ⟶ v), φ.map (Quiver.reverse e) = Quiver.reverse (φ.map e)
The image of a reverse is the reverse of the image.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- Quiver.instHasReverseSymmetrifySymmetrifyQuiver = { reverse' := fun {a b : Quiver.Symmetrify V} (e : a ⟶ b) => Sum.swap e }
Equations
- Quiver.instHasInvolutiveReverseSymmetrifySymmetrifyQuiver = Quiver.HasInvolutiveReverse.mk ⋯
Shorthand for the "forward" arrow corresponding to f
in symmetrify V
Equations
- Quiver.Hom.toPos f = Sum.inl f
Shorthand for the "backward" arrow corresponding to f
in symmetrify V
Equations
- Quiver.Hom.toNeg f = Sum.inr f
Reverse the direction of a path.
Equations
- Quiver.Path.reverse Quiver.Path.nil = Quiver.Path.nil
- Quiver.Path.reverse (Quiver.Path.cons p e) = Quiver.Path.comp (Quiver.Hom.toPath (Quiver.reverse e)) (Quiver.Path.reverse p)
The inclusion of a quiver in its symmetrification
Equations
- Quiver.Symmetrify.of = { obj := id, map := fun {X Y : V} => Sum.inl }
Given a quiver V'
with reversible arrows, a prefunctor to V'
can be lifted to one from
Symmetrify V
to V'
Equations
- One or more equations did not get rendered due to their size.
lift φ
is the only prefunctor extending φ
and preserving reverses.
A prefunctor canonically defines a prefunctor of the symmetrifications.
Equations
- Prefunctor.symmetrify φ = { obj := φ.obj, map := fun {X Y : Quiver.Symmetrify U} => Sum.map φ.map φ.map }
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- ⋯ = ⋯
A quiver is preconnected iff there exists a path between any pair of
vertices.
Note that if V
doesn't 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.
Equations
- Quiver.IsPreconnected V = ∀ (X Y : V), Nonempty (Quiver.Path X Y)