English
An R-linear map f between localized modules extends to an A-linear map by defining its action on M with the same underlying function, and using the localization to interpret scalars from A.
Русский
Линейное по отношению к R отображение f между локализованными модулями можно рассмотреть как A‑линейное отображение, задатую через ту же функцию и локализацию для трактовки скаляров из A.
LaTeX
$$$\\text{extendScalarsOfIsLocalization}(f) : M \\to_A N \\text{ defined by } \\text{toFun}=f,\\; \\text{map\\_add}'=f.map\\_add,\\; \\text{map\\_smul}'=\\big( \\text{IsLocalization.linearMap_compatibleSMul} \\; S \\; A \\; M \\; N \\big).map\\_smul _ $$$
Lean4
/-- An `R`-linear map between two `S⁻¹R`-modules is actually `S⁻¹R`-linear. -/
def extendScalarsOfIsLocalization (f : M →ₗ[R] N) : M →ₗ[A] N
where
toFun := f
map_add' := f.map_add
map_smul' := (IsLocalization.linearMap_compatibleSMul S A M N).map_smul _
