Lie algebras of associative algebras #
This file defines the Lie algebra structure that arises on an associative algebra via the ring commutator.
Since the linear endomorphisms of a Lie algebra form an associative algebra, one can define the adjoint action as a morphism of Lie algebras from a Lie algebra to its linear endomorphisms. We make such a definition in this file.
Main definitions #
LieAlgebra.ofAssociativeAlgebra
LieAlgebra.ofAssociativeAlgebraHom
LieModule.toEndomorphism
LieAlgebra.ad
LinearEquiv.lieConj
AlgEquiv.toLieEquiv
Tags #
lie algebra, ring commutator, adjoint action
The bracket operation for rings is the ring commutator, which captures the extent to which a ring is commutative. It is identically zero exactly when the ring is commutative.
An associative ring gives rise to a Lie ring by taking the bracket to be the ring commutator.
We can regard a module over an associative ring A
as a Lie ring module over A
with Lie
bracket equal to its ring commutator.
Note that this cannot be a global instance because it would create a diamond when M = A
,
specifically we can build two mathematically-different bracket A A
s:
@Ring.bracket A _
which says⁅a, b⁆ = a * b - b * a
(@LieRingModule.ofAssociativeModule A _ A _ _).toBracket
which says⁅a, b⁆ = a • b
(and thus⁅a, b⁆ = a * b
)
See note [reducible non-instances]
Instances For
An associative algebra gives rise to a Lie algebra by taking the bracket to be the ring commutator.
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.
A Lie module yields a Lie algebra morphism into the linear endomorphisms of the module.
See also LieModule.toModuleHom
.
Instances For
The adjoint action of a Lie algebra on itself.
Instances For
A subalgebra of an associative algebra is a Lie subalgebra of the associated Lie algebra.
Instances For
A linear equivalence of two modules induces a Lie algebra equivalence of their endomorphisms.