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]

noncomputable def CategoryTheory.Functor.CommShift.isoZero {C : Type u_1} {D : Type u_2} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] (F : Functor C D) (A : Type u_4) [AddMonoid A] [HasShift C A] [HasShift D A] : (shiftFunctor C 0).comp F ≅ F.comp (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} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] (F : Functor C D) (A : Type u_4) [AddMonoid A] [HasShift C A] [HasShift D A] (X : C) : (isoZero F A).hom.app X = CategoryStruct.comp (F.map ((shiftFunctorZero C A).hom.app X)) ((shiftFunctorZero D A).inv.app (F.obj X))

@[simp]

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

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

For any functor F : C ⥤ D and any a in A such that a = 0, this is the obvious isomorphism shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D 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'_inv_app {C : Type u_1} {D : Type u_2} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] (F : Functor C D) (A : Type u_4) [AddMonoid A] [HasShift C A] [HasShift D A] (a : A) (ha : a = 0) (X : C) : (isoZero' F A a ha).inv.app X = CategoryStruct.comp ((shiftFunctorZero' D a ha).hom.app (F.obj X)) (F.map ((shiftFunctorZero' C a ha).inv.app X))

@[simp]

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

@[simp]

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

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

@[simp]

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

noncomputable def CategoryTheory.Functor.CommShift.isoAdd {C : Type u_1} {D : Type u_2} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] {F : Functor C D} {A : Type u_4} [AddMonoid A] [HasShift C A] [HasShift D A] {a b : A} (e₁ : (shiftFunctor C a).comp F ≅ F.comp (shiftFunctor D a)) (e₂ : (shiftFunctor C b).comp F ≅ F.comp (shiftFunctor D b)) : (shiftFunctor C (a + b)).comp F ≅ F.comp (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} [Category.{u_7, u_1} C] [Category.{u_6, u_2} D] {F : Functor C D} {A : Type u_4} [AddMonoid A] [HasShift C A] [HasShift D A] {a b : A} (e₁ : (shiftFunctor C a).comp F ≅ F.comp (shiftFunctor D a)) (e₂ : (shiftFunctor C b).comp F ≅ F.comp (shiftFunctor D b)) (X : C) : (isoAdd e₁ e₂).hom.app X = CategoryStruct.comp (F.map ((shiftFunctorAdd C a b).hom.app X)) (CategoryStruct.comp (e₂.hom.app ((shiftFunctor C a).obj X)) (CategoryStruct.comp ((shiftFunctor D b).map (e₁.hom.app X)) ((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} [Category.{u_7, u_1} C] [Category.{u_6, u_2} D] {F : Functor C D} {A : Type u_4} [AddMonoid A] [HasShift C A] [HasShift D A] {a b : A} (e₁ : (shiftFunctor C a).comp F ≅ F.comp (shiftFunctor D a)) (e₂ : (shiftFunctor C b).comp F ≅ F.comp (shiftFunctor D b)) (X : C) : (isoAdd e₁ e₂).inv.app X = CategoryStruct.comp ((shiftFunctorAdd D a b).hom.app (F.obj X)) (CategoryStruct.comp ((shiftFunctor D b).map (e₁.inv.app X)) (CategoryStruct.comp (e₂.inv.app ((shiftFunctor C a).obj X)) (F.map ((shiftFunctorAdd C a b).inv.app X))))

class CategoryTheory.Functor.CommShift {C : Type u_1} {D : Type u_2} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] (F : Functor C D) (A : Type u_4) [AddMonoid A] [HasShift C A] [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) : (shiftFunctor C a).comp F ≅ F.comp (shiftFunctor D a)

  The commutation isomorphisms for all a-shifts this functor is equipped with

• zero : iso 0 = isoZero F A
• add (a b : A) : iso (a + b) = isoAdd (iso a) (iso b)

def CategoryTheory.Functor.commShiftIso {C : Type u_1} {D : Type u_2} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] (F : Functor C D) {A : Type u_4} [AddMonoid A] [HasShift C A] [HasShift D A] [F.CommShift A] (a : A) : (shiftFunctor C a).comp F ≅ F.comp (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} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] (F : Functor C D) {A : Type u_4} [AddMonoid A] [HasShift C A] [HasShift D A] [F.CommShift A] {X Y : C} (f : X ⟶ Y) (a : A) : CategoryStruct.comp (F.map ((shiftFunctor C a).map f)) ((F.commShiftIso a).hom.app Y) = CategoryStruct.comp ((F.commShiftIso a).hom.app X) ((shiftFunctor D a).map (F.map f))

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

instance CategoryTheory.Functor.CommShift.id (C : Type u_1) [Category.{u_6, u_1} C] {A : Type u_4} [AddMonoid A] [HasShift C A] : (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} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] [Category.{u_8, u_3} E] (F : Functor C D) (G : Functor D E) {A : Type u_4} [AddMonoid A] [HasShift C A] [HasShift D A] [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} [Category.{u_6, u_1} C] {A : Type u_4} [AddMonoid A] [HasShift C A] (a : A) (X : C) : ((Functor.id C).commShiftIso a).hom.app X = CategoryStruct.id (((shiftFunctor C a).comp (Functor.id C)).obj X)

@[simp]

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

theorem CategoryTheory.Functor.commShiftIso_comp_hom_app {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] [Category.{u_8, u_3} E] (F : Functor C D) (G : Functor D E) {A : Type u_4} [AddMonoid A] [HasShift C A] [HasShift D A] [HasShift E A] [F.CommShift A] [G.CommShift A] (a : A) (X : C) : ((F.comp G).commShiftIso a).hom.app X = 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} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] [Category.{u_8, u_3} E] (F : Functor C D) (G : Functor D E) {A : Type u_4} [AddMonoid A] [HasShift C A] [HasShift D A] [HasShift E A] [F.CommShift A] [G.CommShift A] (a : A) (X : C) : ((F.comp G).commShiftIso a).inv.app X = 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} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] (F : Functor C D) {B : Type u_5} [AddCommMonoid B] [HasShift C B] [HasShift D B] [F.CommShift B] (X : C) (a b : B) : F.map ((shiftFunctorComm C a b).hom.app X) = CategoryStruct.comp ((F.commShiftIso b).hom.app ((shiftFunctor C a).obj X)) (CategoryStruct.comp ((shiftFunctor D b).map ((F.commShiftIso a).hom.app X)) (CategoryStruct.comp ((shiftFunctorComm D a b).hom.app (F.obj X)) (CategoryStruct.comp ((shiftFunctor D a).map ((F.commShiftIso b).inv.app X)) ((F.commShiftIso a).inv.app ((shiftFunctor C b).obj X)))))

@[simp]

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

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

class CategoryTheory.NatTrans.CommShift {C : Type u_1} {D : Type u_2} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] {F₁ F₂ : Functor C D} (τ : F₁ ⟶ F₂) (A : Type u_5) [AddMonoid A] [HasShift C A] [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.

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

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

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

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

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

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

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

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

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

@[deprecated CategoryTheory.NatTrans.shift_comm (since := "2024-12-31")]

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

Alias of CategoryTheory.NatTrans.shift_comm.

@[deprecated CategoryTheory.NatTrans.shift_comm (since := "2024-12-31")]

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

Alias of CategoryTheory.NatTrans.shift_comm.

@[deprecated CategoryTheory.NatTrans.shift_app_comm (since := "2024-12-31")]

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

Alias of CategoryTheory.NatTrans.shift_app_comm.

@[deprecated CategoryTheory.NatTrans.shift_app (since := "2024-12-31")]

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

Alias of CategoryTheory.NatTrans.shift_app.

@[deprecated CategoryTheory.NatTrans.app_shift (since := "2024-12-31")]

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

Alias of CategoryTheory.NatTrans.app_shift.

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

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

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

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

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

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

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

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

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

def CategoryTheory.Functor.CommShift.ofIso {C : Type u_1} {D : Type u_2} [Category.{u_5, u_1} C] [Category.{u_6, u_2} D] {F G : Functor C D} (e : F ≅ G) (A : Type u_4) [AddMonoid A] [HasShift C A] [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} [Category.{u_5, u_1} C] [Category.{u_6, u_2} D] {F G : Functor C D} (e : F ≅ G) (A : Type u_4) [AddMonoid A] [HasShift C A] [HasShift D A] [F.CommShift A] : 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} [Category.{u_8, u_1} C₁] [Category.{u_9, u_2} C₂] [Category.{u_10, u_3} C₃] [Category.{u_11, u_4} D₁] [Category.{u_12, u_5} D₂] [Category.{u_13, u_6} D₃] {F₁₂ : Functor C₁ C₂} {F₂₃ : Functor C₂ C₃} {F₁₃ : Functor C₁ C₃} (α : F₁₃ ⟶ F₁₂.comp F₂₃) {G₁₂ : Functor D₁ D₂} {G₂₃ : Functor D₂ D₃} {G₁₃ : Functor D₁ D₃} (β : G₁₂.comp G₂₃ ⟶ G₁₃) {L₁ : Functor C₁ D₁} {L₂ : Functor C₂ D₂} {L₃ : 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] [HasShift C₁ A] [HasShift C₂ A] [HasShift C₃ A] [HasShift D₁ A] [HasShift D₂ A] [HasShift D₃ A] [F₁₂.CommShift A] [F₂₃.CommShift A] [F₁₃.CommShift A] [CommShift α A] [G₁₂.CommShift A] [G₂₃.CommShift A] [G₁₃.CommShift A] [CommShift β A] [L₁.CommShift A] [L₂.CommShift A] [L₃.CommShift A] [CommShift e₁₂ A] [CommShift e₂₃ A] (h₁₃ : e₁₃ = CategoryStruct.comp (CategoryTheory.whiskerRight α L₃) (CategoryStruct.comp (F₁₂.associator F₂₃ L₃).hom (CategoryStruct.comp (CategoryTheory.whiskerLeft F₁₂ e₂₃) (CategoryStruct.comp (F₁₂.associator L₂ G₂₃).inv (CategoryStruct.comp (CategoryTheory.whiskerRight e₁₂ G₂₃) (CategoryStruct.comp (L₁.associator G₁₂ G₂₃).hom (CategoryTheory.whiskerLeft L₁ β))))))) : 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.