English
Let k be a field, A a k-algebra, and M an object of ModuleCat A. Then M, viewed as an A-module, has a canonical structure of a k-module via restriction of scalars.
Русский
Пусть k — поле, A — k-алгебра, и M — объект ModuleCat A. Рассматривая M как модуль над A, получаем каноническую структуру k-модуля через ограничение скаляров.
LaTeX
$$$ \\forall M\\in \\mathrm{ModuleCat}(A),\\; M \\text{ carries a canonical } k\\text{-module structure via restriction of scalars}. $$$
Lean4
/-- Type synonym for considering a module over a `k`-algebra as a `k`-module. -/
def moduleOfAlgebraModule (M : ModuleCat.{v} A) : Module k M :=
RestrictScalars.module k A M