Derived-category Hom localization from a finite-projective replacement

Over a noetherian commutative ring, a strictly bounded-above complex of finite modules has a strictly bounded-above replacement with finite projective terms. For a bounded-below target, the derived-category Hom map out of that chosen replacement is a module localization. The quasi-isomorphism to the original complex is retained as part of the witness, but this theorem does not assert localization for the Hom map out of the original complex.

theorem CochainComplex.HomComplex.exists_finite_projective_replacement_derivedHomLocalized {R : Type u} [CommRing R] [IsNoetherianRing R] (K Q : CochainComplex (ModuleCat R) ℤ) (S : Submonoid R) (b c : ℤ) [K.IsStrictlyLE b] [Q.IsStrictlyGE c] (hfinite : ∀ (i : ℤ), Module.Finite R ↑(K.X i)) : ∃ (P : CochainComplex (ModuleCat R) ℤ) (p : P ⟶ K), P.IsStrictlyLE b ∧ (∀ (i : ℤ), Module.Finite R ↑(P.X i)) ∧ (∀ (i : ℤ), CategoryTheory.Projective (P.X i)) ∧ P.IsKProjective ∧ QuasiIso p ∧ IsLocalizedModule S (derivedHomLocalizedMap S P Q)

A bounded-above complex of finite modules has a finite-projective, K-projective replacement whose derived-category Hom map into a bounded-below complex localizes. The replacement may have an infinite negative-degree tail; no localization assertion is made for the Hom map out of K itself.