Sequences of functors from a category equipped with a shift

Let F : C ⥤ A be a functor from a category C that is equipped with a shift by an additive monoid M. In this file, we define a typeclass F.ShiftSequence M which includes the data of a sequence of functors F.shift a : C ⥤ A for all a : A. For each a : A, we have an isomorphism F.isoShift a : shiftFunctor C a ⋙ F ≅ F.shift a which satisfies some coherence relations. This allows to state results (e.g. the long exact sequence of an homology functor (TODO)) using functors F.shift a rather than shiftFunctor C a ⋙ F. The reason for this design is that we can often choose functors F.shift a that have better definitional properties than shiftFunctor C a ⋙ F. For example, if C is the derived category (TODO) of an abelian category A and F is the homology functor in degree 0, then for any n : ℤ, we may choose F.shift n to be the homology functor in degree n.

class CategoryTheory.Functor.ShiftSequence {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} A] (F : CategoryTheory.Functor C A) (M : Type u_3) [AddMonoid M] [CategoryTheory.HasShift C M] : Type (max (max (max (max u_1 u_2) u_3) u_4) u_5)

A shift sequence for a functor F : C ⥤ A when C is equipped with a shift by a monoid M involves a sequence of functor sequence n : C ⥤ A for all n : M which behave like shiftFunctor C n ⋙ F.

• sequence : M → CategoryTheory.Functor C A

  a sequence of functors

• isoZero : CategoryTheory.Functor.ShiftSequence.sequence F 0 ≅ F

  sequence 0 identifies to the given functor

• shiftIso : (n a a' : M) → n + a = a' → (CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C n) (CategoryTheory.Functor.ShiftSequence.sequence F a) ≅ CategoryTheory.Functor.ShiftSequence.sequence F a')

  compatibility isomorphism with the shift

• shiftIso_zero : ∀ (a : M), CategoryTheory.Functor.ShiftSequence.shiftIso 0 a a ⋯ = CategoryTheory.isoWhiskerRight (CategoryTheory.shiftFunctorZero C M) (CategoryTheory.Functor.ShiftSequence.sequence F a) ≪≫ CategoryTheory.Functor.leftUnitor (CategoryTheory.Functor.ShiftSequence.sequence F a)
• shiftIso_add : ∀ (n m a a' a'' : M) (ha' : n + a = a') (ha'' : m + a' = a''), CategoryTheory.Functor.ShiftSequence.shiftIso (m + n) a a'' ⋯ = CategoryTheory.isoWhiskerRight (CategoryTheory.shiftFunctorAdd C m n) (CategoryTheory.Functor.ShiftSequence.sequence F a) ≪≫ CategoryTheory.Functor.associator (CategoryTheory.shiftFunctor C m) (CategoryTheory.shiftFunctor C n) (CategoryTheory.Functor.ShiftSequence.sequence F a) ≪≫ CategoryTheory.isoWhiskerLeft (CategoryTheory.shiftFunctor C m) (CategoryTheory.Functor.ShiftSequence.shiftIso n a a' ha') ≪≫ CategoryTheory.Functor.ShiftSequence.shiftIso m a' a'' ha''

noncomputable def CategoryTheory.Functor.ShiftSequence.tautological {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} A] (F : CategoryTheory.Functor C A) (M : Type u_3) [AddMonoid M] [CategoryTheory.HasShift C M] : CategoryTheory.Functor.ShiftSequence F M

The tautological shift sequence on a functor.

Equations

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

def CategoryTheory.Functor.shift {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] (n : M) : CategoryTheory.Functor C A

The shifted functors given by the shift sequence.

Equations

• CategoryTheory.Functor.shift F n = CategoryTheory.Functor.ShiftSequence.sequence F n

def CategoryTheory.Functor.shiftIso {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] (n : M) (a : M) (a' : M) (ha' : n + a = a') : CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C n) (CategoryTheory.Functor.shift F a) ≅ CategoryTheory.Functor.shift F a'

Compatibility isomorphism shiftFunctor C n ⋙ F.shift a ≅ F.shift a' when n + a = a'.

Equations

• CategoryTheory.Functor.shiftIso F n a a' ha' = CategoryTheory.Functor.ShiftSequence.shiftIso n a a' ha'

@[simp]

theorem CategoryTheory.Functor.shiftIso_hom_naturality_assoc {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] {X : C} {Y : C} (n : M) (a : M) (a' : M) (ha' : n + a = a') (f : X ⟶ Y) {Z : A} (h : (CategoryTheory.Functor.shift F a').obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shift F a).map ((CategoryTheory.shiftFunctor C n).map f)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shiftIso F n a a' ha').hom.app Y) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shiftIso F n a a' ha').hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shift F a').map f) h)

@[simp]

theorem CategoryTheory.Functor.shiftIso_hom_naturality {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] {X : C} {Y : C} (n : M) (a : M) (a' : M) (ha' : n + a = a') (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shift F a).map ((CategoryTheory.shiftFunctor C n).map f)) ((CategoryTheory.Functor.shiftIso F n a a' ha').hom.app Y) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shiftIso F n a a' ha').hom.app X) ((CategoryTheory.Functor.shift F a').map f)

@[simp]

theorem CategoryTheory.Functor.shiftIso_inv_naturality_assoc {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] {X : C} {Y : C} (n : M) (a : M) (a' : M) (ha' : n + a = a') (f : X ⟶ Y) {Z : A} (h : (CategoryTheory.Functor.shift F a).obj ((CategoryTheory.shiftFunctor C n).obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shift F a').map f) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shiftIso F n a a' ha').inv.app Y) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shiftIso F n a a' ha').inv.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shift F a).map ((CategoryTheory.shiftFunctor C n).map f)) h)

@[simp]

theorem CategoryTheory.Functor.shiftIso_inv_naturality {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] {X : C} {Y : C} (n : M) (a : M) (a' : M) (ha' : n + a = a') (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shift F a').map f) ((CategoryTheory.Functor.shiftIso F n a a' ha').inv.app Y) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shiftIso F n a a' ha').inv.app X) ((CategoryTheory.Functor.shift F a).map ((CategoryTheory.shiftFunctor C n).map f))

def CategoryTheory.Functor.isoShiftZero {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} A] (F : CategoryTheory.Functor C A) (M : Type u_3) [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] : CategoryTheory.Functor.shift F 0 ≅ F

The canonical isomorphism F.shift 0 ≅ F.

Equations

• CategoryTheory.Functor.isoShiftZero F M = CategoryTheory.Functor.ShiftSequence.isoZero

def CategoryTheory.Functor.isoShift {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] (n : M) : CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C n) F ≅ CategoryTheory.Functor.shift F n

The canonical isomorphism shiftFunctor C n ⋙ F ≅ F.shift n.

Equations

• CategoryTheory.Functor.isoShift F n = CategoryTheory.isoWhiskerLeft (CategoryTheory.shiftFunctor C n) (CategoryTheory.Functor.isoShiftZero F M).symm ≪≫ CategoryTheory.Functor.shiftIso F n 0 n ⋯

theorem CategoryTheory.Functor.isoShift_hom_naturality_assoc {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] (n : M) {X : C} {Y : C} (f : X ⟶ Y) {Z : A} (h : (CategoryTheory.Functor.shift F n).obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor C n).map f)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.isoShift F n).hom.app Y) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.isoShift F n).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shift F n).map f) h)

@[simp]

theorem CategoryTheory.Functor.isoShift_hom_naturality {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] (n : M) {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor C n).map f)) ((CategoryTheory.Functor.isoShift F n).hom.app Y) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.isoShift F n).hom.app X) ((CategoryTheory.Functor.shift F n).map f)

theorem CategoryTheory.Functor.isoShift_inv_naturality_assoc {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] (n : M) {X : C} {Y : C} (f : X ⟶ Y) {Z : A} (h : F.obj ((CategoryTheory.shiftFunctor C n).obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shift F n).map f) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.isoShift F n).inv.app Y) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.isoShift F n).inv.app X) (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor C n).map f)) h)

theorem CategoryTheory.Functor.isoShift_inv_naturality {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] (n : M) {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shift F n).map f) ((CategoryTheory.Functor.isoShift F n).inv.app Y) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.isoShift F n).inv.app X) (F.map ((CategoryTheory.shiftFunctor C n).map f))

theorem CategoryTheory.Functor.shiftIso_zero {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_4, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] (a : M) : CategoryTheory.Functor.shiftIso F 0 a a ⋯ = CategoryTheory.isoWhiskerRight (CategoryTheory.shiftFunctorZero C M) (CategoryTheory.Functor.shift F a) ≪≫ CategoryTheory.Functor.leftUnitor (CategoryTheory.Functor.shift F a)

@[simp]

theorem CategoryTheory.Functor.shiftIso_zero_hom_app {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_4, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] (a : M) (X : C) : (CategoryTheory.Functor.shiftIso F 0 a a ⋯).hom.app X = (CategoryTheory.Functor.shift F a).map ((CategoryTheory.shiftFunctorZero C M).hom.app X)

@[simp]

theorem CategoryTheory.Functor.shiftIso_zero_inv_app {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_4, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] (a : M) (X : C) : (CategoryTheory.Functor.shiftIso F 0 a a ⋯).inv.app X = (CategoryTheory.Functor.shift F a).map ((CategoryTheory.shiftFunctorZero C M).inv.app X)

theorem CategoryTheory.Functor.shiftIso_add {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_4, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] (n : M) (m : M) (a : M) (a' : M) (a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') : CategoryTheory.Functor.shiftIso F (m + n) a a'' ⋯ = CategoryTheory.isoWhiskerRight (CategoryTheory.shiftFunctorAdd C m n) (CategoryTheory.Functor.shift F a) ≪≫ CategoryTheory.Functor.associator (CategoryTheory.shiftFunctor C m) (CategoryTheory.shiftFunctor C n) (CategoryTheory.Functor.shift F a) ≪≫ CategoryTheory.isoWhiskerLeft (CategoryTheory.shiftFunctor C m) (CategoryTheory.Functor.shiftIso F n a a' ha') ≪≫ CategoryTheory.Functor.shiftIso F m a' a'' ha''

theorem CategoryTheory.Functor.shiftIso_add_hom_app {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_4, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] (n : M) (m : M) (a : M) (a' : M) (a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) : (CategoryTheory.Functor.shiftIso F (m + n) a a'' ⋯).hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shift F a).map ((CategoryTheory.shiftFunctorAdd C m n).hom.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shiftIso F n a a' ha').hom.app ((CategoryTheory.shiftFunctor C m).obj X)) ((CategoryTheory.Functor.shiftIso F m a' a'' ha'').hom.app X))

theorem CategoryTheory.Functor.shiftIso_add_inv_app {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_4, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] (n : M) (m : M) (a : M) (a' : M) (a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) : (CategoryTheory.Functor.shiftIso F (m + n) a a'' ⋯).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shiftIso F m a' a'' ha'').inv.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shiftIso F n a a' ha').inv.app ((CategoryTheory.shiftFunctor C m).obj X)) ((CategoryTheory.Functor.shift F a).map ((CategoryTheory.shiftFunctorAdd C m n).inv.app X)))

theorem CategoryTheory.Functor.shiftIso_add' {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_4, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] (n : M) (m : M) (mn : M) (hnm : m + n = mn) (a : M) (a' : M) (a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') : CategoryTheory.Functor.shiftIso F mn a a'' ⋯ = CategoryTheory.isoWhiskerRight (CategoryTheory.shiftFunctorAdd' C m n mn hnm) (CategoryTheory.Functor.shift F a) ≪≫ CategoryTheory.Functor.associator (CategoryTheory.shiftFunctor C m) (CategoryTheory.shiftFunctor C n) (CategoryTheory.Functor.shift F a) ≪≫ CategoryTheory.isoWhiskerLeft (CategoryTheory.shiftFunctor C m) (CategoryTheory.Functor.shiftIso F n a a' ha') ≪≫ CategoryTheory.Functor.shiftIso F m a' a'' ha''

theorem CategoryTheory.Functor.shiftIso_add'_hom_app {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_4, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] (n : M) (m : M) (mn : M) (hnm : m + n = mn) (a : M) (a' : M) (a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) : (CategoryTheory.Functor.shiftIso F mn a a'' ⋯).hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shift F a).map ((CategoryTheory.shiftFunctorAdd' C m n mn hnm).hom.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shiftIso F n a a' ha').hom.app ((CategoryTheory.shiftFunctor C m).obj X)) ((CategoryTheory.Functor.shiftIso F m a' a'' ha'').hom.app X))

theorem CategoryTheory.Functor.shiftIso_add'_inv_app {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_4, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] (n : M) (m : M) (mn : M) (hnm : m + n = mn) (a : M) (a' : M) (a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) : (CategoryTheory.Functor.shiftIso F mn a a'' ⋯).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shiftIso F m a' a'' ha'').inv.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shiftIso F n a a' ha').inv.app ((CategoryTheory.shiftFunctor C m).obj X)) ((CategoryTheory.Functor.shift F a).map ((CategoryTheory.shiftFunctorAdd' C m n mn hnm).inv.app X)))

theorem CategoryTheory.Functor.shiftIso_hom_app_comp_assoc {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_4, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] (n : M) (m : M) (mn : M) (hnm : m + n = mn) (a : M) (a' : M) (a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) {Z : A} (h : (CategoryTheory.Functor.shift F a'').obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shiftIso F n a a' ha').hom.app ((CategoryTheory.shiftFunctor C m).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shiftIso F m a' a'' ha'').hom.app X) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shift F a).map ((CategoryTheory.shiftFunctorAdd' C m n mn hnm).inv.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shiftIso F mn a a'' ⋯).hom.app X) h)

theorem CategoryTheory.Functor.shiftIso_hom_app_comp {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_4, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] (n : M) (m : M) (mn : M) (hnm : m + n = mn) (a : M) (a' : M) (a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shiftIso F n a a' ha').hom.app ((CategoryTheory.shiftFunctor C m).obj X)) ((CategoryTheory.Functor.shiftIso F m a' a'' ha'').hom.app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shift F a).map ((CategoryTheory.shiftFunctorAdd' C m n mn hnm).inv.app X)) ((CategoryTheory.Functor.shiftIso F mn a a'' ⋯).hom.app X)