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), 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

theorem CategoryTheory.MorphismProperty.IsCompatibleWithShift.condition {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {W : CategoryTheory.MorphismProperty C} {A : Type w} {inst_1 : AddMonoid A} {inst_2 : 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

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

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)

theorem CategoryTheory.MorphismProperty.shift {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} (hf : W f) (a : A) : W ((CategoryTheory.shiftFunctor C a).map f)

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.shiftLocalizerMorphism {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [W.IsCompatibleWithShift A] (a : A) : CategoryTheory.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₂} [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

• 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) [L.IsLocalization W] (A : Type w) [AddMonoid A] [CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) (A : Type w) [AddMonoid A] [CategoryTheory.HasShift C A] [W.IsCompatibleWithShift A] : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) (A : Type w) [AddMonoid A] [CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) (A : Type w) [AddMonoid A] [CategoryTheory.HasShift C A] [W.IsCompatibleWithShift A] [W.HasLocalization] : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) (A : Type w) [AddMonoid A] [CategoryTheory.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₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] (F : CategoryTheory.Functor C E) (F' : CategoryTheory.Functor D E) [CategoryTheory.Localization.Lifting L W F F'] [CategoryTheory.HasShift D A] [CategoryTheory.HasShift E A] [L.CommShift A] [F.CommShift A] (a : A) : (CategoryTheory.shiftFunctor D a).comp F' ≅ F'.comp (CategoryTheory.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₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] (F : CategoryTheory.Functor C E) (F' : CategoryTheory.Functor D E) [CategoryTheory.Localization.Lifting L W F F'] [CategoryTheory.HasShift D A] [CategoryTheory.HasShift E A] [L.CommShift A] [F.CommShift A] (a : A) (X : C) : (CategoryTheory.Functor.commShiftOfLocalization.iso L W F F' a).hom.app (L.obj X) = CategoryTheory.CategoryStruct.comp (F'.map ((L.commShiftIso a).inv.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Localization.Lifting.iso L W F F').hom.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp ((F.commShiftIso a).hom.app X) ((CategoryTheory.shiftFunctor E a).map ((CategoryTheory.Localization.Lifting.iso L W F F').inv.app X))))

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

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

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

Equations

• ⋯ = ⋯