English
There is a canonical isomorphism showing that the localized module M' carries an A-module structure such that the scalar action is compatible with the R-action via the isomorphism to the Endomorphism ring.
Русский
Существует каноническое тождество, показывающее, что локализованный модуль M' имеет структуру A-модуля и совместимость действия скаляров прошлой структуры через изоморфизм к кольцу концевых отображений.
LaTeX
$$$$ \\text{IsScalarTower } R A M' $$$$
Lean4
/-- Formula for `IsLocalizedModule.map` when each localized module is a `LocalizedModule`. -/
theorem map_LocalizedModules (g : M₀ →ₗ[R] M₁) (m : M₀) (s : S) :
((map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m s) = LocalizedModule.mk (g m) s :=
by
have := (iso_apply_mk S (mkLinearMap S M₁) (g m) s).symm
rw [iso_localizedModule_eq_refl, refl_apply] at this
simpa [map, lift, iso_localizedModule_eq_refl S M₀]
