English
A reassociated version of the hom-level coherence: the composed action of successive shift isomorphisms equals the map obtained by shifting first then applying the two-step shift isomorphisms and finally the mn-shift isomorphism.
Русский
Переформулированная коherence на уровне гом-уровня: композиция последовательных изоморфий сдвига равна отображению, получаемому сдвигом сначала, затем двумя шагами изоморфий и, наконец, mn-изоморфизмом.
LaTeX
$$$(F.shiftIso n a a' ha').hom.app ((shiftFunctor C m).obj X) \gg (F.shiftIso m a' a'' ha'').hom.app X = (shift F a).map (f⟦n⟧') \gg (F.shiftIso mn a a'' (by rw [← ha'', ← ha', ← hnm, add_assoc])).hom.app X$$$
Lean4
@[reassoc]
theorem shiftIso_hom_app_comp (n m mn : M) (hnm : m + n = mn) (a a' a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'')
(X : C) :
(shiftIso F n a a' ha').hom.app ((shiftFunctor C m).obj X) ≫ (shiftIso F m a' a'' ha'').hom.app X =
(shift F a).map ((shiftFunctorAdd' C m n mn hnm).inv.app X) ≫
(F.shiftIso mn a a'' (by rw [← hnm, ← ha'', ← ha', add_assoc])).hom.app X :=
by
rw [F.shiftIso_add'_hom_app n m mn hnm a a' a'' ha' ha'', ← Functor.map_comp_assoc, Iso.inv_hom_id_app,
Functor.map_id, id_comp]
