English
For any linear map f and elements x,y with a witness that y is localized, map S f acting on the localized element mk x y equals LocalizedModule.mk (f x) y.
Русский
Для линейного отображения f и элементов x и y с доказательством локализации, отображение map на локализованный элемент mk x y равно LocalizedModule.mk (f x) y.
LaTeX
$$$\\text{map S } f (.\\!\\mathrm{mk} x y) = \\mathrm{LocalizedModule.mk}(f x) y$$$
Lean4
/-- A linear map `M →ₗ[R] N` gives a map between localized modules `Mₛ →ₗ[Rₛ] Nₛ`. -/
noncomputable def map : (M →ₗ[R] N) →ₗ[R] (LocalizedModule S M →ₗ[Localization S] LocalizedModule S N) :=
IsLocalizedModule.mapExtendScalars S (LocalizedModule.mkLinearMap S M) (LocalizedModule.mkLinearMap S N)
(Localization S)
