English
Let R be a commutative ring and L a Lie algebra over R. Regard the Lie ring of L as a nonunital nonassociative ring with multiplication given by the Lie bracket. Then the scalar action of R on this ring commutes with multiplication, i.e. for all r ∈ R and a,b ∈ CommutatorRing L, (r · a) · b = a · (r · b).
Русский
Пусть R — коммутативная кольца, а L — Ли-алгебра над R. Рассмотрим Lie-порожденное кольцо CommutatorRing(L) как непостоянное немоноидальное кольцо с умножением, заданным наiel-bracket. Тогда действие скаляра R на это кольцо коммутирует с умножением: для любых r ∈ R и a,b ∈ CommutatorRing L имеем (r · a) · b = a · (r · b).
LaTeX
$$$ \\forall r \\in R,\\ a,b \\in \\mathrm{CommutatorRing}(L),\\ (r \\cdot a) \\cdot b = a \\cdot (r \\cdot b). $$$
Lean4
/-- Regarding the `LieRing` of a `LieAlgebra` as a `NonUnitalNonAssocRing`, we can
reinterpret the `lie_smul` law as an `SMulCommClass`. -/
instance smulCommClass : SMulCommClass R (CommutatorRing L) (CommutatorRing L) :=
⟨fun t x y => (lie_smul t x y).symm⟩
