English
In HasShift.induced setting, the inverse add-hom app equals (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 на 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 shiftFunctorAdd_inv_app_obj_of_induced (a b : A) (X : C) :
letI := HasShift.induced F A s i
(shiftFunctorAdd D 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 simp only [ShiftMkCore.shiftFunctorAdd_eq, HasShift.Induced.add_inv_app_obj]
