Extension of scalars

This file records two facts about Mathlib's extension of scalars ModuleCat.extendScalars.

• Extension of scalars carries multiplication by a scalar to multiplication by its image (TauCeti.ModuleCat.extendScalars_map_smul_id). This transports the curvature equations of a matrix factorization when its components are extended along a ring map, so the resulting factorization has the image potential.
• Extension of scalars to a localization T⁻¹R is localization: for an R-module M, T⁻¹R ⊗_R M is isomorphic to the localized module T⁻¹M as a T⁻¹R-module, by s ⊗ m ↦ s • m / 1 (ModuleCat.extendScalarsLocalizationIso). This identifies the restriction of the quasi-coherent sheaf M~ on Spec R to a basic open D(r) with the sheaf associated with M_r on Spec R_r.

@[simp]

theorem TauCeti.ModuleCat.extendScalars_map_smul_id {S : Type u} {T : Type v} [CommRing S] [CommRing T] {w : S} (f : S →+* T) (M : ModuleCat S) : (ModuleCat.extendScalars f).map (w • CategoryTheory.CategoryStruct.id M) = f w • CategoryTheory.CategoryStruct.id ((ModuleCat.extendScalars f).obj M)

Scalar extension sends multiplication by a scalar to multiplication by its image.

noncomputable def ModuleCat.extendScalarsLocalizationIso {R : Type u} [CommRing R] (M : ModuleCat R) (T : Submonoid R) : (extendScalars (algebraMap R (Localization T))).obj M ≅ ↧(LocalizedModule T ↑M)

Extension of scalars to the localization T⁻¹R is localization: T⁻¹R ⊗_R M is isomorphic to the localized module T⁻¹M, by s ⊗ m ↦ s • m / 1.

This transports LocalizedModule.equivTensorProduct across the Module.compHom structure used by ModuleCat.extendScalars.

Equations

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

@[simp]

theorem ModuleCat.extendScalarsLocalizationIso_hom_one_tmul {R : Type u} [CommRing R] (M : ModuleCat R) (T : Submonoid R) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (M.extendScalarsLocalizationIso T).hom) (1 ⊗ₜ[R] m) = LocalizedModule.mk m 1

extendScalarsLocalizationIso sends 1 ⊗ m to m / 1.

@[simp]

theorem ModuleCat.extendScalarsLocalizationIso_inv_mk_one {R : Type u} [CommRing R] (M : ModuleCat R) (T : Submonoid R) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (M.extendScalarsLocalizationIso T).inv) (LocalizedModule.mk m 1) = 1 ⊗ₜ[R] m

The inverse of extendScalarsLocalizationIso sends m / 1 to 1 ⊗ m.

@[simp]

theorem ModuleCat.extendScalarsLocalizationIso_hom_tmul {R : Type u} [CommRing R] (M : ModuleCat R) (T : Submonoid R) (s : Localization T) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (M.extendScalarsLocalizationIso T).hom) (s ⊗ₜ[R] m) = s • LocalizedModule.mk m 1

extendScalarsLocalizationIso sends a pure tensor to the scalar multiple of m / 1.

@[simp]

theorem ModuleCat.extendScalarsLocalizationIso_inv_mk {R : Type u} [CommRing R] (M : ModuleCat R) (T : Submonoid R) (m : ↑M) (t : ↥T) : (CategoryTheory.ConcreteCategory.hom (M.extendScalarsLocalizationIso T).inv) (LocalizedModule.mk m t) = Localization.mk 1 t ⊗ₜ[R] m

The inverse of extendScalarsLocalizationIso sends m / t to t⁻¹ ⊗ m.