English
There is a canonical linear equivalence between the localization of the Hom-set and the Hom-set of the localized modules:\nHom_R(M,N) localized is equivalent to Hom_{R_S}(M_S,N_S).
Русский
Существует каноническое линейное эквивалентное отображение между локализацией множества гомоморфизмов и множеством гомоморфизмов локализованных модулей: локализация Hom_R(M,N) эквивалентна Hom_{R_S}(M_S,N_S).
LaTeX
$$$$ \\mathrm{Loc}_S(\\mathrm{Hom}_R(M,N)) \\cong \\mathrm{Hom}_{R_S}(M_S,N_S). $$$$
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 →ₗ[R] LocalizedModule S N`
-/
noncomputable def linearEquivMap [Module.FinitePresentation R M] :=
IsLocalizedModule.linearEquiv S (LocalizedModule.mkLinearMap S (M →ₗ[R] N))
(IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M) (LocalizedModule.mkLinearMap S N))
