# Documentation

## Symmetric quivers and arrow reversal #

This file contains constructions related to symmetric quivers:

• Symmetrify V adds formal inverses to each arrow of V.
• HasReverse is the class of quivers where each arrow has an assigned formal inverse.
• HasInvolutiveReverse extends HasReverse 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 of Symmetrify.
def Quiver.Symmetrify (V : Type u_1) :
Type u_1

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
instance Quiver.symmetrifyQuiver (V : Type u) [] :
Equations
• = { Hom := fun (a b : V) => (a b) (b a) }
class Quiver.HasReverse (V : Type u_2) [] :
Type (max u_2 v)

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

• reverse' : {a b : V} → (a b)(b a)

the map which sends an arrow to its reverse

Instances
def Quiver.reverse {V : Type u_4} [] {a : V} {b : V} :
(a b)(b a)

Reverse the direction of an arrow.

Equations
• Quiver.reverse = Quiver.HasReverse.reverse'
Instances For
class Quiver.HasInvolutiveReverse (V : Type u_2) [] extends :
Type (max u_2 v)

A quiver HasInvolutiveReverse if reversing twice is the identity.

• reverse' : {a b : V} → (a b)(b a)
• inv' : ∀ {a b : V} (f : a b),

reverse is involutive

Instances
theorem Quiver.HasInvolutiveReverse.inv' {V : Type u_2} [] [self : ] {a : V} {b : V} (f : a b) :

reverse is involutive

@[simp]
theorem Quiver.reverse_reverse {V : Type u_2} [] [h : ] {a : V} {b : V} (f : a b) :
@[simp]
theorem Quiver.reverse_inj {V : Type u_2} [] [h : ] {a : V} {b : V} (f : a b) (g : a b) :
f = g
theorem Quiver.eq_reverse_iff {V : Type u_2} [] [h : ] {a : V} {b : V} (f : a b) (g : b a) :
class Prefunctor.MapReverse {U : Type u_1} {V : Type u_2} [] [] (φ : U ⥤q V) :

A prefunctor preserving reversal of arrows

• map_reverse' : ∀ {u v : U} (e : u v), φ.map () = Quiver.reverse (φ.map e)

The image of a reverse is the reverse of the image.

Instances
theorem Prefunctor.MapReverse.map_reverse' {U : Type u_1} {V : Type u_2} [] [] {φ : U ⥤q V} [self : φ.MapReverse] {u : U} {v : U} (e : u v) :
φ.map () = Quiver.reverse (φ.map e)

The image of a reverse is the reverse of the image.

@[simp]
theorem Prefunctor.map_reverse {U : Type u_1} {V : Type u_2} [] [] (φ : U ⥤q V) [φ.MapReverse] {u : U} {v : U} (e : u v) :
φ.map () = Quiver.reverse (φ.map e)
instance Prefunctor.mapReverseComp {U : Type u_1} {V : Type u_2} {W : Type u_3} [] [] [] (φ : U ⥤q V) (ψ : V ⥤q W) [φ.MapReverse] [ψ.MapReverse] :
(φ ⋙q ψ).MapReverse
Equations
• =
instance Prefunctor.mapReverseId {U : Type u_1} [] :
(𝟭q U).MapReverse
Equations
• =
instance Quiver.instHasReverseSymmetrify {V : Type u_2} [] :
Equations
• Quiver.instHasReverseSymmetrify = { reverse' := fun {a b : } (e : a b) => }
Equations
• Quiver.instHasInvolutiveReverseSymmetrify =
@[simp]
theorem Quiver.symmetrify_reverse {V : Type u_2} [] {a : } {b : } (e : a b) :
@[reducible, inline]
abbrev Quiver.Hom.toPos {V : Type u_2} [] {X : V} {Y : V} (f : X Y) :
X Y

Shorthand for the "forward" arrow corresponding to f in symmetrify V

Equations
• f.toPos =
Instances For
@[reducible, inline]
abbrev Quiver.Hom.toNeg {V : Type u_2} [] {X : V} {Y : V} (f : X Y) :
Y X

Shorthand for the "backward" arrow corresponding to f in symmetrify V

Equations
• f.toNeg =
Instances For
def Quiver.Path.reverse {V : Type u_2} [] {a : V} {b : V} :

Reverse the direction of a path.

Equations
• Quiver.Path.nil.reverse = Quiver.Path.nil
• (p.cons e).reverse = ().toPath.comp p.reverse
Instances For
@[simp]
theorem Quiver.Path.reverse_toPath {V : Type u_2} [] {a : V} {b : V} (f : a b) :
f.toPath.reverse = ().toPath
@[simp]
theorem Quiver.Path.reverse_comp {V : Type u_2} [] {a : V} {b : V} {c : V} (p : ) (q : ) :
(p.comp q).reverse = q.reverse.comp p.reverse
@[simp]
theorem Quiver.Path.reverse_reverse {V : Type u_2} [] [h : ] {a : V} {b : V} (p : ) :
p.reverse.reverse = p
def Quiver.Symmetrify.of {V : Type u_2} [] :

The inclusion of a quiver in its symmetrification

Equations
• Quiver.Symmetrify.of = { obj := id, map := fun {X Y : V} => Sum.inl }
Instances For
def Quiver.Symmetrify.lift {V : Type u_2} [] {V' : Type u_4} [Quiver V'] [] (φ : V ⥤q V') :

Given a quiver V' with reversible arrows, a prefunctor to V' can be lifted to one from Symmetrify V to V'

Equations
• = { obj := φ.obj, map := fun {X Y : } (f : X Y) => match f with | => φ.map g | => Quiver.reverse (φ.map g) }
Instances For
theorem Quiver.Symmetrify.lift_spec {V : Type u_2} [] {V' : Type u_4} [Quiver V'] [] (φ : V ⥤q V') :
Quiver.Symmetrify.of ⋙q = φ
theorem Quiver.Symmetrify.lift_reverse {V : Type u_2} [] {V' : Type u_4} [Quiver V'] [h : ] (φ : V ⥤q V') {X : } {Y : } (f : X Y) :
.map () = Quiver.reverse (.map f)
theorem Quiver.Symmetrify.lift_unique {V : Type u_2} [] {V' : Type u_4} [Quiver V'] [] (φ : V ⥤q V') (Φ : ) (hΦ : Quiver.Symmetrify.of ⋙q Φ = φ) (hΦinv : ∀ {X Y : } (f : X Y), Φ.map () = Quiver.reverse (Φ.map f)) :

lift φ is the only prefunctor extending φ and preserving reverses.

@[simp]
theorem Prefunctor.symmetrify_obj {U : Type u_1} {V : Type u_2} [] [] (φ : U ⥤q V) :
∀ (a : U), φ.symmetrify.obj a = φ.obj a
@[simp]
theorem Prefunctor.symmetrify_map {U : Type u_1} {V : Type u_2} [] [] (φ : U ⥤q V) :
∀ {X Y : } (a : (X Y) (Y X)), φ.symmetrify.map a = Sum.map φ.map φ.map a
def Prefunctor.symmetrify {U : Type u_1} {V : Type u_2} [] [] (φ : U ⥤q V) :

A prefunctor canonically defines a prefunctor of the symmetrifications.

Equations
• φ.symmetrify = { obj := φ.obj, map := fun {X Y : } => Sum.map φ.map φ.map }
Instances For
instance Prefunctor.symmetrify_mapReverse {U : Type u_1} {V : Type u_2} [] [] (φ : U ⥤q V) :
φ.symmetrify.MapReverse
Equations
• =
instance Quiver.Push.instHasReverse {V : Type u_2} [] {V' : Type u_4} (σ : VV') :
Equations
• One or more equations did not get rendered due to their size.
instance Quiver.Push.instHasInvolutiveReverse {V : Type u_2} [] {V' : Type u_4} (σ : VV') [h : ] :
Equations
theorem Quiver.Push.of_reverse {V : Type u_2} [] {V' : Type u_4} (σ : VV') (X : V) (Y : V) (f : X Y) :
Quiver.reverse (().map f) = ().map ()
instance Quiver.Push.ofMapReverse {V : Type u_2} [] {V' : Type u_4} (σ : VV') [h : ] :
().MapReverse
Equations
• =
def Quiver.IsPreconnected (V : Type u_4) [] :

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
Instances For