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][verdier1996]
@[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.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.
Instances For
@[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 : A}
{b : A}
{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 : A}
{b : A}
{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 : A}
{b : A}
{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.
Instances For
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 : 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
Instances For
@[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 : 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 : 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)
- add : ∀ (a b : A), CategoryTheory.Functor.CommShift.iso (a + b) = CategoryTheory.Functor.CommShift.isoAdd (CategoryTheory.Functor.CommShift.iso a) (CategoryTheory.Functor.CommShift.iso b)
Instances
theorem
CategoryTheory.Functor.CommShift.zero
{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]
[self : F.CommShift A]
:
theorem
CategoryTheory.Functor.CommShift.add
{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]
[self : F.CommShift A]
(a : A)
(b : A)
:
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
Instances For
@[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 : C}
{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_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 : C}
{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_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 : C}
{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)
@[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 : C}
{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))
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 : 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 : A}
{b : A}
{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 : 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)))))
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 : 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_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 : 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_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 : 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))
@[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 : 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)))
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₁ : CategoryTheory.Functor C D}
{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]
:
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
Instances
theorem
CategoryTheory.NatTrans.CommShift.comm'
{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}
{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]
[self : 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
{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}
{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_assoc
{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}
{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.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₁ : CategoryTheory.Functor C D}
{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.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₁ : CategoryTheory.Functor C D}
{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.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₁ : CategoryTheory.Functor C D}
{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.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₁ : CategoryTheory.Functor C D}
{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))
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₁ : CategoryTheory.Functor C D}
{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))
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₁ : CategoryTheory.Functor C D}
{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]
:
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₁ : CategoryTheory.Functor C D}
{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]
:
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]
:
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₁ : CategoryTheory.Functor C D}
{F₂ : CategoryTheory.Functor C D}
{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]
:
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₁ : CategoryTheory.Functor C D}
{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]
:
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 : CategoryTheory.Functor D E}
{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]
:
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 : CategoryTheory.Functor C D}
{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.
Instances For
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 : CategoryTheory.Functor C D}
{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]
:
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₁ β)))))))
:
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.