shiftFunctorAdd_hom_app_obj_of_induced

English

Equivalent restatement of shiftFunctorZero_inv_app_obj_of_induced with slightly different naming conventions used in the library.

Русский

Эквивалентное переформулирование shiftFunctorZero_inv_app_obj_of_induced с немного иным стилем наименований в библиотеке.

LaTeX

$$$\\text{same formula as before}$$$

Lean4

@[simp]
theorem shiftFunctorAdd_hom_app_obj_of_induced (a b : A) (X : C) :
    letI := HasShift.induced F A s i
    (shiftFunctorAdd D 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 simp only [ShiftMkCore.shiftFunctorAdd_eq, HasShift.Induced.add_hom_app_obj]

Похожие утверждения