# 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} (r : ) (A : Type w) [] [] :

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 gr (.map f) (.map g)

the condition that the relation is preserved by the shift

Instances
theorem HomRel.IsCompatibleWithShift.condition {C : Type u} {r : } {A : Type w} [] [] [self : r.IsCompatibleWithShift A] (a : A) ⦃X : C ⦃Y : C (f : X Y) (g : X Y) :
r f gr (.map f) (.map g)

the condition that the relation is preserved by the shift

@[irreducible]
noncomputable instance CategoryTheory.HasShift.quotient {C : Type u} (r : ) (A : Type w) [] [] [r.IsCompatibleWithShift 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} (r : ) (A : Type w) [] [] [r.IsCompatibleWithShift A] :
.CommShift 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.
@[irreducible]
noncomputable def CategoryTheory.Quotient.LiftCommShift.iso {C : Type u} {D : Type u'} [] (F : ) (r : ) {A : Type w} [] [] [] [r.IsCompatibleWithShift A] [F.CommShift A] (hF : ∀ (x y : C) (f₁ f₂ : x y), r f₁ f₂F.map f₁ = F.map f₂) (a : A) :
.comp () ().comp

Auxiliary definition for Quotient.liftCommShift.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Quotient.LiftCommShift.iso_hom_app {C : Type u} {D : Type u'} [] (F : ) (r : ) {A : Type w} [] [] [] [r.IsCompatibleWithShift A] [F.CommShift A] (hF : ∀ (x y : C) (f₁ f₂ : x y), r f₁ f₂F.map f₁ = F.map f₂) (a : A) (X : C) :
().hom.app (.obj X) = CategoryTheory.CategoryStruct.comp (().map ((.commShiftIso a).inv.app X)) ((F.commShiftIso a).hom.app X)
@[simp]
theorem CategoryTheory.Quotient.LiftCommShift.iso_inv_app {C : Type u} {D : Type u'} [] (F : ) (r : ) {A : Type w} [] [] [] [r.IsCompatibleWithShift A] [F.CommShift A] (hF : ∀ (x y : C) (f₁ f₂ : x y), r f₁ f₂F.map f₁ = F.map f₂) (a : A) (X : C) :
().inv.app (.obj X) = CategoryTheory.CategoryStruct.comp ((F.commShiftIso a).inv.app X) (().map ((.commShiftIso a).hom.app X))
noncomputable instance CategoryTheory.Quotient.liftCommShift {C : Type u} {D : Type u'} [] (F : ) (r : ) (A : Type w) [] [] [] [r.IsCompatibleWithShift A] [F.CommShift A] (hF : ∀ (x y : C) (f₁ f₂ : x y), r f₁ f₂F.map f₁ = F.map f₂) :
().CommShift A

When r : HomRel C is compatible with the shift by an additive monoid, and F : C ⥤ D is a functor which commutes with the shift and is compatible with r, then the induced functor Quotient.lift r F _ : Quotient r ⥤ D also commutes with the shift.

Equations
• = { iso := , zero := , add := }
instance CategoryTheory.Quotient.liftCommShift_compatibility {C : Type u} {D : Type u'} [] (F : ) (r : ) (A : Type w) [] [] [] [r.IsCompatibleWithShift A] [F.CommShift A] (hF : ∀ (x y : C) (f₁ f₂ : x y), r f₁ f₂F.map f₁ = F.map f₂) :
Equations
• =