English
For a ∈ A and X ∈ Ob(C), the inv.app X of (shiftFunctorAdd C a 0) equals the hom.app of shiftFunctorZero at X⟦a⟧, composed to the right with eqToHom of the same equality a+0 = a.
Русский
Пусть a ∈ A и X ∈ Ob(C). Тогда inv.app X мономорфизм (shiftFunctorAdd C a 0) равен hom.app (shiftFunctorZero) на X⟦a⟧, композиция с eqToHom от равенства a+0 = a.
LaTeX
$$$ (\\mathrm{shiftFunctorAdd} \\, C \\, a \\, 0).inv.\\mathrm{app} \\, X = (\\mathrm{shiftFunctorZero} \\, C \\, A).hom.\\mathrm{app} (X\\\\langle a \\\\rangle ) \\\\gg \\operatorname{eqToHom}(\\mathrm{by\\ dsimp;\\ rw[add_zero]}) $$$
Lean4
theorem shiftFunctorAdd_add_zero_inv_app (a : A) (X : C) :
(shiftFunctorAdd C a 0).inv.app X = (shiftFunctorZero C A).hom.app (X⟦a⟧) ≫ eqToHom (by dsimp; rw [add_zero]) := by
simp [← shiftFunctorAdd'_add_zero_inv_app, shiftFunctorAdd']
