# Documentation

Mathlib.CategoryTheory.Shift.Localization

# The shift induced on a localized category #

Let C be a category equipped with a shift by a monoid A. A morphism property W on C satisfies W.IsCompatibleWithShift A when for all a : A, a morphism f is in W iff f⟦a⟧' is. When this compatibility is satisfied, then the corresponding localized category can be equipped with a shift by A, and the localization functor is compatible with the shift.

• condition : ∀ (a : A),

the condition that for all a : A, the morphism property W is not changed when we take its inverse image by the shift functor by a

A morphism property W on a category C is compatible with the shift by a monoid A when for all a : A, a morphism f belongs to W if and only if f⟦a⟧' does.

Instances
theorem CategoryTheory.MorphismProperty.IsCompatibleWithShift.iff {C : Type u₁} [] {A : Type w} [] [] {X : C} {Y : C} (f : X Y) (a : A) :
W (().obj X) (().obj Y) (().map f) W X Y f
theorem CategoryTheory.MorphismProperty.IsCompatibleWithShift.shiftFunctor_comp_inverts {C : Type u₁} {D : Type u₂} [] [] (L : ) {A : Type w} [] [] (a : A) :
@[irreducible]
noncomputable def CategoryTheory.HasShift.localized {C : Type u₁} {D : Type u₂} [] [] (L : ) (A : Type w) [] [] :

When L : C ⥤ D is a localization functor with respect to a morphism property W that is compatible with the shift by a monoid A on C, this is the induced shift on the category D.

Instances For
@[irreducible]
noncomputable def CategoryTheory.Functor.CommShift.localized {C : Type u₁} {D : Type u₂} [] [] (L : ) (A : Type w) [] [] :

The localization functor L : C ⥤ D is compatible with the shift.

Instances For
@[irreducible]
noncomputable instance CategoryTheory.HasShift.localization {C : Type u₁} [] (A : Type w) [] [] :

The localized category W.Localization is endowed with the induced shift.

@[irreducible]
noncomputable instance CategoryTheory.MorphismProperty.commShift_Q {C : Type u₁} [] (A : Type w) [] [] :

The localization functor W.Q : C ⥤ W.Localization is compatible with the shift.