English
For a shift-structured functor F and indices n, m, mn with hnm = m + n = mn and a, a′, a″ as above, the hom component of the mn-shift isomorphism factors through the map (shift F a).map of the hom-component of the shiftFunctorAdd' morphism, followed by the corresponding iso components.
Русский
Для функторa F с структурой сдвига и индексов n, m, mn с hnm = m + n = mn и индексов a, a′, a″, гом-компонент изоморфизма сдвига mn разлагается через отображение (shift F a).map гом-компонента morphism shiftFunctorAdd' и соответствующие компоненты изоморфности.
LaTeX
$$$\ (F.shiftIso\ mn\ a\ a'' (by rw [\lt- hnm, \lt- ha'', \lt- ha', add_assoc])).hom.app X = (shift F a).map ((shiftFunctorAdd' C m n mn hnm).hom.app X) \gg (shiftIso F n a a' ha').hom.app ((shiftFunctor C m).obj X) \gg (shiftIso F m a' a'' ha'').hom.app X$$$
Lean4
theorem shiftIso_add'_hom_app (n m mn : M) (hnm : m + n = mn) (a a' a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'')
(X : C) :
(F.shiftIso mn a a'' (by rw [← hnm, ← ha'', ← ha', add_assoc])).hom.app X =
(shift F a).map ((shiftFunctorAdd' C m n mn hnm).hom.app X) ≫
(shiftIso F n a a' ha').hom.app ((shiftFunctor C m).obj X) ≫ (shiftIso F m a' a'' ha'').hom.app X :=
by simp [F.shiftIso_add' n m mn hnm a a' a'' ha' ha'']
