## 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`.

source
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

- Quiver.Symmetrify V = V

Instances For

source
instance Quiver.symmetrifyQuiver (V : Type u) [Quiver V] :
Quiver (Symmetrify V)
Equations

- Quiver.symmetrifyQuiver V = { Hom := fun (a b : V) => (a ⟶ b) ⊕ (b ⟶ a) }

source
class Quiver.HasReverse (V : Type u_2) [Quiver V] :
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

source
def Quiver.reverse {V : Type u_4} [Quiver V] [HasReverse V] {a b : V} :
(a ⟶ b) → (b ⟶ a)

Reverse the direction of an arrow.

Equations

- Quiver.reverse = Quiver.HasReverse.reverse'

Instances For

source
class Quiver.HasInvolutiveReverse (V : Type u_2) [Quiver V] extends Quiver.HasReverse V :
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 (reverse f) = f

  `reverse` is involutive

Instances

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

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.

Instances

source
@[simp]
theorem Prefunctor.map_reverse {U : Type u_1} {V : Type u_2} [Quiver U] [Quiver V] [Quiver.HasReverse U] [Quiver.HasReverse V] (φ : U ⥤q V) [φ.MapReverse] {u v : U} (e : u ⟶ v) :
φ.map (Quiver.reverse e) = Quiver.reverse (φ.map e)
source
instance Prefunctor.mapReverseComp {U : Type u_1} {V : Type u_2} {W : Type u_3} [Quiver U] [Quiver V] [Quiver W] [Quiver.HasReverse U] [Quiver.HasReverse V] [Quiver.HasReverse W] (φ : U ⥤q V) (ψ : V ⥤q W) [φ.MapReverse] [ψ.MapReverse] :
(φ ⋙q ψ).MapReverse
source
instance Prefunctor.mapReverseId {U : Type u_1} [Quiver U] [Quiver.HasReverse U] :
(𝟭q U).MapReverse
source
instance Quiver.instHasReverseSymmetrify {V : Type u_2} [Quiver V] :
HasReverse (Symmetrify V)
Equations

- Quiver.instHasReverseSymmetrify = { reverse' := fun {a b : Quiver.Symmetrify V} (e : a ⟶ b) => Sum.swap e }

source
instance Quiver.instHasInvolutiveReverseSymmetrify {V : Type u_2} [Quiver V] :
HasInvolutiveReverse (Symmetrify V)
Equations

- Quiver.instHasInvolutiveReverseSymmetrify = { reverse' := fun {a b : Quiver.Symmetrify V} (e : a ⟶ b) => Sum.swap e, inv' := ⋯ }

source
@[simp]
theorem Quiver.symmetrify_reverse {V : Type u_2} [Quiver V] {a b : Symmetrify V} (e : a ⟶ b) :
reverse e = Sum.swap e
source
@[reducible, inline]
abbrev Quiver.Hom.toPos {V : Type u_2} [Quiver V] {X Y : V} (f : X ⟶ Y) :
X ⟶ Y

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

Equations

- f.toPos = Sum.inl f

Instances For

source
@[reducible, inline]
abbrev Quiver.Hom.toNeg {V : Type u_2} [Quiver V] {X Y : V} (f : X ⟶ Y) :
Y ⟶ X

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

Equations

- f.toNeg = Sum.inr f

Instances For

source
def Quiver.Path.reverse {V : Type u_2} [Quiver V] [HasReverse V] {a b : V} :
Path a b → Path b a

Reverse the direction of a path.

Equations

- Quiver.Path.nil.reverse = Quiver.Path.nil
- (p.cons e).reverse = (Quiver.reverse e).toPath.comp p.reverse

Instances For

source
@[simp]
theorem Quiver.Path.reverse_toPath {V : Type u_2} [Quiver V] [HasReverse V] {a b : V} (f : a ⟶ b) :
f.toPath.reverse = (Quiver.reverse f).toPath
source
@[simp]
theorem Quiver.Path.reverse_comp {V : Type u_2} [Quiver V] [HasReverse V] {a b c : V} (p : Path a b) (q : Path b c) :
(p.comp q).reverse = q.reverse.comp p.reverse
source
@[simp]
theorem Quiver.Path.reverse_reverse {V : Type u_2} [Quiver V] [h : HasInvolutiveReverse V] {a b : V} (p : Path a b) :
p.reverse.reverse = p
source
def Quiver.Symmetrify.of {V : Type u_2} [Quiver V] :
V ⥤q Symmetrify V

The inclusion of a quiver in its symmetrification

Equations

- Quiver.Symmetrify.of = { obj := id, map := fun {X Y : V} => Sum.inl }

Instances For

source
@[simp]
theorem Quiver.Symmetrify.of_map {V : Type u_2} [Quiver V] {X✝ Y✝ : V} (val : X✝ ⟶ Y✝) :
of.map val = Sum.inl val
source
@[simp]
theorem Quiver.Symmetrify.of_obj {V : Type u_2} [Quiver V] (a : V) :
of.obj a = id a
source
def Quiver.Symmetrify.lift {V : Type u_2} [Quiver V] {V' : Type u_4} [Quiver V'] [HasReverse V'] (φ : V ⥤q V') :
Symmetrify 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

- Quiver.Symmetrify.lift φ = { obj := φ.obj, map := fun {X Y : Quiver.Symmetrify V} (x : X ⟶ Y) => match x with | Sum.inl g => φ.map g | Sum.inr g => Quiver.reverse (φ.map g) }

Instances For

source
theorem Quiver.Symmetrify.lift_spec {V : Type u_2} [Quiver V] {V' : Type u_4} [Quiver V'] [HasReverse V'] (φ : V ⥤q V') :
of ⋙q lift φ = φ
source
theorem Quiver.Symmetrify.lift_reverse {V : Type u_2} [Quiver V] {V' : Type u_4} [Quiver V'] [h : HasInvolutiveReverse V'] (φ : V ⥤q V') {X Y : Symmetrify V} (f : X ⟶ Y) :
(lift φ).map (reverse f) = reverse ((lift φ).map f)
source
theorem Quiver.Symmetrify.lift_unique {V : Type u_2} [Quiver V] {V' : Type u_4} [Quiver V'] [HasReverse V'] (φ : V ⥤q V') (Φ : Symmetrify V ⥤q V') (hΦ : of ⋙q Φ = φ) (hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)) :
Φ = lift φ

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

source
def Prefunctor.symmetrify {U : Type u_1} {V : Type u_2} [Quiver U] [Quiver V] (φ : U ⥤q V) :
Quiver.Symmetrify U ⥤q Quiver.Symmetrify V

A prefunctor canonically defines a prefunctor of the symmetrifications.

Equations

- φ.symmetrify = { obj := φ.obj, map := fun {X Y : Quiver.Symmetrify U} => Sum.map φ.map φ.map }

Instances For

source
@[simp]
theorem Prefunctor.symmetrify_obj {U : Type u_1} {V : Type u_2} [Quiver U] [Quiver V] (φ : U ⥤q V) (a✝ : U) :
φ.symmetrify.obj a✝ = φ.obj a✝
source
@[simp]
theorem Prefunctor.symmetrify_map {U : Type u_1} {V : Type u_2} [Quiver U] [Quiver V] (φ : U ⥤q V) {X✝ Y✝ : Quiver.Symmetrify U} (a✝ : (X✝ ⟶ Y✝) ⊕ (Y✝ ⟶ X✝)) :
φ.symmetrify.map a✝ = Sum.map φ.map φ.map a✝
source
instance Prefunctor.symmetrify_mapReverse {U : Type u_1} {V : Type u_2} [Quiver U] [Quiver V] (φ : U ⥤q V) :
φ.symmetrify.MapReverse
source
instance Quiver.Push.instHasReverse {V : Type u_2} [Quiver V] {V' : Type u_4} (σ : V → V') [HasReverse V] :
HasReverse (Push σ)
Equations

- One or more equations did not get rendered due to their size.

source
instance Quiver.Push.instHasInvolutiveReverse {V : Type u_2} [Quiver V] {V' : Type u_4} (σ : V → V') [h : HasInvolutiveReverse V] :
HasInvolutiveReverse (Push σ)
Equations

- One or more equations did not get rendered due to their size.

source
theorem Quiver.Push.of_reverse {V : Type u_2} [Quiver V] {V' : Type u_4} (σ : V → V') [HasInvolutiveReverse V] (X Y : V) (f : X ⟶ Y) :
reverse ((of σ).map f) = (of σ).map (reverse f)
source
instance Quiver.Push.ofMapReverse {V : Type u_2} [Quiver V] {V' : Type u_4} (σ : V → V') [h : HasInvolutiveReverse V] :
(of σ).MapReverse