English
Compatibility of shiftIso with addition ensures the additive behaviour composes correctly with Functor's associator and whiskers.
Русский
Совместимость shiftIso с операцией сложения обеспечивает аддитивное поведение через ассоциатор функторов и обрамляющие изоморфизмы.
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'' .hom.app X $$$
Lean4
theorem shiftIso_add_hom_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''])).hom.app X =
(shift F a).map ((shiftFunctorAdd C m n).hom.app X) ≫
(shiftIso F n a a' ha').hom.app ((shiftFunctor C m).obj X) ≫ (shiftIso F m a' a'' ha'').hom.app X :=
by simp [F.shiftIso_add n m a a' a'' ha' ha'']
