Functors which commute with shifts

Let C and D be two categories equipped with shifts by an additive monoid A. In this file, we define the notion of functor F : C ⥤ D which "commutes" with these shifts. The associated type class is [F.CommShift A]. The data consists of commutation isomorphisms F.commShiftIso a : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a for all a : A which satisfy a compatibility with the addition and the zero. After this was formalised in Lean, it was found that this definition is exactly the definition which appears in Jean-Louis Verdier's thesis (I 1.2.3/1.2.4), although the language is different. (In Verdier's thesis, the shift is not given by a monoidal functor Discrete A ⥤ C ⥤ C, but by a fibred category C ⥤ BA, where BA is the category with one object, the endomorphisms of which identify to A. The choice of a cleavage for this fibered category gives the individual shift functors.)

References

• Jean-Louis Verdier, Des catégories dérivées des catégories abéliennes

noncomputable def CategoryTheory.Functor.CommShift.isoZero {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] (F : CategoryTheory.Functor C D) (A : Type u_4) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] : (CategoryTheory.shiftFunctor C 0).comp F ≅ F.comp (CategoryTheory.shiftFunctor D 0)

For any functor F : C ⥤ D, this is the obvious isomorphism shiftFunctor C (0 : A) ⋙ F ≅ F ⋙ shiftFunctor D (0 : A) deduced from the isomorphisms shiftFunctorZero on both categories C and D.

Equations

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

@[simp]

theorem CategoryTheory.Functor.CommShift.isoZero_hom_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] (F : CategoryTheory.Functor C D) (A : Type u_4) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] (X : C) : (CategoryTheory.Functor.CommShift.isoZero F A).hom.app X = CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorZero C A).hom.app X)) ((CategoryTheory.shiftFunctorZero D A).inv.app (F.obj X))

@[simp]

theorem CategoryTheory.Functor.CommShift.isoZero_inv_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] (F : CategoryTheory.Functor C D) (A : Type u_4) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] (X : C) : (CategoryTheory.Functor.CommShift.isoZero F A).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero D A).hom.app (F.obj X)) (F.map ((CategoryTheory.shiftFunctorZero C A).inv.app X))

noncomputable def CategoryTheory.Functor.CommShift.isoAdd' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] {F : CategoryTheory.Functor C D} {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] {a b c : A} (h : a + b = c) (e₁ : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)) (e₂ : (CategoryTheory.shiftFunctor C b).comp F ≅ F.comp (CategoryTheory.shiftFunctor D b)) : (CategoryTheory.shiftFunctor C c).comp F ≅ F.comp (CategoryTheory.shiftFunctor D c)

If a functor F : C ⥤ D is equipped with "commutation isomorphisms" with the shifts by a and b, then there is a commutation isomorphism with the shift by c when a + b = c.

Equations

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

@[simp]

theorem CategoryTheory.Functor.CommShift.isoAdd'_inv_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] {F : CategoryTheory.Functor C D} {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] {a b c : A} (h : a + b = c) (e₁ : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)) (e₂ : (CategoryTheory.shiftFunctor C b).comp F ≅ F.comp (CategoryTheory.shiftFunctor D b)) (X : C) : (CategoryTheory.Functor.CommShift.isoAdd' h e₁ e₂).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' D a b c h).hom.app (F.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map (e₁.inv.app X)) (CategoryTheory.CategoryStruct.comp (e₂.inv.app ((CategoryTheory.shiftFunctor C a).obj X)) (F.map ((CategoryTheory.shiftFunctorAdd' C a b c h).inv.app X))))

@[simp]

theorem CategoryTheory.Functor.CommShift.isoAdd'_hom_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] {F : CategoryTheory.Functor C D} {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] {a b c : A} (h : a + b = c) (e₁ : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)) (e₂ : (CategoryTheory.shiftFunctor C b).comp F ≅ F.comp (CategoryTheory.shiftFunctor D b)) (X : C) : (CategoryTheory.Functor.CommShift.isoAdd' h e₁ e₂).hom.app X = CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorAdd' C a b c h).hom.app X)) (CategoryTheory.CategoryStruct.comp (e₂.hom.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map (e₁.hom.app X)) ((CategoryTheory.shiftFunctorAdd' D a b c h).inv.app (F.obj X))))

noncomputable def CategoryTheory.Functor.CommShift.isoAdd {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] {F : CategoryTheory.Functor C D} {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] {a b : A} (e₁ : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)) (e₂ : (CategoryTheory.shiftFunctor C b).comp F ≅ F.comp (CategoryTheory.shiftFunctor D b)) : (CategoryTheory.shiftFunctor C (a + b)).comp F ≅ F.comp (CategoryTheory.shiftFunctor D (a + b))

If a functor F : C ⥤ D is equipped with "commutation isomorphisms" with the shifts by a and b, then there is a commutation isomorphism with the shift by a + b.

Equations

• CategoryTheory.Functor.CommShift.isoAdd e₁ e₂ = CategoryTheory.Functor.CommShift.isoAdd' ⋯ e₁ e₂

@[simp]

theorem CategoryTheory.Functor.CommShift.isoAdd_hom_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {F : CategoryTheory.Functor C D} {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] {a b : A} (e₁ : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)) (e₂ : (CategoryTheory.shiftFunctor C b).comp F ≅ F.comp (CategoryTheory.shiftFunctor D b)) (X : C) : (CategoryTheory.Functor.CommShift.isoAdd e₁ e₂).hom.app X = CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorAdd C a b).hom.app X)) (CategoryTheory.CategoryStruct.comp (e₂.hom.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map (e₁.hom.app X)) ((CategoryTheory.shiftFunctorAdd D a b).inv.app (F.obj X))))

@[simp]

theorem CategoryTheory.Functor.CommShift.isoAdd_inv_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {F : CategoryTheory.Functor C D} {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] {a b : A} (e₁ : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)) (e₂ : (CategoryTheory.shiftFunctor C b).comp F ≅ F.comp (CategoryTheory.shiftFunctor D b)) (X : C) : (CategoryTheory.Functor.CommShift.isoAdd e₁ e₂).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd D a b).hom.app (F.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map (e₁.inv.app X)) (CategoryTheory.CategoryStruct.comp (e₂.inv.app ((CategoryTheory.shiftFunctor C a).obj X)) (F.map ((CategoryTheory.shiftFunctorAdd C a b).inv.app X))))

class CategoryTheory.Functor.CommShift {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] (F : CategoryTheory.Functor C D) (A : Type u_4) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] : Type (max (max u_1 u_4) u_7)

A functor F commutes with the shift by a monoid A if it is equipped with commutation isomorphisms with the shifts by all a : A, and these isomorphisms satisfy coherence properties with respect to 0 : A and the addition in A.

• iso : (a : A) → (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)
• zero : CategoryTheory.Functor.CommShift.iso 0 = CategoryTheory.Functor.CommShift.isoZero F A
• add : ∀ (a b : A), CategoryTheory.Functor.CommShift.iso (a + b) = CategoryTheory.Functor.CommShift.isoAdd (CategoryTheory.Functor.CommShift.iso a) (CategoryTheory.Functor.CommShift.iso b)

def CategoryTheory.Functor.commShiftIso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.CommShift A] (a : A) : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)

If a functor F commutes with the shift by A (i.e. [F.CommShift A]), then F.commShiftIso a is the given isomorphism shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a.

Equations

• F.commShiftIso a = CategoryTheory.Functor.CommShift.iso a

@[simp]

theorem CategoryTheory.Functor.commShiftIso_hom_naturality {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.CommShift A] {X Y : C} (f : X ⟶ Y) (a : A) : CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor C a).map f)) ((F.commShiftIso a).hom.app Y) = CategoryTheory.CategoryStruct.comp ((F.commShiftIso a).hom.app X) ((CategoryTheory.shiftFunctor D a).map (F.map f))

@[simp]

theorem CategoryTheory.Functor.commShiftIso_hom_naturality_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.CommShift A] {X Y : C} (f : X ⟶ Y) (a : A) {Z : D} (h : (CategoryTheory.shiftFunctor D a).obj (F.obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor C a).map f)) (CategoryTheory.CategoryStruct.comp ((F.commShiftIso a).hom.app Y) h) = CategoryTheory.CategoryStruct.comp ((F.commShiftIso a).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (F.map f)) h)

@[simp]

theorem CategoryTheory.Functor.commShiftIso_inv_naturality {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.CommShift A] {X Y : C} (f : X ⟶ Y) (a : A) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (F.map f)) ((F.commShiftIso a).inv.app Y) = CategoryTheory.CategoryStruct.comp ((F.commShiftIso a).inv.app X) (F.map ((CategoryTheory.shiftFunctor C a).map f))

@[simp]

theorem CategoryTheory.Functor.commShiftIso_inv_naturality_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.CommShift A] {X Y : C} (f : X ⟶ Y) (a : A) {Z : D} (h : F.obj ((CategoryTheory.shiftFunctor C a).obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (F.map f)) (CategoryTheory.CategoryStruct.comp ((F.commShiftIso a).inv.app Y) h) = CategoryTheory.CategoryStruct.comp ((F.commShiftIso a).inv.app X) (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor C a).map f)) h)

theorem CategoryTheory.Functor.commShiftIso_zero {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] (F : CategoryTheory.Functor C D) (A : Type u_4) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.CommShift A] : F.commShiftIso 0 = CategoryTheory.Functor.CommShift.isoZero F A

theorem CategoryTheory.Functor.commShiftIso_add {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.CommShift A] (a b : A) : F.commShiftIso (a + b) = CategoryTheory.Functor.CommShift.isoAdd (F.commShiftIso a) (F.commShiftIso b)

theorem CategoryTheory.Functor.commShiftIso_add' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.CommShift A] {a b c : A} (h : a + b = c) : F.commShiftIso c = CategoryTheory.Functor.CommShift.isoAdd' h (F.commShiftIso a) (F.commShiftIso b)

instance CategoryTheory.Functor.CommShift.id (C : Type u_1) [CategoryTheory.Category.{u_6, u_1} C] {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] : (CategoryTheory.Functor.id C).CommShift A

Equations

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

instance CategoryTheory.Functor.CommShift.comp {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] [CategoryTheory.Category.{u_8, u_3} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [CategoryTheory.HasShift E A] [F.CommShift A] [G.CommShift A] : (F.comp G).CommShift A

Equations

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

@[simp]

theorem CategoryTheory.Functor.commShiftIso_id_hom_app {C : Type u_1} [CategoryTheory.Category.{u_6, u_1} C] {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] (a : A) (X : C) : ((CategoryTheory.Functor.id C).commShiftIso a).hom.app X = CategoryTheory.CategoryStruct.id (((CategoryTheory.shiftFunctor C a).comp (CategoryTheory.Functor.id C)).obj X)

@[simp]

theorem CategoryTheory.Functor.commShiftIso_id_inv_app {C : Type u_1} [CategoryTheory.Category.{u_6, u_1} C] {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] (a : A) (X : C) : ((CategoryTheory.Functor.id C).commShiftIso a).inv.app X = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.id C).comp (CategoryTheory.shiftFunctor C a)).obj X)

theorem CategoryTheory.Functor.commShiftIso_comp_hom_app {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] [CategoryTheory.Category.{u_8, u_3} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [CategoryTheory.HasShift E A] [F.CommShift A] [G.CommShift A] (a : A) (X : C) : ((F.comp G).commShiftIso a).hom.app X = CategoryTheory.CategoryStruct.comp (G.map ((F.commShiftIso a).hom.app X)) ((G.commShiftIso a).hom.app (F.obj X))

theorem CategoryTheory.Functor.commShiftIso_comp_inv_app {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] [CategoryTheory.Category.{u_8, u_3} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [CategoryTheory.HasShift E A] [F.CommShift A] [G.CommShift A] (a : A) (X : C) : ((F.comp G).commShiftIso a).inv.app X = CategoryTheory.CategoryStruct.comp ((G.commShiftIso a).inv.app (F.obj X)) (G.map ((F.commShiftIso a).inv.app X))

theorem CategoryTheory.Functor.map_shiftFunctorComm_hom_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] (F : CategoryTheory.Functor C D) {B : Type u_5} [AddCommMonoid B] [CategoryTheory.HasShift C B] [CategoryTheory.HasShift D B] [F.CommShift B] (X : C) (a b : B) : F.map ((CategoryTheory.shiftFunctorComm C a b).hom.app X) = CategoryTheory.CategoryStruct.comp ((F.commShiftIso b).hom.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map ((F.commShiftIso a).hom.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorComm D a b).hom.app (F.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map ((F.commShiftIso b).inv.app X)) ((F.commShiftIso a).inv.app ((CategoryTheory.shiftFunctor C b).obj X)))))

@[simp]

theorem CategoryTheory.Functor.map_shiftFunctorCompIsoId_hom_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.CommShift A] (X : C) (a b : A) (h : a + b = 0) : F.map ((CategoryTheory.shiftFunctorCompIsoId C a b h).hom.app X) = CategoryTheory.CategoryStruct.comp ((F.commShiftIso b).hom.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map ((F.commShiftIso a).hom.app X)) ((CategoryTheory.shiftFunctorCompIsoId D a b h).hom.app (F.obj X)))

theorem CategoryTheory.Functor.map_shiftFunctorCompIsoId_hom_app_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.CommShift A] (X : C) (a b : A) (h : a + b = 0) {Z : D} (h✝ : F.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorCompIsoId C a b h).hom.app X)) h✝ = CategoryTheory.CategoryStruct.comp ((F.commShiftIso b).hom.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map ((F.commShiftIso a).hom.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId D a b h).hom.app (F.obj X)) h✝))

@[simp]

theorem CategoryTheory.Functor.map_shiftFunctorCompIsoId_inv_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.CommShift A] (X : C) (a b : A) (h : a + b = 0) : F.map ((CategoryTheory.shiftFunctorCompIsoId C a b h).inv.app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId D a b h).inv.app (F.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map ((F.commShiftIso a).inv.app X)) ((F.commShiftIso b).inv.app ((CategoryTheory.shiftFunctor C a).obj X)))

theorem CategoryTheory.Functor.map_shiftFunctorCompIsoId_inv_app_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.CommShift A] (X : C) (a b : A) (h : a + b = 0) {Z : D} (h✝ : F.obj ((CategoryTheory.shiftFunctor C b).obj ((CategoryTheory.shiftFunctor C a).obj X)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorCompIsoId C a b h).inv.app X)) h✝ = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId D a b h).inv.app (F.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map ((F.commShiftIso a).inv.app X)) (CategoryTheory.CategoryStruct.comp ((F.commShiftIso b).inv.app ((CategoryTheory.shiftFunctor C a).obj X)) h✝))

class CategoryTheory.NatTrans.CommShift {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] {F₁ F₂ : CategoryTheory.Functor C D} (τ : F₁ ⟶ F₂) (A : Type u_5) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F₁.CommShift A] [F₂.CommShift A] : Prop

If τ : F₁ ⟶ F₂ is a natural transformation between two functors which commute with a shift by an additive monoid A, this typeclass asserts a compatibility of τ with these shifts.

• comm' : ∀ (a : A), CategoryTheory.CategoryStruct.comp (F₁.commShiftIso a).hom (CategoryTheory.whiskerRight τ (CategoryTheory.shiftFunctor D a)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.shiftFunctor C a) τ) (F₂.commShiftIso a).hom

theorem CategoryTheory.NatTrans.CommShift.comm {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {F₁ F₂ : CategoryTheory.Functor C D} (τ : F₁ ⟶ F₂) {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F₁.CommShift A] [F₂.CommShift A] [CategoryTheory.NatTrans.CommShift τ A] (a : A) : CategoryTheory.CategoryStruct.comp (F₁.commShiftIso a).hom (CategoryTheory.whiskerRight τ (CategoryTheory.shiftFunctor D a)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.shiftFunctor C a) τ) (F₂.commShiftIso a).hom

theorem CategoryTheory.NatTrans.CommShift.comm_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {F₁ F₂ : CategoryTheory.Functor C D} (τ : F₁ ⟶ F₂) {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F₁.CommShift A] [F₂.CommShift A] [CategoryTheory.NatTrans.CommShift τ A] (a : A) (X : C) : CategoryTheory.CategoryStruct.comp ((F₁.commShiftIso a).hom.app X) ((CategoryTheory.shiftFunctor D a).map (τ.app X)) = CategoryTheory.CategoryStruct.comp (τ.app ((CategoryTheory.shiftFunctor C a).obj X)) ((F₂.commShiftIso a).hom.app X)

theorem CategoryTheory.NatTrans.CommShift.comm_app_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {F₁ F₂ : CategoryTheory.Functor C D} (τ : F₁ ⟶ F₂) {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F₁.CommShift A] [F₂.CommShift A] [CategoryTheory.NatTrans.CommShift τ A] (a : A) (X : C) {Z : D} (h : (CategoryTheory.shiftFunctor D a).obj (F₂.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F₁.commShiftIso a).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (τ.app X)) h) = CategoryTheory.CategoryStruct.comp (τ.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp ((F₂.commShiftIso a).hom.app X) h)

theorem CategoryTheory.NatTrans.CommShift.shift_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {F₁ F₂ : CategoryTheory.Functor C D} (τ : F₁ ⟶ F₂) {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F₁.CommShift A] [F₂.CommShift A] [CategoryTheory.NatTrans.CommShift τ A] (a : A) (X : C) : (CategoryTheory.shiftFunctor D a).map (τ.app X) = CategoryTheory.CategoryStruct.comp ((F₁.commShiftIso a).inv.app X) (CategoryTheory.CategoryStruct.comp (τ.app ((CategoryTheory.shiftFunctor C a).obj X)) ((F₂.commShiftIso a).hom.app X))

theorem CategoryTheory.NatTrans.CommShift.shift_app_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {F₁ F₂ : CategoryTheory.Functor C D} (τ : F₁ ⟶ F₂) {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F₁.CommShift A] [F₂.CommShift A] [CategoryTheory.NatTrans.CommShift τ A] (a : A) (X : C) {Z : D} (h : (CategoryTheory.shiftFunctor D a).obj (F₂.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (τ.app X)) h = CategoryTheory.CategoryStruct.comp ((F₁.commShiftIso a).inv.app X) (CategoryTheory.CategoryStruct.comp (τ.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp ((F₂.commShiftIso a).hom.app X) h))

theorem CategoryTheory.NatTrans.CommShift.app_shift {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {F₁ F₂ : CategoryTheory.Functor C D} (τ : F₁ ⟶ F₂) {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F₁.CommShift A] [F₂.CommShift A] [CategoryTheory.NatTrans.CommShift τ A] (a : A) (X : C) : τ.app ((CategoryTheory.shiftFunctor C a).obj X) = CategoryTheory.CategoryStruct.comp ((F₁.commShiftIso a).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (τ.app X)) ((F₂.commShiftIso a).inv.app X))

theorem CategoryTheory.NatTrans.CommShift.app_shift_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {F₁ F₂ : CategoryTheory.Functor C D} (τ : F₁ ⟶ F₂) {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F₁.CommShift A] [F₂.CommShift A] [CategoryTheory.NatTrans.CommShift τ A] (a : A) (X : C) {Z : D} (h : F₂.obj ((CategoryTheory.shiftFunctor C a).obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp (τ.app ((CategoryTheory.shiftFunctor C a).obj X)) h = CategoryTheory.CategoryStruct.comp ((F₁.commShiftIso a).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (τ.app X)) (CategoryTheory.CategoryStruct.comp ((F₂.commShiftIso a).inv.app X) h))

instance CategoryTheory.NatTrans.CommShift.of_iso_inv {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] {F₁ F₂ : CategoryTheory.Functor C D} (e : F₁ ≅ F₂) (A : Type u_5) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F₁.CommShift A] [F₂.CommShift A] [CategoryTheory.NatTrans.CommShift e.hom A] : CategoryTheory.NatTrans.CommShift e.inv A

Equations

• ⋯ = ⋯

theorem CategoryTheory.NatTrans.CommShift.of_isIso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {F₁ F₂ : CategoryTheory.Functor C D} (τ : F₁ ⟶ F₂) (A : Type u_5) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F₁.CommShift A] [F₂.CommShift A] [CategoryTheory.IsIso τ] [CategoryTheory.NatTrans.CommShift τ A] : CategoryTheory.NatTrans.CommShift (CategoryTheory.inv τ) A

instance CategoryTheory.NatTrans.CommShift.id {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] (F₁ : CategoryTheory.Functor C D) (A : Type u_5) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F₁.CommShift A] : CategoryTheory.NatTrans.CommShift (CategoryTheory.CategoryStruct.id F₁) A

Equations

• ⋯ = ⋯

instance CategoryTheory.NatTrans.CommShift.comp {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] {F₁ F₂ F₃ : CategoryTheory.Functor C D} (τ : F₁ ⟶ F₂) (τ' : F₂ ⟶ F₃) (A : Type u_5) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F₁.CommShift A] [F₂.CommShift A] [F₃.CommShift A] [CategoryTheory.NatTrans.CommShift τ A] [CategoryTheory.NatTrans.CommShift τ' A] : CategoryTheory.NatTrans.CommShift (CategoryTheory.CategoryStruct.comp τ τ') A

Equations

• ⋯ = ⋯

instance CategoryTheory.NatTrans.CommShift.whiskerRight {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] [CategoryTheory.Category.{u_8, u_3} E] {F₁ F₂ : CategoryTheory.Functor C D} (τ : F₁ ⟶ F₂) (G : CategoryTheory.Functor D E) (A : Type u_5) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [CategoryTheory.HasShift E A] [F₁.CommShift A] [F₂.CommShift A] [G.CommShift A] [CategoryTheory.NatTrans.CommShift τ A] : CategoryTheory.NatTrans.CommShift (CategoryTheory.whiskerRight τ G) A

Equations

• ⋯ = ⋯

instance CategoryTheory.NatTrans.CommShift.whiskerLeft {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{u_8, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] [CategoryTheory.Category.{u_7, u_3} E] (F₁ : CategoryTheory.Functor C D) {G G' : CategoryTheory.Functor D E} (τ'' : G ⟶ G') (A : Type u_5) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [CategoryTheory.HasShift E A] [F₁.CommShift A] [G.CommShift A] [G'.CommShift A] [CategoryTheory.NatTrans.CommShift τ'' A] : CategoryTheory.NatTrans.CommShift (CategoryTheory.whiskerLeft F₁ τ'') A

Equations

• ⋯ = ⋯

instance CategoryTheory.NatTrans.CommShift.associator {C : Type u_1} {D : Type u_2} {E : Type u_3} {J : Type u_4} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_9, u_2} D] [CategoryTheory.Category.{u_8, u_3} E] [CategoryTheory.Category.{u_7, u_4} J] (F₁ : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} (H : CategoryTheory.Functor E J) (A : Type u_5) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [CategoryTheory.HasShift E A] [CategoryTheory.HasShift J A] [F₁.CommShift A] [G.CommShift A] [H.CommShift A] : CategoryTheory.NatTrans.CommShift (F₁.associator G H).hom A

Equations

• ⋯ = ⋯

instance CategoryTheory.NatTrans.CommShift.leftUnitor {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] (F₁ : CategoryTheory.Functor C D) (A : Type u_5) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F₁.CommShift A] : CategoryTheory.NatTrans.CommShift F₁.leftUnitor.hom A

Equations

• ⋯ = ⋯

instance CategoryTheory.NatTrans.CommShift.rightUnitor {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] (F₁ : CategoryTheory.Functor C D) (A : Type u_5) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F₁.CommShift A] : CategoryTheory.NatTrans.CommShift F₁.rightUnitor.hom A

Equations

• ⋯ = ⋯

def CategoryTheory.Functor.CommShift.ofIso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {F G : CategoryTheory.Functor C D} (e : F ≅ G) (A : Type u_4) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.CommShift A] : G.CommShift A

If e : F ≅ G is an isomorphism of functors and if F commutes with the shift, then G also commutes with the shift.

Equations

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

theorem CategoryTheory.Functor.CommShift.ofIso_compatibility {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {F G : CategoryTheory.Functor C D} (e : F ≅ G) (A : Type u_4) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.CommShift A] : CategoryTheory.NatTrans.CommShift e.hom A

theorem CategoryTheory.NatTrans.CommShift.verticalComposition {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [CategoryTheory.Category.{u_8, u_1} C₁] [CategoryTheory.Category.{u_9, u_2} C₂] [CategoryTheory.Category.{u_10, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} D₁] [CategoryTheory.Category.{u_12, u_5} D₂] [CategoryTheory.Category.{u_13, u_6} D₃] {F₁₂ : CategoryTheory.Functor C₁ C₂} {F₂₃ : CategoryTheory.Functor C₂ C₃} {F₁₃ : CategoryTheory.Functor C₁ C₃} (α : F₁₃ ⟶ F₁₂.comp F₂₃) {G₁₂ : CategoryTheory.Functor D₁ D₂} {G₂₃ : CategoryTheory.Functor D₂ D₃} {G₁₃ : CategoryTheory.Functor D₁ D₃} (β : G₁₂.comp G₂₃ ⟶ G₁₃) {L₁ : CategoryTheory.Functor C₁ D₁} {L₂ : CategoryTheory.Functor C₂ D₂} {L₃ : CategoryTheory.Functor C₃ D₃} (e₁₂ : F₁₂.comp L₂ ⟶ L₁.comp G₁₂) (e₂₃ : F₂₃.comp L₃ ⟶ L₂.comp G₂₃) (e₁₃ : F₁₃.comp L₃ ⟶ L₁.comp G₁₃) (A : Type u_7) [AddMonoid A] [CategoryTheory.HasShift C₁ A] [CategoryTheory.HasShift C₂ A] [CategoryTheory.HasShift C₃ A] [CategoryTheory.HasShift D₁ A] [CategoryTheory.HasShift D₂ A] [CategoryTheory.HasShift D₃ A] [F₁₂.CommShift A] [F₂₃.CommShift A] [F₁₃.CommShift A] [CategoryTheory.NatTrans.CommShift α A] [G₁₂.CommShift A] [G₂₃.CommShift A] [G₁₃.CommShift A] [CategoryTheory.NatTrans.CommShift β A] [L₁.CommShift A] [L₂.CommShift A] [L₃.CommShift A] [CategoryTheory.NatTrans.CommShift e₁₂ A] [CategoryTheory.NatTrans.CommShift e₂₃ A] (h₁₃ : e₁₃ = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight α L₃) (CategoryTheory.CategoryStruct.comp (F₁₂.associator F₂₃ L₃).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft F₁₂ e₂₃) (CategoryTheory.CategoryStruct.comp (F₁₂.associator L₂ G₂₃).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight e₁₂ G₂₃) (CategoryTheory.CategoryStruct.comp (L₁.associator G₁₂ G₂₃).hom (CategoryTheory.whiskerLeft L₁ β))))))) : CategoryTheory.NatTrans.CommShift e₁₃ A

Assume that we have a diagram of categories

C₁ ⥤ D₁
‖     ‖
v     v
C₂ ⥤ D₂
‖     ‖
v     v
C₃ ⥤ D₃

with functors F₁₂ : C₁ ⥤ C₂, F₂₃ : C₂ ⥤ C₃ and F₁₃ : C₁ ⥤ C₃ on the first column that are related by a natural transformation α : F₁₃ ⟶ F₁₂ ⋙ F₂₃ and similarly β : G₁₂ ⋙ G₂₃ ⟶ G₁₃ on the second column. Assume that we have natural transformations e₁₂ : F₁₂ ⋙ L₂ ⟶ L₁ ⋙ G₁₂ (top square), e₂₃ : F₂₃ ⋙ L₃ ⟶ L₂ ⋙ G₂₃ (bottom square), and e₁₃ : F₁₃ ⋙ L₃ ⟶ L₁ ⋙ G₁₃ (outer square), where the horizontal functors are denoted L₁, L₂ and L₃. Assume that e₁₃ is determined by the other natural transformations α, e₂₃, e₁₂ and β. Then, if all these categories are equipped with a shift by an additive monoid A, and all these functors commute with these shifts, then the natural transformation e₁₃ of the outer square commutes with the shift if all α, e₂₃, e₁₂ and β do.