English
There is a canonical isomorphism between the object (F.rightDerived n).obj X and the homology of the mapped injective cocomplex.
Русский
Существуют канонические изоморфизмы между (F.rightDerived n).obj X и гомологией отображённого кокомологического комплексa.
LaTeX
$$$(F.rightDerived n).\\mathrm{obj}X \\cong \\mathrm{Homology}_n((F\\ mapHomologicalComplex)\\circ I.cocomplex)$$$
Lean4
/-- We can compute a right derived functor using a chosen injective resolution. -/
noncomputable def isoRightDerivedObj {X : C} (I : InjectiveResolution X) (F : C ⥤ D) [F.Additive] (n : ℕ) :
(F.rightDerived n).obj X ≅
(HomologicalComplex.homologyFunctor D _ n).obj ((F.mapHomologicalComplex _).obj I.cocomplex) :=
(HomotopyCategory.homologyFunctor D _ n).mapIso (I.isoRightDerivedToHomotopyCategoryObj F) ≪≫
(HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).app _
