English
The application of left-derived functors to a morphism can be computed via a descent along projective resolutions.
Русский
Применение левых производных к морфизму вычисляется через спуск по проективным резольвциям.
LaTeX
$$$ (F.leftDerived n).map f = (P.isoLeftDerivedObj F n).hom \circ (F.mapHomologicalComplex _ \circ) \circ (Q.isoLeftDerivedObj F n)^{-1} $$$
Lean4
/-- We can compute a left derived functor on a morphism using a descent of that morphism
to a chain map between chosen projective resolutions.
-/
theorem leftDerived_map_eq (F : C ⥤ D) [F.Additive] (n : ℕ) {X Y : C} (f : X ⟶ Y) {P : ProjectiveResolution X}
{Q : ProjectiveResolution Y} (g : P.complex ⟶ Q.complex) (w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f) :
(F.leftDerived n).map f =
(P.isoLeftDerivedObj F n).hom ≫
(F.mapHomologicalComplex _ ⋙ HomologicalComplex.homologyFunctor _ _ n).map g ≫ (Q.isoLeftDerivedObj F n).inv :=
by
rw [← cancel_mono (Q.isoLeftDerivedObj F n).hom, ProjectiveResolution.isoLeftDerivedObj_hom_naturality f P Q g _ F n,
assoc, assoc, Iso.inv_hom_id, comp_id]
rw [← HomologicalComplex.comp_f, w, HomologicalComplex.comp_f, ChainComplex.single₀_map_f_zero]
