Conditional localization of derived-category Hom-sets

Degreewise module localization induces a map on derived-category morphisms. The canonical class-to-homotopy comparison followed by Qh identifies this map with degree-zero Hom-complex class localization when both the source and its localization are K-projective. Under the separate class-localization hypothesis, this map is a localization of R-modules. Both module categories use their standard derived-category structures.

No preservation of arbitrary K-projectivity, internal derived-Hom object, or geometric pullback comparison is asserted.

noncomputable def CochainComplex.HomComplex.derivedLocalizationComparison {R : Type u} [CommRing R] (S : Submonoid R) (X : CochainComplex (ModuleCat R) ℤ) : (ModuleCat.localizedModuleFunctor S).mapDerivedCategory.obj (DerivedCategory.Qh.obj ((HomotopyCategory.quotient (ModuleCat R) (ComplexShape.up ℤ)).obj X)) ≅ DerivedCategory.Qh.obj ((HomotopyCategory.quotient (ModuleCat (Localization S)) (ComplexShape.up ℤ)).obj (((ModuleCat.localizedModuleFunctor S).mapHomologicalComplex (ComplexShape.up ℤ)).obj X))

The canonical comparison between localizing a derived image and taking the derived image of the degreewise localized complex. It is the component of the existing mapDerivedCategoryFactorsh isomorphism.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CochainComplex.HomComplex.derivedHomLocalizedMap {R : Type u} [CommRing R] (S : Submonoid R) (P Q : CochainComplex (ModuleCat R) ℤ) : (DerivedCategory.Qh.obj ((HomotopyCategory.quotient (ModuleCat R) (ComplexShape.up ℤ)).obj P) ⟶ DerivedCategory.Qh.obj ((HomotopyCategory.quotient (ModuleCat R) (ComplexShape.up ℤ)).obj Q)) →ₗ[R] 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))

Degreewise localization on derived-category morphisms, conjugated by the canonical comparison isomorphisms. This linear map is defined without any K-projectivity hypothesis; the class comparison below needs both sources K-projective.

Equations

• One or more equations did not get rendered due to their size.

theorem CochainComplex.HomComplex.cohomologyClassLocalizedMap_derived_naturality {R : Type u} [CommRing R] (S : Submonoid R) (P Q : CochainComplex (ModuleCat R) ℤ) [P.IsKProjective] [IsKProjective (((ModuleCat.localizedModuleFunctor S).mapHomologicalComplex (ComplexShape.up ℤ)).obj P)] (x : CohomologyClass P Q 0) : CategoryTheory.CategoryStruct.comp ((ModuleCat.localizedModuleFunctor S).mapDerivedCategory.map ((CohomologyClass.derivedCategoryHomAddEquiv P Q) x)) (derivedLocalizationComparison S Q).hom = CategoryTheory.CategoryStruct.comp (derivedLocalizationComparison S P).hom ((CohomologyClass.derivedCategoryHomAddEquiv (((ModuleCat.localizedModuleFunctor S).mapHomologicalComplex (ComplexShape.up ℤ)).obj P) (((ModuleCat.localizedModuleFunctor S).mapHomologicalComplex (ComplexShape.up ℤ)).obj Q)) ((cohomologyClassLocalizedMap P Q S) x))

The class-to-derived comparison commutes with degreewise localization. Both source complexes must be K-projective; no boundedness is needed here.

theorem CochainComplex.HomComplex.derivedHomLocalizedMap_class_square {R : Type u} [CommRing R] (S : Submonoid R) (P Q : CochainComplex (ModuleCat R) ℤ) [P.IsKProjective] [IsKProjective (((ModuleCat.localizedModuleFunctor S).mapHomologicalComplex (ComplexShape.up ℤ)).obj P)] (x : CohomologyClass P Q 0) : (derivedHomLocalizedMap S P Q) ((CohomologyClass.derivedCategoryHomLinearEquiv P Q) x) = (CohomologyClass.derivedCategoryHomLinearEquiv (((ModuleCat.localizedModuleFunctor S).mapHomologicalComplex (ComplexShape.up ℤ)).obj P) (((ModuleCat.localizedModuleFunctor S).mapHomologicalComplex (ComplexShape.up ℤ)).obj Q)) ((cohomologyClassLocalizedMap P Q S) x)

The linear derived-Hom map agrees pointwise with class localization through the two K-projective class-to-derived linear equivalences.

theorem CochainComplex.HomComplex.derivedHomLocalizedMap_isLocalized {R : Type u} [CommRing R] (S : Submonoid R) (P Q : CochainComplex (ModuleCat R) ℤ) [P.IsKProjective] [IsKProjective (((ModuleCat.localizedModuleFunctor S).mapHomologicalComplex (ComplexShape.up ℤ)).obj P)] (hclass : IsLocalizedModule S (cohomologyClassLocalizedMap P Q S)) : IsLocalizedModule S (derivedHomLocalizedMap S P Q)

If the degree-zero class map is a localization, so is the induced derived-category Hom map. K-projectivity of the localized source is an explicit separate assumption.

theorem CochainComplex.HomComplex.derivedHomLocalizedMap_isLocalized_of_bounded_above_below {R : Type u} [CommRing R] (S : Submonoid R) (P Q : CochainComplex (ModuleCat R) ℤ) [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 R ↑(P.X ↑i)] : IsLocalizedModule S (derivedHomLocalizedMap S P Q)

The half-bounded finite-presentation class theorem transfers to derived-category Hom-sets when both sources are K-projective.

theorem CochainComplex.HomComplex.derivedHomLocalizedMap_isLocalized_of_bounded_projective {R : Type u} [CommRing R] (S : Submonoid R) (P Q : CochainComplex (ModuleCat R) ℤ) (c b : ℤ) [P.IsStrictlyLE b] [Q.IsStrictlyGE c] [∀ (i : ℤ), CategoryTheory.Projective (P.X i)] [∀ (i : ↥(Finset.Icc (c - 1) b)), Module.FinitePresentation R ↑(P.X ↑i)] : IsLocalizedModule S (derivedHomLocalizedMap S P Q)

Bounded-above termwise projectivity supplies K-projectivity of both P and its degreewise localization. The finite-presentation condition is separate and comes from the half-bounded Hom-complex localization theorem.