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 ((commShiftIso L a).inv.app X)) (CategoryStruct.comp ((Localization.Lifting.iso L W F F').hom.app ((shiftFunctor C a).obj X)) (CategoryStruct.comp ((commShiftIso F 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 ((commShiftIso L a).inv.app X)) (CategoryStruct.comp ((Localization.Lifting.iso L W F F').hom.app ((shiftFunctor C a).obj X)) (CategoryStruct.comp ((commShiftIso F 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 ((commShiftIso F a).inv.app X) (CategoryStruct.comp ((Localization.Lifting.iso L W F F').inv.app ((shiftFunctor C a).obj X)) (F'.map ((commShiftIso L 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 ((commShiftIso F a).inv.app X) (CategoryStruct.comp ((Localization.Lifting.iso L W F F').inv.app ((shiftFunctor C a).obj X)) (CategoryStruct.comp (F'.map ((commShiftIso L 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' = { commShiftIso := CategoryTheory.Functor.commShiftOfLocalization.iso L W F F', commShiftIso_zero := ⋯, commShiftIso_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) : (commShiftIso F' a).hom.app (L.obj X) = CategoryStruct.comp (F'.map ((commShiftIso L a).inv.app X)) (CategoryStruct.comp ((Localization.Lifting.iso L W F F').hom.app ((shiftFunctor C a).obj X)) (CategoryStruct.comp ((commShiftIso F 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) : (commShiftIso 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 ((commShiftIso F a).inv.app X) (CategoryStruct.comp ((Localization.Lifting.iso L W F F').inv.app ((shiftFunctor C a).obj X)) (F'.map ((commShiftIso L 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

noncomputable def CategoryTheory.LocalizerMorphism.commShift {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_6, u_1} C₁] [Category.{u_7, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (M : Type u_3) [AddMonoid M] [HasShift C₁ M] [HasShift C₂ M] [Φ.functor.CommShift M] {D₁ : Type u_4} {D₂ : Type u_5} [Category.{u_8, u_4} D₁] [Category.{u_9, u_5} D₂] (L₁ : Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : Functor C₂ D₂) [HasShift D₁ M] [HasShift D₂ M] [L₁.CommShift M] [L₂.CommShift M] (G : Functor D₁ D₂) (e : Φ.functor.comp L₂ ≅ L₁.comp G) : G.CommShift M

This is the commutation of a functor G to shifts by an additive monoid M when e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G is an isomorphism, Φ is a localizer morphism and L₁ is a localization functor. We assume that all categories involved are equipped with shifts and that L₁, L₂ and Φ.functor commute to them.

Equations

• Φ.commShift M L₁ L₂ G e = L₁.commShiftOfLocalization W₁ M (Φ.functor.comp L₂) G

theorem CategoryTheory.LocalizerMorphism.commShift_iso_hom_app {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_8, u_1} C₁] [Category.{u_9, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) {M : Type u_3} [AddMonoid M] [HasShift C₁ M] [HasShift C₂ M] [Φ.functor.CommShift M] {D₁ : Type u_4} {D₂ : Type u_5} [Category.{u_7, u_4} D₁] [Category.{u_6, u_5} D₂] (L₁ : Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : Functor C₂ D₂) [HasShift D₁ M] [HasShift D₂ M] [L₁.CommShift M] [L₂.CommShift M] (G : Functor D₁ D₂) (e : Φ.functor.comp L₂ ≅ L₁.comp G) (m : M) (X : C₁) : (Functor.commShiftIso G m).hom.app (L₁.obj X) = CategoryStruct.comp (G.map ((Functor.commShiftIso L₁ m).inv.app X)) (CategoryStruct.comp (e.inv.app ((shiftFunctor C₁ m).obj X)) (CategoryStruct.comp (L₂.map ((Functor.commShiftIso Φ.functor m).hom.app X)) (CategoryStruct.comp ((Functor.commShiftIso L₂ m).hom.app (Φ.functor.obj X)) ((shiftFunctor D₂ m).map (e.hom.app X)))))

theorem CategoryTheory.LocalizerMorphism.commShift_iso_hom_app_assoc {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_8, u_1} C₁] [Category.{u_9, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) {M : Type u_3} [AddMonoid M] [HasShift C₁ M] [HasShift C₂ M] [Φ.functor.CommShift M] {D₁ : Type u_4} {D₂ : Type u_5} [Category.{u_7, u_4} D₁] [Category.{u_6, u_5} D₂] (L₁ : Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : Functor C₂ D₂) [HasShift D₁ M] [HasShift D₂ M] [L₁.CommShift M] [L₂.CommShift M] (G : Functor D₁ D₂) (e : Φ.functor.comp L₂ ≅ L₁.comp G) (m : M) (X : C₁) {Z : D₂} (h : (shiftFunctor D₂ m).obj (G.obj (L₁.obj X)) ⟶ Z) : CategoryStruct.comp ((Functor.commShiftIso G m).hom.app (L₁.obj X)) h = CategoryStruct.comp (G.map ((Functor.commShiftIso L₁ m).inv.app X)) (CategoryStruct.comp (e.inv.app ((shiftFunctor C₁ m).obj X)) (CategoryStruct.comp (L₂.map ((Functor.commShiftIso Φ.functor m).hom.app X)) (CategoryStruct.comp ((Functor.commShiftIso L₂ m).hom.app (Φ.functor.obj X)) (CategoryStruct.comp ((shiftFunctor D₂ m).map (e.hom.app X)) h))))

theorem CategoryTheory.LocalizerMorphism.commShift_iso_inv_app {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_8, u_1} C₁] [Category.{u_9, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) {M : Type u_3} [AddMonoid M] [HasShift C₁ M] [HasShift C₂ M] [Φ.functor.CommShift M] {D₁ : Type u_4} {D₂ : Type u_5} [Category.{u_7, u_4} D₁] [Category.{u_6, u_5} D₂] (L₁ : Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : Functor C₂ D₂) [HasShift D₁ M] [HasShift D₂ M] [L₁.CommShift M] [L₂.CommShift M] (G : Functor D₁ D₂) (e : Φ.functor.comp L₂ ≅ L₁.comp G) (m : M) (X : C₁) : (Functor.commShiftIso G m).inv.app (L₁.obj X) = CategoryStruct.comp ((shiftFunctor D₂ m).map (e.inv.app X)) (CategoryStruct.comp ((Functor.commShiftIso L₂ m).inv.app (Φ.functor.obj X)) (CategoryStruct.comp (L₂.map ((Functor.commShiftIso Φ.functor m).inv.app X)) (CategoryStruct.comp (e.hom.app ((shiftFunctor C₁ m).obj X)) (G.map ((Functor.commShiftIso L₁ m).hom.app X)))))

theorem CategoryTheory.LocalizerMorphism.commShift_iso_inv_app_assoc {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_8, u_1} C₁] [Category.{u_9, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) {M : Type u_3} [AddMonoid M] [HasShift C₁ M] [HasShift C₂ M] [Φ.functor.CommShift M] {D₁ : Type u_4} {D₂ : Type u_5} [Category.{u_7, u_4} D₁] [Category.{u_6, u_5} D₂] (L₁ : Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : Functor C₂ D₂) [HasShift D₁ M] [HasShift D₂ M] [L₁.CommShift M] [L₂.CommShift M] (G : Functor D₁ D₂) (e : Φ.functor.comp L₂ ≅ L₁.comp G) (m : M) (X : C₁) {Z : D₂} (h : G.obj ((shiftFunctor D₁ m).obj (L₁.obj X)) ⟶ Z) : CategoryStruct.comp ((Functor.commShiftIso G m).inv.app (L₁.obj X)) h = CategoryStruct.comp ((shiftFunctor D₂ m).map (e.inv.app X)) (CategoryStruct.comp ((Functor.commShiftIso L₂ m).inv.app (Φ.functor.obj X)) (CategoryStruct.comp (L₂.map ((Functor.commShiftIso Φ.functor m).inv.app X)) (CategoryStruct.comp (e.hom.app ((shiftFunctor C₁ m).obj X)) (CategoryStruct.comp (G.map ((Functor.commShiftIso L₁ m).hom.app X)) h))))

theorem CategoryTheory.LocalizerMorphism.natTransCommShift_hom {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_6, u_1} C₁] [Category.{u_8, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) {M : Type u_3} [AddMonoid M] [HasShift C₁ M] [HasShift C₂ M] [Φ.functor.CommShift M] {D₁ : Type u_4} {D₂ : Type u_5} [Category.{u_9, u_4} D₁] [Category.{u_7, u_5} D₂] (L₁ : Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : Functor C₂ D₂) [HasShift D₁ M] [HasShift D₂ M] [L₁.CommShift M] [L₂.CommShift M] (G : Functor D₁ D₂) (e : Φ.functor.comp L₂ ≅ L₁.comp G) : NatTrans.CommShift e.hom M

noncomputable instance CategoryTheory.LocalizerMorphism.instCommShiftLocalizedFunctor {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_6, u_1} C₁] [Category.{u_7, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) {M : Type u_3} [AddMonoid M] [HasShift C₁ M] [HasShift C₂ M] [Φ.functor.CommShift M] {D₁ : Type u_4} {D₂ : Type u_5} [Category.{u_8, u_4} D₁] [Category.{u_9, u_5} D₂] (L₁ : Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : Functor C₂ D₂) [HasShift D₁ M] [HasShift D₂ M] [L₁.CommShift M] [L₂.CommShift M] [L₂.IsLocalization W₂] : (Φ.localizedFunctor L₁ L₂).CommShift M

Equations

• Φ.instCommShiftLocalizedFunctor L₁ L₂ = Φ.commShift M L₁ L₂ (Φ.localizedFunctor L₁ L₂) (CategoryTheory.CatCommSq.iso Φ.functor L₁ L₂ (Φ.localizedFunctor L₁ L₂))

instance CategoryTheory.LocalizerMorphism.instCommShiftLocalizationHomFunctorIsoFunctorQLocalizedFunctor {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_6, u_1} C₁] [Category.{u_7, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) {M : Type u_3} [AddMonoid M] [HasShift C₁ M] [HasShift C₂ M] [Φ.functor.CommShift M] [W₁.IsCompatibleWithShift M] [W₂.IsCompatibleWithShift M] : NatTrans.CommShift (CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).hom M