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.

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


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


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