English
A representation of an associative algebra A on a module M also yields a representation of A regarded as a Lie algebra, with the Lie action given by the same underlying action: for a ∈ A and m ∈ M, ⁅a, m⁆ = a · m.
Русский
Представление ассоциативной алгебры A на модуле M даёт представление A как Lie-алгебры, причем действие задаётся тем же действием модуля: ⁅a, m⁆ = a·m.
LaTeX
$$$$[a,m] = a\cdot m \quad (a \in A, \ m \in M).$$$$
Lean4
/-- A representation of an associative algebra `A` is also a representation of `A`, regarded as a
Lie algebra via the ring commutator.
See the comment at `LieRingModule.ofAssociativeModule` for why the possibility `M = A` means
this cannot be a global instance. -/
theorem ofAssociativeModule : LieModule R A M
where
smul_lie := smul_assoc
lie_smul := smul_algebra_smul_comm
