English
In the HasShift.induced setting, the inverse add-hom component app at F.obj X is given by (s b).map ((i a).hom.app X) ≫ (i b).hom.app ((shiftFunctor C a).obj X) ≫ F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (i (a + b)).inv.app X.
Русский
В рамках HasShift.Induced, обратная часть add-hom на F.obj X задаётся как (s b).map ((i a).hom.app X) ≫ (i b).hom.app ((shiftFunctor C a).obj X) ≫ F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (i (a + b)).inv.app X.
LaTeX
$$$(add F s i a b).inv.app (F.obj X) = (s b).map ((i a).hom.app X) \\\\;\\circ\\\\; (i b).hom.app ((shiftFunctor C a).obj X) \\\\;\\circ\\\\; F.map ((shiftFunctorAdd C a b).inv.app X) \\\\;\\circ\\\\; (i (a + b)).inv.app X$$$
Lean4
@[simp]
theorem add_inv_app_obj (a b : A) (X : C) :
(add F s i a b).inv.app (F.obj X) =
(s b).map ((i a).hom.app X) ≫
(i b).hom.app ((shiftFunctor C a).obj X) ≫ F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (i (a + b)).inv.app X :=
by
have h : whiskerLeft F (add F s i a b).inv = _ := ((whiskeringLeft C D D).obj F).map_preimage _
exact (NatTrans.congr_app h X).trans (by simp)
