English
Let L, F, G form a shift sequence with appropriate isomorphisms e and e'. For any n, a, a' in M with n + a = a' and any X in C, the component of the induced shift isomorphism at L X factors as a composition of the pieces (F' a), (e' a), (G shift), and (e' a').
Русский
Пусть данные L, F, G образуют последовательность сдвигов с соответствующими изоморфизмами e и e'. Для любых элементов n, a, a' множества M с условием n + a = a' и любого X в C, компонент индуцированного изоморфизма сдвига на L X раскладывается в композицию составных частей (F' a), (e' a), (G shift) и (e' a').
LaTeX
$$$ (shiftIso\ L\ G\ M\ F'\ e'\ n\ a\ a'\ ha').hom.app\ (L.obj\ X) = (F'\ a).map\ ((L.commShiftIso\ n).inv.app\ X) \;\gg\; (e'\ a).hom.app\ (X\langle n \rangle) \;\gg\; (G.shiftIso\ n\ a\ a'\ ha').hom.app\ X \;\gg\; (e'\ a').inv.app\ X $$$
Lean4
theorem shiftIso_hom_app_obj (n a a' : M) (ha' : n + a = a') (X : C) :
(shiftIso L G M F' e' n a a' ha').hom.app (L.obj X) =
(F' a).map ((L.commShiftIso n).inv.app X) ≫
(e' a).hom.app (X⟦n⟧) ≫ (G.shiftIso n a a' ha').hom.app X ≫ (e' a').inv.app X :=
(NatTrans.congr_app (((whiskeringLeft C D A).obj L).map_preimage _) X).trans (by simp)
