English
For any X with a projective resolution P and additive functor F, there is a canonical isomorphism between the value of the left derived functor and the image of P under F in the homotopy category.
Русский
Для любого X с проективным разрешением P и добавитного функторы F существует каноническое изоморфизм между значением левого производного и образом P под F в гомотопной категории.
LaTeX
$$$\exists \; \text{iso}: (F.leftDerived_n)^\bullet X \cong (F.mapHomologicalComplex _) (P^\bullet).$$$
Lean4
/-- If `P : ProjectiveResolution Z` and `F : C ⥤ D` is an additive functor, this is
an isomorphism between `F.leftDerivedToHomotopyCategory.obj X` and the complex
obtained by applying `F` to `P.complex`. -/
noncomputable def isoLeftDerivedToHomotopyCategoryObj {X : C} (P : ProjectiveResolution X) (F : C ⥤ D) [F.Additive] :
F.leftDerivedToHomotopyCategory.obj X ≅ (F.mapHomologicalComplex _ ⋙ HomotopyCategory.quotient _ _).obj P.complex :=
(F.mapHomotopyCategory _).mapIso P.iso ≪≫ (F.mapHomotopyCategoryFactors _).app P.complex
