English
Let S be a monoid acting on a commutative ring R with compatible actions on R and its opposite, and assume IsCentralScalar S R holds. Then the induced action of S on the free Lie algebra FreeLieAlgebra R X is central, i.e., the action commutes with the Lie algebra structure in the sense of central scalars.
Русский
Пусть S — моноид, действующий над кольцом R и над противоположной структурой R совместимо, и выполняется условие IsCentralScalar S R. Тогда на свободной Lie-алгебре FreeLieAlgebra R X действует центральный скалярный масштабирования S, т.е. действие скаляра перекрестно сLie-структурой.
LaTeX
$$$\operatorname{IsCentralScalar}(S, \mathrm{FreeLieAlgebra}_R X).$$$
Lean4
instance {S : Type*} [Monoid S] [DistribMulAction S R] [DistribMulAction Sᵐᵒᵖ R] [IsScalarTower S R R]
[IsCentralScalar S R] : IsCentralScalar S (FreeLieAlgebra R X) where
op_smul_eq_smul t := Quot.ind fun a => congr_arg (Quot.mk _) (op_smul_eq_smul t a)
