The derived module-localization comparison on displayed complexes

The exact derived natural isomorphism between scalar extension and canonical module localization agrees with the degreewise comparison after passage through the homotopy and derived quotients. No Hom-set localization or geometric pullback result is asserted here.

noncomputable def ModuleCat.extendScalarsLocalizationDerivedFactorsh {R : Type u} [CommRing R] (S : Submonoid R) (K : CochainComplex (ModuleCat R) ℤ) : (extendScalarsLocalizationDerived S).obj (DerivedCategory.Qh.obj ((HomotopyCategory.quotient (ModuleCat R) (ComplexShape.up ℤ)).obj K)) ≅ DerivedCategory.Qh.obj ((HomotopyCategory.quotient (ModuleCat (Localization S)) (ComplexShape.up ℤ)).obj (((extendScalars (algebraMap R (Localization S))).mapHomologicalComplex (ComplexShape.up ℤ)).obj K))

The Qh factorization of exact derived scalar extension on a displayed cochain complex. The required exactness and additivity instances are local.

Equations

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

theorem ModuleCat.extendScalarsLocalizationDerivedNatIso_Qh {R : Type u} [CommRing R] (S : Submonoid R) (K : CochainComplex (ModuleCat R) ℤ) : CategoryTheory.CategoryStruct.comp ((extendScalarsLocalizationDerivedNatIso S).hom.app (DerivedCategory.Qh.obj ((HomotopyCategory.quotient (ModuleCat R) (ComplexShape.up ℤ)).obj K))) ((localizedModuleFunctor S).mapDerivedCategoryFactorsh.hom.app ((HomotopyCategory.quotient (ModuleCat R) (ComplexShape.up ℤ)).obj K)) = CategoryTheory.CategoryStruct.comp (extendScalarsLocalizationDerivedFactorsh S K).hom (DerivedCategory.Qh.map ((HomotopyCategory.quotient (ModuleCat (Localization S)) (ComplexShape.up ℤ)).map ((extendScalarsLocalizationCochainNatIso S).hom.app K)))

The derived scalar-extension/localization isomorphism agrees on a displayed complex with the degreewise cochain comparison after Qh and the canonical derived-functor factorizations. This has no boundedness or finiteness premise.