Tensor extension and canonical module localization in ModuleCat

For the canonical ring Localization S, extension of scalars and Mathlib's localizedModuleFunctor S are naturally isomorphic. The latter uses a Shrink carrier, so the comparison is not definitional. Its component sends the tensor generator 1 ⊗ m to localizedModuleMkLinearMap S m.

The natural isomorphism also acts on cochain complexes. No arrow descent or derived-category Hom localization is asserted here.

noncomputable def ModuleCat.extendScalarsLocalizationIso {R : Type u} [CommRing R] (S : Submonoid R) (M : ModuleCat R) : (extendScalars (algebraMap R (Localization S))).obj M ≅ (localizedModuleFunctor S).obj M

The canonical scalar-extension/localized-module comparison at one module.

Equations

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

theorem ModuleCat.extendScalarsLocalizationIso_hom_tmul {R : Type u} [CommRing R] (S : Submonoid R) (M : ModuleCat R) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (extendScalarsLocalizationIso S M).hom) (1 ⊗ₜ[R] m) = (M.localizedModuleMkLinearMap S) m

The component comparison agrees with the two localization generators.

noncomputable def ModuleCat.extendScalarsLocalizationNatIso {R : Type u} [CommRing R] (S : Submonoid R) : extendScalars (algebraMap R (Localization S)) ≅ localizedModuleFunctor S

Canonical natural isomorphism between tensor extension and localized modules.

Equations

• ModuleCat.extendScalarsLocalizationNatIso S = CategoryTheory.NatIso.ofComponents (ModuleCat.extendScalarsLocalizationIso S) ⋯

noncomputable def ModuleCat.extendScalarsLocalizationCochainNatIso {R : Type u} [CommRing R] (S : Submonoid R) : (extendScalars (algebraMap R (Localization S))).mapHomologicalComplex (ComplexShape.up ℤ) ≅ (localizedModuleFunctor S).mapHomologicalComplex (ComplexShape.up ℤ)

The comparison on cochain complexes is induced degreewise by the canonical natural isomorphism of module functors.

Equations

• ModuleCat.extendScalarsLocalizationCochainNatIso S = CategoryTheory.NatIso.mapHomologicalComplex (ModuleCat.extendScalarsLocalizationNatIso S) (ComplexShape.up ℤ)