English
There is a canonical isomorphism between the value of the left-derived functor and the homology of the mapped resolution for each X and P.
Русский
Существует канонический изоморфизм между значением левого производного функторa и гомологией образованного разрешения для каждого X и P.
LaTeX
$$$ (F.leftDerived n).obj X \cong H_n( (F.mapHomologicalComplex _) .obj P.complex )$$$
Lean4
theorem leftDerivedToHomotopyCategory_app_eq {F G : C ⥤ D} [F.Additive] [G.Additive] (α : F ⟶ G) {X : C}
(P : ProjectiveResolution X) :
(NatTrans.leftDerivedToHomotopyCategory α).app X =
(P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
(HomotopyCategory.quotient _ _).map ((NatTrans.mapHomologicalComplex α _).app P.complex) ≫
(P.isoLeftDerivedToHomotopyCategoryObj G).inv :=
by
rw [← cancel_mono (P.isoLeftDerivedToHomotopyCategoryObj G).hom, assoc, assoc, Iso.inv_hom_id, comp_id]
dsimp [isoLeftDerivedToHomotopyCategoryObj, Functor.mapHomotopyCategoryFactors,
NatTrans.leftDerivedToHomotopyCategory]
rw [assoc]
erw [id_comp, comp_id]
obtain ⟨β, hβ⟩ := (HomotopyCategory.quotient _ _).map_surjective (iso P).hom
rw [← hβ]
dsimp
simp only [← Functor.map_comp, NatTrans.mapHomologicalComplex_naturality]
rfl
