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₁} [Category.{v₁, u₁} C] (W : MorphismProperty C) (A : Type w) [AddMonoid A] [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 (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₁} [Category.{v₁, u₁} C] (W : MorphismProperty C) {A : Type w} [AddMonoid A] [HasShift C A] [W.IsCompatibleWithShift A] {X Y : C} (f : X ⟶ Y) (a : A) : W ((shiftFunctor C a).map f) ↔ W f

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

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

@[reducible, inline]

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

The morphism of localizer from W to W given by the functor shiftFunctor C a when a : A and W is compatible with the shift by A.

Equations

• W.shiftLocalizerMorphism a = { functor := CategoryTheory.shiftFunctor C a, map := ⋯ }

@[irreducible]

noncomputable def CategoryTheory.HasShift.localized {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] (A : Type w) [AddMonoid A] [HasShift C A] [W.IsCompatibleWithShift A] : 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₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] (A : Type w) [AddMonoid A] [HasShift C A] [W.IsCompatibleWithShift A] : L.CommShift 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₁} [Category.{v₁, u₁} C] (W : MorphismProperty C) (A : Type w) [AddMonoid A] [HasShift C A] [W.IsCompatibleWithShift A] : HasShift W.Localization A

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

Equations

• CategoryTheory.HasShift.localization W A = CategoryTheory.HasShift.localized W.Q W A

@[irreducible]

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

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

Equations

• W.commShift_Q A = CategoryTheory.Functor.CommShift.localized W.Q W A

@[irreducible]

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

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

Equations

• CategoryTheory.HasShift.localization' W A = CategoryTheory.HasShift.localized W.Q' W A

@[irreducible]

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

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

Equations

• W.commShift_Q' A = CategoryTheory.Functor.CommShift.localized W.Q' W A

noncomputable def CategoryTheory.Functor.commShiftOfLocalization.iso {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] {A : Type w} [AddMonoid A] [HasShift C A] (F : Functor C E) (F' : Functor D E) [Localization.Lifting L W F F'] [HasShift D A] [HasShift E A] [L.CommShift A] [F.CommShift A] (a : A) : (shiftFunctor D a).comp F' ≅ F'.comp (shiftFunctor E a)

Auxiliary definition for Functor.commShiftOfLocalization.

Equations

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

@[simp]

theorem CategoryTheory.Functor.commShiftOfLocalization.iso_hom_app {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] {A : Type w} [AddMonoid A] [HasShift C A] (F : Functor C E) (F' : Functor D E) [Localization.Lifting L W F F'] [HasShift D A] [HasShift E A] [L.CommShift A] [F.CommShift A] (a : A) (X : C) : (iso L W F F' a).hom.app (L.obj X) = CategoryStruct.comp (F'.map ((L.commShiftIso a).inv.app X)) (CategoryStruct.comp ((Localization.Lifting.iso L W F F').hom.app ((shiftFunctor C a).obj X)) (CategoryStruct.comp ((F.commShiftIso a).hom.app X) ((shiftFunctor E a).map ((Localization.Lifting.iso L W F F').inv.app X))))

theorem CategoryTheory.Functor.commShiftOfLocalization.iso_hom_app_assoc {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] {A : Type w} [AddMonoid A] [HasShift C A] (F : Functor C E) (F' : Functor D E) [Localization.Lifting L W F F'] [HasShift D A] [HasShift E A] [L.CommShift A] [F.CommShift A] (a : A) (X : C) {Z : E} (h : (shiftFunctor E a).obj (F'.obj (L.obj X)) ⟶ Z) : CategoryStruct.comp ((iso L W F F' a).hom.app (L.obj X)) h = CategoryStruct.comp (F'.map ((L.commShiftIso a).inv.app X)) (CategoryStruct.comp ((Localization.Lifting.iso L W F F').hom.app ((shiftFunctor C a).obj X)) (CategoryStruct.comp ((F.commShiftIso a).hom.app X) (CategoryStruct.comp ((shiftFunctor E a).map ((Localization.Lifting.iso L W F F').inv.app X)) h)))

@[simp]

theorem CategoryTheory.Functor.commShiftOfLocalization.iso_inv_app {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] {A : Type w} [AddMonoid A] [HasShift C A] (F : Functor C E) (F' : Functor D E) [Localization.Lifting L W F F'] [HasShift D A] [HasShift E A] [L.CommShift A] [F.CommShift A] (a : A) (X : C) : (iso L W F F' a).inv.app (L.obj X) = CategoryStruct.comp ((shiftFunctor E a).map ((Localization.Lifting.iso L W F F').hom.app X)) (CategoryStruct.comp ((F.commShiftIso a).inv.app X) (CategoryStruct.comp ((Localization.Lifting.iso L W F F').inv.app ((shiftFunctor C a).obj X)) (F'.map ((L.commShiftIso a).hom.app X))))

theorem CategoryTheory.Functor.commShiftOfLocalization.iso_inv_app_assoc {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] {A : Type w} [AddMonoid A] [HasShift C A] (F : Functor C E) (F' : Functor D E) [Localization.Lifting L W F F'] [HasShift D A] [HasShift E A] [L.CommShift A] [F.CommShift A] (a : A) (X : C) {Z : E} (h : F'.obj ((shiftFunctor D a).obj (L.obj X)) ⟶ Z) : CategoryStruct.comp ((iso L W F F' a).inv.app (L.obj X)) h = CategoryStruct.comp ((shiftFunctor E a).map ((Localization.Lifting.iso L W F F').hom.app X)) (CategoryStruct.comp ((F.commShiftIso a).inv.app X) (CategoryStruct.comp ((Localization.Lifting.iso L W F F').inv.app ((shiftFunctor C a).obj X)) (CategoryStruct.comp (F'.map ((L.commShiftIso a).hom.app X)) h)))

noncomputable def CategoryTheory.Functor.commShiftOfLocalization {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] (A : Type w) [AddMonoid A] [HasShift C A] (F : Functor C E) (F' : Functor D E) [Localization.Lifting L W F F'] [HasShift D A] [HasShift E A] [L.CommShift A] [F.CommShift A] : F'.CommShift A

In the context of localization of categories, if a functor is induced by a functor which commutes with the shift, then this functor commutes with the shift.

Equations

• L.commShiftOfLocalization W A F F' = { iso := CategoryTheory.Functor.commShiftOfLocalization.iso L W F F', zero := ⋯, add := ⋯ }

theorem CategoryTheory.Functor.commShiftOfLocalization_iso_hom_app {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] {A : Type w} [AddMonoid A] [HasShift C A] (F : Functor C E) (F' : Functor D E) [Localization.Lifting L W F F'] [HasShift D A] [HasShift E A] [L.CommShift A] [F.CommShift A] (a : A) (X : C) : (F'.commShiftIso a).hom.app (L.obj X) = CategoryStruct.comp (F'.map ((L.commShiftIso a).inv.app X)) (CategoryStruct.comp ((Localization.Lifting.iso L W F F').hom.app ((shiftFunctor C a).obj X)) (CategoryStruct.comp ((F.commShiftIso a).hom.app X) ((shiftFunctor E a).map ((Localization.Lifting.iso L W F F').inv.app X))))

theorem CategoryTheory.Functor.commShiftOfLocalization_iso_inv_app {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] {A : Type w} [AddMonoid A] [HasShift C A] (F : Functor C E) (F' : Functor D E) [Localization.Lifting L W F F'] [HasShift D A] [HasShift E A] [L.CommShift A] [F.CommShift A] (a : A) (X : C) : (F'.commShiftIso a).inv.app (L.obj X) = CategoryStruct.comp ((shiftFunctor E a).map ((Localization.Lifting.iso L W F F').hom.app X)) (CategoryStruct.comp ((F.commShiftIso a).inv.app X) (CategoryStruct.comp ((Localization.Lifting.iso L W F F').inv.app ((shiftFunctor C a).obj X)) (F'.map ((L.commShiftIso a).hom.app X))))

instance CategoryTheory.NatTrans.commShift_iso_hom_of_localization {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] (A : Type w) [AddMonoid A] [HasShift C A] (F : Functor C E) (F' : Functor D E) [Localization.Lifting L W F F'] [HasShift D A] [HasShift E A] [L.CommShift A] [F.CommShift A] : CommShift (Localization.Lifting.iso L W F F').hom A