English
For e1,e2 as in the previous lemma, the inv component of the sum is given by a composition involving the hom of shiftAdd and the maps e1,e2, concluding with the map F.
Русский
Для e1,e2 как в предыдущем лемме, обратная составляющая суммы задаётся композицией, включающей гом от shiftAdd и отображения e1,e2, завершая отображением F.
LaTeX
$$$ (CommShift.isoAdd e₁ e₂).inv.app X = (shiftFunctorAdd D a b).hom.app (F.obj X) ≫ (shiftFunctor D b).map (e₁.inv.app X) ≫ e₂.inv.app ((CategoryTheory.shiftFunctor C a).obj X) ≫ F.map ((shiftFunctorAdd C a b).inv.app X) $$$
Lean4
@[simp]
theorem isoAdd_inv_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₂).inv.app X =
(shiftFunctorAdd D a b).hom.app (F.obj X) ≫
(shiftFunctor D b).map (e₁.inv.app X) ≫
e₂.inv.app ((shiftFunctor C a).obj X) ≫ F.map ((shiftFunctorAdd C a b).inv.app X) :=
by simp only [isoAdd, isoAdd'_inv_app, shiftFunctorAdd'_eq_shiftFunctorAdd]
