English
For every X and P: ProjectiveResolution X, there is an isomorphism between (F.leftDerived n).obj X and the homology of the mapped complex.
Русский
Для каждого X и P: ProjectiveResolution X существует изоморфизм между (F.leftDerived n).obj X и гомологией образованного комплекса.
LaTeX
$$$ (F.leftDerived n).\!\!\!\!\! .obj X \cong H_n( (F.mapHomologicalComplex _).obj P.complex ).$$$
Lean4
/-- We can compute a left derived functor using a chosen projective resolution. -/
noncomputable def isoLeftDerivedObj {X : C} (P : ProjectiveResolution X) (F : C ⥤ D) [F.Additive] (n : ℕ) :
(F.leftDerived n).obj X ≅
(HomologicalComplex.homologyFunctor D _ n).obj ((F.mapHomologicalComplex _).obj P.complex) :=
(HomotopyCategory.homologyFunctor D _ n).mapIso (P.isoLeftDerivedToHomotopyCategoryObj F) ≪≫
(HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).app _
