English
The inverse part of the left-derived object naturality is natural in morphisms of objects.
Русский
Обратная часть естественности левого производного объекта естественна по морфизмам объектов.
LaTeX
$$$ (P.isoLeftDerivedObj F n).inv \circ F.leftDerived n.map f = \cdots$$$
Lean4
/-- A component of the natural transformation between left-derived functors can be computed
using a chosen projective resolution. -/
theorem leftDerived_app_eq {F G : C ⥤ D} [F.Additive] [G.Additive] (α : F ⟶ G) {X : C} (P : ProjectiveResolution X)
(n : ℕ) :
(NatTrans.leftDerived α n).app X =
(P.isoLeftDerivedObj F n).hom ≫
(HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map
((NatTrans.mapHomologicalComplex α _).app P.complex) ≫
(P.isoLeftDerivedObj G n).inv :=
by
dsimp [NatTrans.leftDerived, isoLeftDerivedObj]
rw [ProjectiveResolution.leftDerivedToHomotopyCategory_app_eq α P, Functor.map_comp, Functor.map_comp, assoc]
erw [←
(HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.naturality_assoc
((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)]
simp only [Functor.comp_map, Iso.hom_inv_id_app_assoc]
