English
For a finitely presented M, the canonical linear equivalence on extend scalars evaluated at f equals the mapExtendScalars applied to f.
Русский
Для модуля с конечной презентацией, применение канонического линейного эквивалента кExtendScalars имеет одинаковый вид с отображением mapExtendScalars на f.
LaTeX
$$$$ \\text{Module.FinitePresentation.linearEquivMapExtendScalars } S ((\\mathrm{LocalizedModule.mkLinearMap} S (M \\to N)) f) = (\\mathrm{IsLocalizedModule.mapExtendScalars} S (\\mathrm{LocalizedModule.mkLinearMap} S M) (\\mathrm{LocalizedModule.mkLinearMap} S N) (\\mathrm{Localization} S)) f. $$$$
Lean4
/-- Let `M` be a finitely presented `R`-module, `N` a `R`-module, `S : Submonoid R`.
The linear equivalence between the `M →ₗ[R] N` localized at `S` and
`LocalizedModule S M →ₗ[Localization S] LocalizedModule S N`
-/
noncomputable def linearEquivMapExtendScalars [Module.FinitePresentation R M] :=
IsLocalizedModule.linearEquiv S (LocalizedModule.mkLinearMap S (M →ₗ[R] N))
(IsLocalizedModule.mapExtendScalars S (LocalizedModule.mkLinearMap S M) (LocalizedModule.mkLinearMap S N)
(Localization S))
