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.

ink

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

ink

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

Equations

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

ink

class Quiver.HasReverse (V : Type u_1) [inst : Quiver V] : Type (maxu_1v)

• the map which sends an arrow to its reverse

  reverse' : {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.

ink

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

Reverse the direction of an arrow.

Equations

• Quiver.reverse = Quiver.HasReverse.reverse'

ink

class Quiver.HasInvolutiveReverse (V : Type u_1) [inst : Quiver V] extends Quiver.HasReverse : Type (maxu_1v)

• reverse is involutive

  inv' : ∀ {a b : V} (f : a ⟶ b), Quiver.reverse (Quiver.reverse f) = f

A quiver HasInvolutiveReverse if reversing twice is the identity.`

ink

@[simp]

theorem Quiver.reverse_reverse {V : Type u_1} [inst : Quiver V] [h : Quiver.HasInvolutiveReverse V] {a : V} {b : V} (f : a ⟶ b) : Quiver.reverse (Quiver.reverse f) = f

ink

@[simp]

theorem Quiver.reverse_inj {V : Type u_1} [inst : Quiver V] [h : Quiver.HasInvolutiveReverse V] {a : V} {b : V} (f : a ⟶ b) (g : a ⟶ b) : Quiver.reverse f = Quiver.reverse g ↔ f = g

ink

theorem Quiver.eq_reverse_iff {V : Type u_1} [inst : Quiver V] [h : Quiver.HasInvolutiveReverse V] {a : V} {b : V} (f : a ⟶ b) (g : b ⟶ a) : f = Quiver.reverse g ↔ Quiver.reverse f = g

ink

class Prefunctor.MapReverse {U : Type u_1} {V : Type u_2} [inst : Quiver U] [inst : Quiver V] [inst : Quiver.HasReverse U] [inst : Quiver.HasReverse V] (φ : U ⥤q V) : Type

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

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

A prefunctor preserving reversal of arrows

ink

@[simp]

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

ink

instance Prefunctor.mapReverseComp {U : Type u_1} {V : Type u_2} {W : Type u_3} [inst : Quiver U] [inst : Quiver V] [inst : Quiver W] [inst : Quiver.HasReverse U] [inst : Quiver.HasReverse V] [inst : Quiver.HasReverse W] (φ : U ⥤q V) (ψ : V ⥤q W) [inst : Prefunctor.MapReverse φ] [inst : Prefunctor.MapReverse ψ] : Prefunctor.MapReverse (φ ⋙q ψ)

Equations

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

ink

instance Prefunctor.mapReverseId {U : Type u_1} [inst : Quiver U] [inst : Quiver.HasReverse U] : Prefunctor.MapReverse (𝟭q U)

Equations

• Prefunctor.mapReverseId = { map_reverse' := (_ : ∀ {u v : U} (x : u ⟶ v), Prefunctor.map (𝟭q U) (Quiver.reverse x) = Prefunctor.map (𝟭q U) (Quiver.reverse x)) }

ink

instance Quiver.instHasReverseSymmetrifySymmetrifyQuiver {V : Type u_1} [inst : Quiver V] : Quiver.HasReverse (Quiver.Symmetrify V)

Equations

• Quiver.instHasReverseSymmetrifySymmetrifyQuiver = { reverse' := fun {a b} e => Sum.swap e }

ink

instance Quiver.instHasInvolutiveReverseSymmetrifySymmetrifyQuiver {V : Type u_1} [inst : Quiver V] : Quiver.HasInvolutiveReverse (Quiver.Symmetrify V)

Equations

• Quiver.instHasInvolutiveReverseSymmetrifySymmetrifyQuiver = Quiver.HasInvolutiveReverse.mk (_ : ∀ {a b : Quiver.Symmetrify V} (e : a ⟶ b), (Sum.swap ∘ Sum.swap) e = id e)

ink

@[simp]

theorem Quiver.symmetrify_reverse {V : Type u_1} [inst : Quiver V] {a : Quiver.Symmetrify V} {b : Quiver.Symmetrify V} (e : a ⟶ b) : Quiver.reverse e = Sum.swap e

ink

@[inline]

abbrev Quiver.Hom.toPos {V : Type u_1} [inst : Quiver V] {X : V} {Y : V} (f : X ⟶ Y) : X ⟶ Y

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

Equations

• Quiver.Hom.toPos f = Sum.inl f

ink

@[inline]

abbrev Quiver.Hom.toNeg {V : Type u_1} [inst : Quiver V] {X : V} {Y : V} (f : X ⟶ Y) : Y ⟶ X

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

Equations

• Quiver.Hom.toNeg f = Sum.inr f

ink

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

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)

ink

@[simp]

theorem Quiver.Path.reverse_toPath {V : Type u_1} [inst : Quiver V] [inst : Quiver.HasReverse V] {a : V} {b : V} (f : a ⟶ b) : Quiver.Path.reverse (Quiver.Hom.toPath f) = Quiver.Hom.toPath (Quiver.reverse f)

ink

@[simp]

theorem Quiver.Path.reverse_comp {V : Type u_1} [inst : Quiver V] [inst : Quiver.HasReverse V] {a : V} {b : V} {c : V} (p : Quiver.Path a b) (q : Quiver.Path b c) : Quiver.Path.reverse (Quiver.Path.comp p q) = Quiver.Path.comp (Quiver.Path.reverse q) (Quiver.Path.reverse p)

ink

@[simp]

theorem Quiver.Path.reverse_reverse {V : Type u_1} [inst : Quiver V] [h : Quiver.HasInvolutiveReverse V] {a : V} {b : V} (p : Quiver.Path a b) : Quiver.Path.reverse (Quiver.Path.reverse p) = p

ink

def Quiver.Symmetrify.of {V : Type u_1} [inst : Quiver V] : V ⥤q Quiver.Symmetrify V

The inclusion of a quiver in its symmetrification

Equations

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

ink

def Quiver.Symmetrify.lift {V : Type u_1} [inst : Quiver V] {V' : Type u_2} [inst : Quiver V'] [inst : Quiver.HasReverse V'] (φ : V ⥤q V') : Quiver.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} f => match f with | Sum.inl g => Prefunctor.map φ g | Sum.inr g => Quiver.reverse (Prefunctor.map φ g) }

ink

theorem Quiver.Symmetrify.lift_spec {V : Type u_2} [inst : Quiver V] {V' : Type u_1} [inst : Quiver V'] [inst : Quiver.HasReverse V'] (φ : V ⥤q V') : Quiver.Symmetrify.of ⋙q Quiver.Symmetrify.lift φ = φ

ink

theorem Quiver.Symmetrify.lift_reverse {V : Type u_2} [inst : Quiver V] {V' : Type u_1} [inst : Quiver V'] [h : Quiver.HasInvolutiveReverse V'] (φ : V ⥤q V') {X : Quiver.Symmetrify V} {Y : Quiver.Symmetrify V} (f : X ⟶ Y) : Prefunctor.map (Quiver.Symmetrify.lift φ) (Quiver.reverse f) = Quiver.reverse (Prefunctor.map (Quiver.Symmetrify.lift φ) f)

ink

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

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

ink

instance Quiver.Push.instHasReversePushInstQuiverPush {V : Type u_1} [inst : Quiver V] {V' : Type u_2} (σ : V → V') [inst : Quiver.HasReverse V] : Quiver.HasReverse (Quiver.Push σ)

Equations

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

ink

instance Quiver.Push.instHasInvolutiveReversePushInstQuiverPush {V : Type u_1} [inst : Quiver V] {V' : Type u_2} (σ : V → V') [h : Quiver.HasInvolutiveReverse V] : Quiver.HasInvolutiveReverse (Quiver.Push σ)

Equations

• Quiver.Push.instHasInvolutiveReversePushInstQuiverPush σ = Quiver.HasInvolutiveReverse.mk (_ : ∀ {a b : Quiver.Push σ} (x : a ⟶ b), Quiver.reverse (Quiver.reverse x) = x)

ink

theorem Quiver.Push.of_reverse {V : Type u_1} [inst : Quiver V] {V' : Type u_2} (σ : V → V') [inst : Quiver.HasInvolutiveReverse V] (X : V) (Y : V) (f : X ⟶ Y) : Quiver.reverse (Prefunctor.map (Quiver.Push.of σ) f) = Prefunctor.map (Quiver.Push.of σ) (Quiver.reverse f)

ink

instance Quiver.Push.ofMapReverse {V : Type u_1} [inst : Quiver V] {V' : Type u_2} (σ : V → V') [h : Quiver.HasInvolutiveReverse V] : Prefunctor.MapReverse (Quiver.Push.of σ)

Equations

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

ink

def Quiver.IsPreconnected (V : Type u_1) [inst : Quiver V] : Prop

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 simple_graph, 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)