moduleOfAlgebraModule — Mathlib

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

Похожие утверждения