English
For an additive functor F : C → D, there is a construction of the left derived functor which lands in the homotopy category of chain complexes in D, built from applying F to projective resolutions in C.
Русский
Для добавитного функтору F: C → D существует построение левого производного функторa, который отображается в гомотопию категорию комплексoв в D, полученную применением F к проективным разрешениям в C.
LaTeX
$$$ F: C \to D \text{ additive } \Rightarrow L^F_n: C \to D \quad\text{defined by } X \mapsto H_n(F(P^\bullet_X)),$$$
Lean4
/-- When `F : C ⥤ D` is an additive functor, this is
the functor `C ⥤ HomotopyCategory D (ComplexShape.down ℕ)` which
sends `X : C` to `F` applied to a projective resolution of `X`. -/
noncomputable def leftDerivedToHomotopyCategory (F : C ⥤ D) [F.Additive] :
C ⥤ HomotopyCategory D (ComplexShape.down ℕ) :=
projectiveResolutions C ⋙ F.mapHomotopyCategory _
