# 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 and Bracket 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 a NonUnitalNonAssocSemiring by turning its Bracket (denoted ⁅, ⁆) into a Mul (denoted *).
• LieHom.toNonUnitalAlgHom

## Tags #

lie algebra, non-unital, non-associative

def CommutatorRing (L : Type v) :

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 *).

Equations
Instances For

A LieRing can be regarded as a NonUnitalNonAssocSemiring by turning its Bracket (denoted ⁅, ⁆) into a Mul (denoted *).

Equations
• = let_fun this := let __src := inferInstance; ; this
Equations
• = inst
Equations
Equations
• = let_fun this := inferInstance; this
instance LieAlgebra.instCommutatorRing (R : Type u) (L : Type v) [] [] [] :
Equations
• = let_fun this := inferInstance; this
instance LieAlgebra.isScalarTower (R : Type u) (L : Type v) [] [] [] :

Regarding the LieRing of a LieAlgebra as a NonUnitalNonAssocSemiring, we can reinterpret the smul_lie law as an IsScalarTower.

Equations
• =
instance LieAlgebra.smulCommClass (R : Type u) (L : Type v) [] [] [] :

Regarding the LieRing of a LieAlgebra as a NonUnitalNonAssocSemiring, we can reinterpret the lie_smul law as an SMulCommClass.

Equations
• =
@[simp]
theorem LieHom.toNonUnitalAlgHom_toFun {R : Type u} {L : Type v} [] [] [] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R L₂) (a : L) :
f.toNonUnitalAlgHom a = f a
@[simp]
theorem LieHom.toNonUnitalAlgHom_apply {R : Type u} {L : Type v} [] [] [] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R L₂) (a : L) :
f.toNonUnitalAlgHom a = f a
def LieHom.toNonUnitalAlgHom {R : Type u} {L : Type v} [] [] [] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R L₂) :

Regarding the LieRing of a LieAlgebra as a NonUnitalNonAssocSemiring, we can regard a LieHom as a NonUnitalAlgHom.

Equations
• f.toNonUnitalAlgHom = { toFun := f, map_smul' := , map_zero' := , map_add' := , map_mul' := }
Instances For
theorem LieHom.toNonUnitalAlgHom_injective {R : Type u} {L : Type v} [] [] [] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] :
Function.Injective LieHom.toNonUnitalAlgHom