Canonical integer localization of degree-zero Hom-complex cohomology classes

The generic class-localization map carries a scoped, transported R-module structure. At R = ℤ, the same underlying additive map is relinearized with the ordinary integer action, and remains a module localization. This is a statement about Hom-complex cohomology, not derived-category Homs.

theorem CochainComplex.HomComplex.cohomologyClassLocalizedIntMap_isLocalized (P Q : CochainComplex (ModuleCat ℤ) ℤ) (S : Submonoid ℤ) (c b : ℤ) [P.IsStrictlyLE b] [Q.IsStrictlyGE c] [∀ (i : ↥(Finset.Icc (c - 1) b)), Module.FinitePresentation ℤ ↑(P.X ↑i)] : IsLocalizedModule S (cohomologyClassLocalizedMap P Q S).toAddMonoidHom.toIntLinearMap

Under half-boundedness and finite presentation on Icc (c - 1) b, the ordinary integer-linear class map is a module localization.