English
The inverse component of the additivity shift iso can be written as a composition of the two inverse parts and a pullback shift cat map.
Русский
Обратный компонент изоморфизма сложения можно записать как композицию двух обратных частей и отображение категориального модуля PullbackShift.
LaTeX
$$$ (F.shiftIso (m+n) a a'' (by rw [add_assoc, ha', ha''])).inv.app X = (F.shiftIso m a' a'' ha'').inv.app X \; \gg\; (F.shiftIso n a a' ha').inv.app ((shiftFunctor C m).obj X) \; \gg\; (F.shift a).map ((shiftFunctorAdd C m n).inv.app X) $$$
Lean4
theorem shiftIso_add_inv_app (n m a a' a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) :
(F.shiftIso (m + n) a a'' (by rw [add_assoc, ha', ha''])).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).inv.app X) :=
by simp [F.shiftIso_add n m a a' a'' ha' ha'']
