Source naturality of derived-category Hom localization

The degreewise-localization map on derived-category Hom-sets commutes with precomposition by an arbitrary cochain map. No K-projectivity or boundedness is needed for this naturality square. It is shared by the degree-zero and bounded-complex finite-module localization theorems.

theorem CochainComplex.HomComplex.derivedHomLocalizedMap_precomp {R : Type u} [CommRing R] (S : Submonoid R) (X Y Q : CochainComplex (ModuleCat R) ℤ) (f : X ⟶ Y) (g : DerivedCategory.Qh.obj ((HomotopyCategory.quotient (ModuleCat R) (ComplexShape.up ℤ)).obj Y) ⟶ DerivedCategory.Qh.obj ((HomotopyCategory.quotient (ModuleCat R) (ComplexShape.up ℤ)).obj Q)) : (derivedHomLocalizedMap S X Q) (CategoryTheory.CategoryStruct.comp (DerivedCategory.Qh.map ((HomotopyCategory.quotient (ModuleCat R) (ComplexShape.up ℤ)).map f)) g) = CategoryTheory.CategoryStruct.comp (DerivedCategory.Qh.map ((HomotopyCategory.quotient (ModuleCat (Localization S)) (ComplexShape.up ℤ)).map (((ModuleCat.localizedModuleFunctor S).mapHomologicalComplex (ComplexShape.up ℤ)).map f))) ((derivedHomLocalizedMap S Y Q) g)

Degreewise localization of derived-category Hom-sets commutes with precomposition by a cochain map. The source change on the localized side is the image of that map under degreewise localization.