English
There is a canonical morphism from F.obj X to the cycles in degree 0 of (F.mapHomologicalComplex _).obj P.cocomplex.
Русский
Существует каноническое отображение из F.obj X в циклы нулевой степени (F.mapHomologicalComplex _).obj P.cocomplex.
LaTeX
$$$F.obj X \\to ((F.mapHomologicalComplex _).obj P.cocomplex).cycles 0$$$
Lean4
/-- If `P : InjectiveResolution X` and `F` is an additive functor, this is
the canonical morphism from `F.obj X` to the cycles in degree `0` of
`(F.mapHomologicalComplex _).obj P.cocomplex`. -/
noncomputable def toRightDerivedZero' {X : C} (P : InjectiveResolution X) (F : C ⥤ D) [F.Additive] :
F.obj X ⟶ ((F.mapHomologicalComplex _).obj P.cocomplex).cycles 0 :=
HomologicalComplex.liftCycles _ (F.map (P.ι.f 0)) 1 (by simp)
(by
dsimp
rw [← F.map_comp, HomologicalComplex.Hom.comm, HomologicalComplex.single_obj_d, zero_comp, F.map_zero])
