English
Let a ∈ A and X be an object of C. Then the hom component of the shiftFunctorAdd C a 0 at X is equal to the composition of eqToHom (since a+0 = a) with the inverse of shiftFunctorZero applied to X⟦a⟧.
Русский
Пусть a ∈ A и X — объект C. Тогда компоненту гомоморфизма (shiftFunctorAdd C a 0).hom в X равен композиции eqToHom(потому что a+0 = a) с обратным мономом (inv.app) shiftFunctorZero на X⟦a⟧.
LaTeX
$$$ (\\mathrm{shiftFunctorAdd} \\, C \\, a \\, 0).\\mathrm{hom}.\\mathrm{app} \\, X = \\operatorname{eqToHom}(\\mathrm{by\\ dsimp;\\ rw [add_zero]}) \\\\gg (\\mathrm{shiftFunctorZero} \\, C \\, A).inv.\\mathrm{app} (X\\langle a \\rangle ) $$$
Lean4
theorem shiftFunctorAdd_add_zero_hom_app (a : A) (X : C) :
(shiftFunctorAdd C a 0).hom.app X = eqToHom (by dsimp; rw [add_zero]) ≫ (shiftFunctorZero C A).inv.app (X⟦a⟧) := by
simp [← shiftFunctorAdd'_add_zero_hom_app, shiftFunctorAdd']
