isCentralScalar — Mathlib

English

RestrictScalars inherits a central scalar action from R on M when M is an S-module and IsCentralScalar S M holds; equivalently, op_smul_eq_smul holds: (algebraMap R S r) acting on the opposite side equals the scalar action from R.

Русский

RestrictScalars наследует центральное действие скаляра R на M при условии, что M является S-модулем и IsCentralScalar S M. Эквивалентно, выполняется op_smul_eq_smul: (algebraMap R S r) действует как скаляр S.

LaTeX

$$$$ \\text{IsCentralScalar } R (\\mathrm{RestrictScalars}(R,S,M)) $$$$

Lean4

instance isCentralScalar [Module S M] [Module Sᵐᵒᵖ M] [IsCentralScalar S M] : IsCentralScalar R (RestrictScalars R S M)
    where op_smul_eq_smul r _x := (op_smul_eq_smul (algebraMap R S r) (_ : M) :)

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