The shift on a quotient category

Let C be a category equipped a shift by a monoid A. If we have a relation on morphisms r : HomRel C that is compatible with the shift (i.e. if two morphisms f and g are related, then f⟦a⟧' and g⟦a⟧' are also related for all a : A), then the quotient category Quotient r is equipped with a shift.

The condition r.IsCompatibleWithShift A on the relation r is a class so that the shift can be automatically infered on the quotient category.

class HomRel.IsCompatibleWithShift {C : Type u} [CategoryTheory.Category.{v, u} C] (r : HomRel C) (A : Type w) [AddMonoid A] [CategoryTheory.HasShift C A] : Prop

A relation on morphisms is compatible with the shift by a monoid A when the relation if preserved by the shift.

• condition : ∀ (a : A) ⦃X Y : C⦄ (f g : X ⟶ Y), r f g → r ((CategoryTheory.shiftFunctor C a).toPrefunctor.map f) ((CategoryTheory.shiftFunctor C a).toPrefunctor.map g)

  the condition that the relation is preserved by the shift

@[irreducible]

noncomputable instance CategoryTheory.HasShift.quotient {C : Type u} [CategoryTheory.Category.{v, u} C] (r : HomRel C) (A : Type w) [AddMonoid A] [CategoryTheory.HasShift C A] [HomRel.IsCompatibleWithShift r A] : CategoryTheory.HasShift (CategoryTheory.Quotient r) A

The shift by a monoid A induced on a quotient category Quotient r when the relation r is compatible with the shift.

Equations

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

@[irreducible]

noncomputable instance CategoryTheory.Quotient.functor_commShift {C : Type u} [CategoryTheory.Category.{v, u} C] (r : HomRel C) (A : Type w) [AddMonoid A] [CategoryTheory.HasShift C A] [HomRel.IsCompatibleWithShift r A] : CategoryTheory.Functor.CommShift (CategoryTheory.Quotient.functor r) A

The functor Quotient.functor r : C ⥤ Quotient r commutes with the shift.

Equations

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