Degree-zero class localization in the homotopy category

The degree-zero class-localization map commutes with the functor on homotopy categories induced by degreewise module localization. This additive square requires no boundedness, finite-presentation, or K-projectivity hypotheses. It is not a derived-Hom localization or geometric base-change theorem.

The class-to-homotopy equivalence and its cocycle formula come from the neutral HomComplexCohomologyHomotopy leaf; only the localization square is proved here.

theorem CochainComplex.HomComplex.cohomologyClassLocalizedMap_homotopy_mk {R : Type u} [CommRing R] (P Q : CochainComplex (ModuleCat R) ℤ) (S : Submonoid R) (z : Cocycle P Q 0) : (cohomologyClassHomotopyAddEquiv (CochainComplex.HomComplex.localizedComplex✝ S P) (CochainComplex.HomComplex.localizedComplex✝ S Q)) ((cohomologyClassLocalizedMap P Q S) (CohomologyClass.mk z)) = ((ModuleCat.localizedModuleFunctor S).mapHomotopyCategory (ComplexShape.up ℤ)).map ((cohomologyClassHomotopyAddEquiv P Q) (CohomologyClass.mk z))

The localization square on a cocycle representative. By cohomologyClassHomotopyAddEquiv_mk, the source morphism is the homotopy class of z.homOf, and the target is the class of its degreewise localization.

theorem CochainComplex.HomComplex.cohomologyClassLocalizedMap_homotopy_naturality {R : Type u} [CommRing R] (P Q : CochainComplex (ModuleCat R) ℤ) (S : Submonoid R) : (cohomologyClassHomotopyAddEquiv (CochainComplex.HomComplex.localizedComplex✝ S P) (CochainComplex.HomComplex.localizedComplex✝ S Q)).toAddMonoidHom.comp (cohomologyClassLocalizedMap P Q S).toAddMonoidHom = ((ModuleCat.localizedModuleFunctor S).mapHomotopyCategory (ComplexShape.up ℤ)).mapAddHom.comp (cohomologyClassHomotopyAddEquiv P Q).toAddMonoidHom

Degree-zero class localization commutes, as an additive map, with degreewise localization on homotopy-category morphisms. No finiteness or K-projectivity assumptions are involved.