shiftFunctorZero_inv_app_obj_of_induced

English

Let F: C ⥤ D with HasShift.induced structure via i; then (shiftFunctorZero D A).inv.app (F.obj X) equals F.map ((shiftFunctorZero C A).inv.app X) ≫ (i 0).inv.app X.

Русский

Пусть F: C ⥤ D с индуцированной структурой через i; тогда (shiftFunctorZero D A).inv.app (F.obj X) = F.map ((shiftFunctorZero C A).inv.app X) ≫ (i 0).inv.app X.

LaTeX

$$$(shiftFunctorZero D A).inv.app (F.obj X) = F.map ((shiftFunctorZero C A).inv.app X) \\circ (i 0).inv.app X$$$

Lean4

@[simp]
theorem shiftFunctorZero_inv_app_obj_of_induced (X : C) :
    letI := HasShift.induced F A s i
    (shiftFunctorZero D A).inv.app (F.obj X) = F.map ((shiftFunctorZero C A).inv.app X) ≫ (i 0).inv.app X :=
  by simp only [ShiftMkCore.shiftFunctorZero_eq, HasShift.Induced.zero_inv_app_obj]

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