English
For F, s, i providing HasShift.induced, the additive-shift step 'add F s i a b' yields a hom component whose app at X is given by the prescribed composite: (i(a+b)).hom.app X ≫ F.map ((shiftFunctorAdd C a b).hom.app X) ≫ (i b).inv.app ((shiftFunctor C a).obj X) ≫ (s b).map ((i a).inv.app X).
Русский
Для заданного HasShift.induced, добавляющая операция add F s i a b формирует компоненту гомоморфизма, которая при применении к X задаётся композиционным образом: (i(a+b)).hom.app X ≫ F.map ((shiftFunctorAdd C a b).hom.app X) ≫ (i b).inv.app ((shiftFunctor C a).obj X) ≫ (s b).map ((i a).inv.app X).
LaTeX
$$$(add F s i a b).hom.app (F.obj X) = (i (a+b)).hom.app X \\\\;\\circ\\; F.map ((shiftFunctorAdd C a b).hom.app X) \\\\;\\circ\\; (i b).inv.app ((shiftFunctor C a).obj X) \\\\;\\circ\\; (s b).map ((i a).inv.app X)$$$
Lean4
@[simp]
theorem add_hom_app_obj (a b : A) (X : C) :
(add F s i a b).hom.app (F.obj X) =
(i (a + b)).hom.app X ≫
F.map ((shiftFunctorAdd C a b).hom.app X) ≫
(i b).inv.app ((shiftFunctor C a).obj X) ≫ (s b).map ((i a).inv.app X) :=
by
have h : whiskerLeft F (add F s i a b).hom = _ := ((whiskeringLeft C D D).obj F).map_preimage _
exact (NatTrans.congr_app h X).trans (by simp)
