English
Dual to the previous, the inverse component of the mn-shift isomorphism also decomposes through the inverse of shiftFunctorAdd' and the inverse components of the individual shift isomorphisms, arranged in the corresponding whiskering/associator order.
Русский
Обратный компонент изоморфизма сдвига mn разлагается через обратный morphism shiftFunctorAdd' и обратные компоненты отдельных изоморфий сдвига, в нужном порядке whisker/ассociаторa.
LaTeX
$$$\ (F.shiftIso mn a a'' (by rw [\lt- hnm, \lt- ha'', \lt- ha', add_assoc])).inv.app X = (shiftIso F m a' a'' ha'').inv.app X \gg (shiftIso F n a a' ha').inv.app ((shiftFunctor C m).obj X) \gg (shift F a).map ((shiftFunctorAdd' C m n mn hnm).inv.app X)$$$
Lean4
theorem shiftIso_add'_inv_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])).inv.app X =
(shiftIso F m a' a'' ha'').inv.app X ≫
(shiftIso F n a a' ha').inv.app ((shiftFunctor C m).obj X) ≫
(shift F a).map ((shiftFunctorAdd' C m n mn hnm).inv.app X) :=
by simp [F.shiftIso_add' n m mn hnm a a' a'' ha' ha'']
