English
There is a canonical R-algebra homomorphism from the original coefficient algebra S to the R-linear endomorphisms of the restricted scalar module RestrictScalars R S M; this map encodes the S-action on M after restricting scalars from S to R.
Русский
Существует каноническое R-алгеброгомоморфное отображение из исходного алгебраического кольца S в кольцо R-линейных преобразований End_R(RestrictScalars R S M); это отображение кодирует действие S на M после ограничения скаляров с S до R.
LaTeX
$$$\\mathrm{lsmul}: S \\to_{\\mathsf{Alg}_R} \\mathrm{End}_R(\\mathrm{RestrictScalars}(R,S,M))$$$
Lean4
/-- The `R`-algebra homomorphism from the original coefficient algebra `S` to endomorphisms
of `RestrictScalars R S M`.
-/
def lsmul [Module S M] : S →ₐ[R] Module.End R (RestrictScalars R S M) :=
-- We use `RestrictScalars.moduleOrig` in the implementation,
-- but not in the type.
letI : Module S (RestrictScalars R S M) := RestrictScalars.moduleOrig R S M
Algebra.lsmul R R (RestrictScalars R S M)
