English
A component of the natural transformation between right-derived functors can be computed using an injective resolution.
Русский
Компонент натурального преобразования между правыми производными можно вычислить через инъективное разрешение.
LaTeX
$$$(\\mathrm{rightDerived} \\alpha n).\\mathrm{app}X = (P.isoRightDerivedObj F n).hom \\circ (\\mathrm{mapHomologicalComplex} \\alpha) \\circ (P.isoRightDerivedObj G n)^{-1}$$$
Lean4
/-- We can compute a right derived functor on a morphism using a descent of that morphism
to a cochain map between chosen injective resolutions.
-/
theorem rightDerived_map_eq (F : C ⥤ D) [F.Additive] (n : ℕ) {X Y : C} (f : X ⟶ Y) {P : InjectiveResolution X}
{Q : InjectiveResolution Y} (g : P.cocomplex ⟶ Q.cocomplex) (w : P.ι ≫ g = (CochainComplex.single₀ C).map f ≫ Q.ι) :
(F.rightDerived n).map f =
(P.isoRightDerivedObj F n).hom ≫
(F.mapHomologicalComplex _ ⋙ HomologicalComplex.homologyFunctor _ _ n).map g ≫ (Q.isoRightDerivedObj F n).inv :=
by
rw [← cancel_mono (Q.isoRightDerivedObj F n).hom, InjectiveResolution.isoRightDerivedObj_hom_naturality f P Q g _ F n,
assoc, assoc, Iso.inv_hom_id, comp_id]
rw [← HomologicalComplex.comp_f, w, HomologicalComplex.comp_f, CochainComplex.single₀_map_f_zero]
