English
For two shift-coupled isomorphisms e1,e2, the hom component of their sum is given by F.map of the shiftAdd hom, followed by the respective applications of e2 and e1 and then the inverse of shiftAdd in the target.
Русский
Для двух изоморфизмов, сочетающихся со сдвигами e1,e2, гомоморфизм их суммы задаётся через отображение F.map от гомоморфизма shiftAdd, затем применения e2 и e1 и затем обратного shiftAdd на целевом объекте.
LaTeX
$$$ (CommShift.isoAdd e₁ e₂).hom.app X = F.map ((shiftFunctorAdd C a b).hom.app X) ≫ e₂.hom.app ((shiftFunctor C a).obj X) ≫ (shiftFunctor D b).map (e₁.hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X) $$$
Lean4
@[simp]
theorem isoAdd_hom_app {a b : A} (e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a)
(e₂ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b) (X : C) :
(CommShift.isoAdd e₁ e₂).hom.app X =
F.map ((shiftFunctorAdd C a b).hom.app X) ≫
e₂.hom.app ((shiftFunctor C a).obj X) ≫
(shiftFunctor D b).map (e₁.hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X) :=
by simp only [isoAdd, isoAdd'_hom_app, shiftFunctorAdd'_eq_shiftFunctorAdd]
