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.

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

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.

• condition : ∀ (a : A), CategoryTheory.MorphismProperty.inverseImage W (CategoryTheory.shiftFunctor C a) = W

  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

theorem CategoryTheory.MorphismProperty.IsCompatibleWithShift.iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.MorphismProperty.IsCompatibleWithShift W A] {X : C} {Y : C} (f : X ⟶ Y) (a : A) : W ((CategoryTheory.shiftFunctor C a).toPrefunctor.map f) ↔ W f

theorem CategoryTheory.MorphismProperty.IsCompatibleWithShift.shiftFunctor_comp_inverts {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [CategoryTheory.Functor.IsLocalization L W] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.MorphismProperty.IsCompatibleWithShift W A] (a : A) : CategoryTheory.MorphismProperty.IsInvertedBy W (CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C a) L)

@[irreducible]

noncomputable def CategoryTheory.HasShift.localized {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [CategoryTheory.Functor.IsLocalization L W] (A : Type w) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.MorphismProperty.IsCompatibleWithShift W A] : CategoryTheory.HasShift D A

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.

Equations

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

@[irreducible]

noncomputable def CategoryTheory.Functor.CommShift.localized {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [CategoryTheory.Functor.IsLocalization L W] (A : Type w) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.MorphismProperty.IsCompatibleWithShift W A] : CategoryTheory.Functor.CommShift L A

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

Equations

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

@[irreducible]

noncomputable instance CategoryTheory.HasShift.localization {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) (A : Type w) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.MorphismProperty.IsCompatibleWithShift W A] : CategoryTheory.HasShift (CategoryTheory.MorphismProperty.Localization W) A

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

Equations

• CategoryTheory.HasShift.localization W A = CategoryTheory.HasShift.localized (CategoryTheory.MorphismProperty.Q W) W A

@[irreducible]

noncomputable instance CategoryTheory.MorphismProperty.commShift_Q {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) (A : Type w) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.MorphismProperty.IsCompatibleWithShift W A] : CategoryTheory.Functor.CommShift (CategoryTheory.MorphismProperty.Q W) A

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

Equations

• CategoryTheory.MorphismProperty.commShift_Q W A = CategoryTheory.Functor.CommShift.localized (CategoryTheory.MorphismProperty.Q W) W A