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.

source

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), W.inverseImage (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

Instances

source

theorem CategoryTheory.MorphismProperty.IsCompatibleWithShift.condition {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [self : W.IsCompatibleWithShift A] (a : A) :

W.inverseImage (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

source

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] [W.IsCompatibleWithShift A] {X : C} {Y : C} (f : X ⟶ Y) (a : A) :

W ((CategoryTheory.shiftFunctor C a).map f) ↔ W f

source

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) [L.IsLocalization W] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [W.IsCompatibleWithShift A] (a : A) :

W.IsInvertedBy ((CategoryTheory.shiftFunctor C a).comp L)

source

@[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) [L.IsLocalization W] (A : Type w) [AddMonoid A] [CategoryTheory.HasShift C A] [W.IsCompatibleWithShift 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