English
The shiftIso for a sum m+n factors through the sum of the shifts with associator and whiskering with F.
Русский
Сдвиг-изоморфизм для суммы m+n разлагается через суммы сдвигов и ассоциатор/F-обрамление.
LaTeX
$$$ F.shiftIso (m+n) a a'' (by rw [add_assoc, ha', ha'']).hom.app X = \; isoWhiskerRight (shiftFunctorAdd C m n) _ \; ≪≫ \; Functor.associator _ _ _ \; ≪≫ \; isoWhiskerLeft _ (F.shiftIso n a a' ha') \; ≪≫ F.shiftIso m a' a'' ha'' $$$
Lean4
theorem shiftIso_add (n m a a' a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') :
F.shiftIso (m + n) a a'' (by rw [add_assoc, ha', ha'']) =
isoWhiskerRight (shiftFunctorAdd C m n) _ ≪≫
Functor.associator _ _ _ ≪≫ isoWhiskerLeft _ (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha'' :=
ShiftSequence.shiftIso_add _ _ _ _ _ _ _
