Degree-zero Hom localization from a finite-term resolution

For a finite module over a noetherian commutative ring, choose the finite-term projective resolution supplied by ModuleCat.exists_finite_projectiveResolution. Against a bounded-below module complex, the degree-zero derived-category Hom map of this chosen cochain resolution is a module localization. The source resolution is strictly bounded above by zero and may have an infinite negative tail. This does not identify the map with localization of derived Homs from the degree-zero complex of the original module; that requires a separate quasi-isomorphism comparison.

theorem CochainComplex.HomComplex.exists_finite_projectiveResolution_derivedHomLocalized {R : Type u} [CommRing R] [IsNoetherianRing R] (M : ModuleCat R) [Module.Finite R ↑M] (S : Submonoid R) (Q : CochainComplex (ModuleCat R) ℤ) (c : ℤ) [Q.IsStrictlyGE c] : ∃ (P : CategoryTheory.ProjectiveResolution M), (∀ (i : ℤ), Module.Finite R ↑(P.cochainComplex.X i)) ∧ P.cochainComplex.IsStrictlyLE 0 ∧ (∀ (i : ℤ), CategoryTheory.Projective (P.cochainComplex.X i)) ∧ QuasiIso P.π' ∧ IsLocalizedModule S (derivedHomLocalizedMap S P.cochainComplex Q)

A finite module admits a finite-term projective cochain resolution whose degree-zero derived-category Hom map into a bounded-below target localizes. The ProjectiveResolution witness also carries the augmentation to M; no finite length or derived-Hom comparison for M[0] is asserted.