English
There is a canonical linear isomorphism between the localized module LocalizedModule S M and Localization S ⊗_R M, giving the standard tensor-product realization of localization.
Русский
Существует каноническое линейное изоморфизм между локализованным модулем LocalizedModule S M и тензорным продуктом Localization S ⊗_R M, реализующее локализацию через тензор-произведение.
LaTeX
$$$\text{LocalizedModule } S M \cong_\text{lin} (\operatorname{Localization} S) \otimes_R M$$$
Lean4
/-- The map `(f : M →ₗ[R] M')` is a localization of modules iff the map
`(Localization S) × M → N, (s, m) ↦ s • f m` is the tensor product (insomuch as it is the universal
bilinear map).
In particular, there is an isomorphism between `LocalizedModule S M` and `(Localization S) ⊗[R] M`
given by `m/s ↦ (1/s) ⊗ₜ m`.
-/
theorem isLocalizedModule_iff_isBaseChange : IsLocalizedModule S f ↔ IsBaseChange A f :=
by
refine ⟨fun _ ↦ IsLocalizedModule.isBaseChange S A f, fun h ↦ ?_⟩
have : IsBaseChange A (LocalizedModule.mkLinearMap S M) := IsLocalizedModule.isBaseChange S A _
let e := (this.equiv.symm.trans h.equiv).restrictScalars R
convert IsLocalizedModule.of_linearEquiv S (LocalizedModule.mkLinearMap S M) e
ext
rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, LinearEquiv.restrictScalars_apply,
LinearEquiv.trans_apply, IsBaseChange.equiv_symm_apply, IsBaseChange.equiv_tmul, one_smul]
