Degree-zero derived-category Hom localization for a finite module

The finite-term projective resolution of a finite module over a noetherian commutative ring gives localization of derived-category Hom-sets from that resolution. Its quasi-isomorphism to the degree-zero complex of the module, and the corresponding localized quasi-isomorphism, transport this statement to the degree-zero complex itself. The target is still the degreewise localization of that complex; no comparison with a single complex of the localized module is asserted here.

This concerns Hom-sets in the derived category, not an internal derived-Hom complex. The target complex is bounded below; the chosen resolution may have an infinite negative tail. No assertion about arbitrary bounded complexes, geometric pullback, hearts, or Theorem 5.7(2) follows.

theorem CochainComplex.HomComplex.degreeZero_derivedHomLocalizedMap_isLocalized {R : Type u} [CommRing R] (S : Submonoid R) [IsNoetherianRing R] (M : ModuleCat R) [Module.Finite R ↑M] (Q : CochainComplex (ModuleCat R) ℤ) (c : ℤ) [Q.IsStrictlyGE c] : IsLocalizedModule S (derivedHomLocalizedMap S ((singleFunctor (ModuleCat R) 0).obj M) Q)

For a finite module over a noetherian ring, localization of the degree-zero derived-category Hom-set from its degree-zero complex into any bounded-below module complex is a localization of R-modules. The codomain uses degreewise localization of the displayed complexes; no single-complex identification or internal derived-Hom base change is part of this statement.