Canonical integer localization of derived-category Hom-sets

At R = ℤ, the generic derived-Hom localization map is relinearized with the ordinary integer actions on its source and target additive Hom groups. It is a module localization under the canonical integer class-map hypothesis. The bounded-projective specialization proves that hypothesis and supplies both K-projectivity instances. This does not construct internal derived Hom.

noncomputable def CochainComplex.HomComplex.derivedHomLocalizedIntMap (S : Submonoid ℤ) (P Q : CochainComplex (ModuleCat ℤ) ℤ) : (DerivedCategory.Qh.obj ((HomotopyCategory.quotient (ModuleCat ℤ) (ComplexShape.up ℤ)).obj P) ⟶ DerivedCategory.Qh.obj ((HomotopyCategory.quotient (ModuleCat ℤ) (ComplexShape.up ℤ)).obj Q)) →ₗ[ℤ] DerivedCategory.Qh.obj ((HomotopyCategory.quotient (ModuleCat (Localization S)) (ComplexShape.up ℤ)).obj (((ModuleCat.localizedModuleFunctor S).mapHomologicalComplex (ComplexShape.up ℤ)).obj P)) ⟶ DerivedCategory.Qh.obj ((HomotopyCategory.quotient (ModuleCat (Localization S)) (ComplexShape.up ℤ)).obj (((ModuleCat.localizedModuleFunctor S).mapHomologicalComplex (ComplexShape.up ℤ)).obj Q))

The generic map on derived-category morphisms, equipped with the canonical integer-module actions rather than the scoped linear actions.

Equations

• CochainComplex.HomComplex.derivedHomLocalizedIntMap S P Q = (CochainComplex.HomComplex.derivedHomLocalizedMap S P Q).toAddMonoidHom.toIntLinearMap

theorem CochainComplex.HomComplex.derivedHomLocalizedIntMap_class_square (S : Submonoid ℤ) (P Q : CochainComplex (ModuleCat ℤ) ℤ) [P.IsKProjective] [IsKProjective (((ModuleCat.localizedModuleFunctor S).mapHomologicalComplex (ComplexShape.up ℤ)).obj P)] (x : CohomologyClass P Q 0) : (derivedHomLocalizedIntMap S P Q) ((CohomologyClass.derivedCategoryHomIntLinearEquiv P Q) x) = (CohomologyClass.derivedCategoryHomIntLinearEquiv (((ModuleCat.localizedModuleFunctor S).mapHomologicalComplex (ComplexShape.up ℤ)).obj P) (((ModuleCat.localizedModuleFunctor S).mapHomologicalComplex (ComplexShape.up ℤ)).obj Q)) ((cohomologyClassLocalizedMap P Q S) x)

The canonical integer-linear map agrees with class localization through the canonical integer-linear class-to-derived equivalences.

theorem CochainComplex.HomComplex.derivedHomLocalizedIntMap_isLocalized (S : Submonoid ℤ) (P Q : CochainComplex (ModuleCat ℤ) ℤ) [P.IsKProjective] [IsKProjective (((ModuleCat.localizedModuleFunctor S).mapHomologicalComplex (ComplexShape.up ℤ)).obj P)] (hclass : IsLocalizedModule S (cohomologyClassLocalizedMap P Q S).toAddMonoidHom.toIntLinearMap) : IsLocalizedModule S (derivedHomLocalizedIntMap S P Q)

A canonical integer class-localization hypothesis transfers to the canonical integer map on derived-category Hom groups.

theorem CochainComplex.HomComplex.derivedHomLocalizedIntMap_isLocalized_of_bounded_above_below (S : Submonoid ℤ) (P Q : CochainComplex (ModuleCat ℤ) ℤ) [P.IsKProjective] [IsKProjective (((ModuleCat.localizedModuleFunctor S).mapHomologicalComplex (ComplexShape.up ℤ)).obj P)] (c b : ℤ) [P.IsStrictlyLE b] [Q.IsStrictlyGE c] [∀ (i : ↥(Finset.Icc (c - 1) b)), Module.FinitePresentation ℤ ↑(P.X ↑i)] : IsLocalizedModule S (derivedHomLocalizedIntMap S P Q)

The half-bounded finite-presentation class result gives canonical integer localization of derived Homs when both sources are K-projective.

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

An ordinary integer-module caller can use this bounded-above result without opening either scoped Hom-complex or ModuleCat.Algebra actions.