English
Naturality of the right-derived object isomorphism with respect to a morphism f.
Русский
Естественность изоморфизма правых производных объектов по отображению f.
LaTeX
$$$(I.isoRightDerivedObj F n).inv \\circ (F.rightDerived n).map f = \\cdots$$$
Lean4
/-- A component of the natural transformation between right-derived functors can be computed
using a chosen injective resolution. -/
theorem rightDerived_app_eq {F G : C ⥤ D} [F.Additive] [G.Additive] (α : F ⟶ G) {X : C} (P : InjectiveResolution X)
(n : ℕ) :
(NatTrans.rightDerived α n).app X =
(P.isoRightDerivedObj F n).hom ≫
(HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map
((NatTrans.mapHomologicalComplex α _).app P.cocomplex) ≫
(P.isoRightDerivedObj G n).inv :=
by
dsimp [NatTrans.rightDerived, isoRightDerivedObj]
rw [InjectiveResolution.rightDerivedToHomotopyCategory_app_eq α P, Functor.map_comp, Functor.map_comp, assoc]
erw [←
(HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.naturality_assoc
((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)]
simp only [Functor.comp_map, Iso.hom_inv_id_app_assoc]
