English
A localized module map together with a localized module map for g and l yields an R_s-linear isomorphism between M' and N'.
Русский
Локализованное отображение модуля вместе с локализованным отображением g и l даёт R_s-линейное изоморфизм между M' и N'.
LaTeX
$$$\\text{mapEquiv}(e) : M' \\simeq_{R_s} N'$$$
Lean4
/-- An `R`-module isomorphism `M ≃ₗ[R] N` gives an `Rₛ`-module isomorphism `Mₛ ≃ₗ[Rₛ] Nₛ`. -/
@[simps!]
noncomputable def mapEquiv (e : M ≃ₗ[R] N) : M' ≃ₗ[Rₛ] N' :=
LinearEquiv.ofLinear (IsLocalizedModule.mapExtendScalars S f g Rₛ e)
(IsLocalizedModule.mapExtendScalars S g f Rₛ e.symm)
(by
apply LinearMap.restrictScalars_injective R
apply IsLocalizedModule.linearMap_ext S g g
ext; simp)
(by
apply LinearMap.restrictScalars_injective R
apply IsLocalizedModule.linearMap_ext S f f
ext; simp)
