isCentralScalar — Mathlib

English

If S acts centrally on M, then it acts centrally on the quotient M/P as well: the S-action commutes with the R-action on the quotient.

Русский

Если S действует как центральный скаляр на M, то он действует как центральный скаляр и на фактор-модуле M/P: действие S коммутирует с действием R на фактор-модуле.

LaTeX

$$$\forall s \in S, \forall r \in R,\forall [x] \in M/P,\ s \cdot (r \cdot [x]) = r \cdot (s \cdot [x])$$$

Lean4

instance isCentralScalar [SMul Sᵐᵒᵖ R] [SMul Sᵐᵒᵖ M] [IsScalarTower Sᵐᵒᵖ R M] [IsCentralScalar S M] :
    IsCentralScalar S (M ⧸ P) where op_smul_eq_smul _x := Quotient.ind' fun _z => congr_arg mk <| op_smul_eq_smul _ _

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