isScalarTower_of_algebra_moduleCat

English

Let k be a field, A a k-algebra, and M an A-module. Then there is a scalar tower IsScalarTower k A M, i.e., the k-action and the A-action on M are compatible: (r a) m = r (a m) for all r ∈ k, a ∈ A, m ∈ M.

Русский

Пусть k — поле, A — k-алгебра, и M — A-модуль. Тогда существует цепь скаляров IsScalarTower k A M, то есть действия k и A на M согласованы: (r a) m = r (a m) для всех r ∈ k, a ∈ A, m ∈ M.

LaTeX

$$$ IsScalarTower(k,A,M). $$$

Lean4

theorem isScalarTower_of_algebra_moduleCat (M : ModuleCat.{v} A) : IsScalarTower k A M :=
  RestrictScalars.isScalarTower k A M

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