Derived-category Hom localization from bounded-above finite complexes

For a strictly bounded-above complex of finite modules over a noetherian commutative ring, the finite-projective replacement of 4aq has a quasi-isomorphism to the original complex. Its image under degreewise localization is also a quasi-isomorphism. The two induced source isomorphisms transport localization of derived-category Hom-sets from the replacement to the original complex, against a strictly bounded-below target.

The replacement may have an infinite negative-degree tail. This theorem is about Hom-sets in the derived category; it does not construct an internal derived-Hom complex, a geometric pullback or projector comparison, a heart statement, or Theorem 5.7(2).

theorem CochainComplex.HomComplex.derivedHomLocalizedMap_isLocalized_of_bounded_finite {R : Type u} [CommRing R] [IsNoetherianRing R] (S : Submonoid R) (K Q : CochainComplex (ModuleCat R) ℤ) (b c : ℤ) [K.IsStrictlyLE b] [Q.IsStrictlyGE c] (hfinite : ∀ (i : ℤ), Module.Finite R ↑(K.X i)) : IsLocalizedModule S (derivedHomLocalizedMap S K Q)

A strictly bounded-above complex of finite R-modules has a localized derived-category Hom-set map into every strictly bounded-below complex. There is no finiteness assumption on the target. The codomain of the map is the Hom-set between the degreewise localized displayed complexes.