LocalizedModule is module tensor Localization

Stream: Is there code for X?

[Kevin Buzzard]

I want that $M_P=R_P\otimes_RM$. I was certainly expecting to find it but couldn't. Am I looking for the wrong thing?

import Mathlib

universe u v w

variable {R : Type u} [CommSemiring R] (S : Submonoid R)
variable (M : Type v) [AddCommMonoid M] [Module R M]

open TensorProduct

-- Do we not have this?
example : LocalizedModule S M  ≃ₗ[R] (Localization S) ⊗[R] M := sorry

-- If not, presumably we get it from `IsLocalizedModule.iso`.

-- But do we not even have _this_??
variable (A : Type w) [Semiring A] [Algebra R A] in
noncomputable def TensorProduct.includeRight : M →ₗ[R] A ⊗[R] M where
  toFun m := 1 ⊗ₜ m
  map_add' := tmul_add 1
  map_smul' r := tmul_smul r 1

instance : IsLocalizedModule S (TensorProduct.includeRight M (Localization S)) where
  map_units x := sorry -- presumably true
  surj' := sorry -- presumably true
  exists_of_eq := sorry -- presumably true

noncomputable example : LocalizedModule S M  ≃ₗ[R] (Localization S) ⊗[R] M :=
  IsLocalizedModule.iso S (TensorProduct.includeRight M (Localization S))

[Junyan Xu]

import Mathlib

universe u v w

variable {R : Type u} [CommSemiring R] (S : Submonoid R)
variable (M : Type v) [AddCommMonoid M] [Module R M]

open TensorProduct

noncomputable example : LocalizedModule S M ≃ₗ[R] (Localization S) ⊗[R] M :=
  (IsLocalizedModule.isBaseChange S _ <| LocalizedModule.mkLinearMap S M).equiv.symm.restrictScalars R

[Junyan Xu]

Maybe this should be added to mathlib