Lie algebras as non-unital, non-associative algebras #
The definition of Lie algebras uses the Bracket
typeclass for multiplication whereas we have a
separate Mul
typeclass used for general algebras.
It is useful to have a special typeclass for Lie algebras because:
- it enables us to use the traditional notation
⁅x, y⁆
for the Lie multiplication, - associative algebras carry a natural Lie algebra structure via the ring commutator and so we need
them to carry both
Mul
andBracket
simultaneously, - more generally, Poisson algebras (not yet defined) need both typeclasses.
However there are times when it is convenient to be able to regard a Lie algebra as a general algebra and we provide some basic definitions for doing so here.
Main definitions #
CommutatorRing
turns a Lie ring into aNonUnitalNonAssocSemiring
by turning itsBracket
(denoted⁅, ⁆
) into aMul
(denoted*
).LieHom.toNonUnitalAlgHom
Tags #
lie algebra, non-unital, non-associative
Type synonym for turning a LieRing
into a NonUnitalNonAssocSemiring
.
A LieRing
can be regarded as a NonUnitalNonAssocSemiring
by turning its
Bracket
(denoted ⁅, ⁆
) into a Mul
(denoted *
).
Instances For
A LieRing
can be regarded as a NonUnitalNonAssocSemiring
by turning its
Bracket
(denoted ⁅, ⁆
) into a Mul
(denoted *
).
Regarding the LieRing
of a LieAlgebra
as a NonUnitalNonAssocSemiring
, we can
reinterpret the smul_lie
law as an IsScalarTower
.
Regarding the LieRing
of a LieAlgebra
as a NonUnitalNonAssocSemiring
, we can
reinterpret the lie_smul
law as an SMulCommClass
.
Regarding the LieRing
of a LieAlgebra
as a NonUnitalNonAssocSemiring
, we can
regard a LieHom
as a NonUnitalAlgHom
.