Exact derived comparison for canonical module localization

Scalar extension to Localization S and ModuleCat.localizedModuleFunctor S are naturally isomorphic exact functors. This file lifts their comparison to derived categories. It does not identify a geometric pullback or assert localization of a derived-category Hom group.

noncomputable def ModuleCat.extendScalarsLocalizationDerived {R : Type u} [CommRing R] (S : Submonoid R) : CategoryTheory.Functor (DerivedCategory (ModuleCat R)) (DerivedCategory (ModuleCat (Localization S)))

Exact derived scalar extension to the canonical localization. The exactness and additivity witnesses remain local to this definition.

Equations

• ModuleCat.extendScalarsLocalizationDerived S = (ModuleCat.extendScalars (algebraMap R (Localization S))).mapDerivedCategory

noncomputable def ModuleCat.localizedModuleDerived {R : Type u} [CommRing R] (S : Submonoid R) : CategoryTheory.Functor (DerivedCategory (ModuleCat R)) (DerivedCategory (ModuleCat (Localization S)))

Exact derived functor of Mathlib's canonical localized-module functor.

Equations

• ModuleCat.localizedModuleDerived S = (ModuleCat.localizedModuleFunctor S).mapDerivedCategory

noncomputable def ModuleCat.extendScalarsLocalizationDerivedNatIso {R : Type u} [CommRing R] (S : Submonoid R) : extendScalarsLocalizationDerived S ≅ localizedModuleDerived S

Derived natural isomorphism induced by the canonical ModuleCat comparison.

Equations

• ModuleCat.extendScalarsLocalizationDerivedNatIso S = id (CategoryTheory.NatIso.mapDerivedCategory (ModuleCat.extendScalarsLocalizationNatIso S))

theorem ModuleCat.extendScalarsLocalizationDerivedNatIso_naturality {R : Type u} [CommRing R] (S : Submonoid R) {X Y : DerivedCategory (ModuleCat R)} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((extendScalarsLocalizationDerived S).map f) ((extendScalarsLocalizationDerivedNatIso S).hom.app Y) = CategoryTheory.CategoryStruct.comp ((extendScalarsLocalizationDerivedNatIso S).hom.app X) ((localizedModuleDerived S).map f)

The comparison commutes with every arrow of the source derived category.