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

Tags

lie algebra, non-unital, non-associative

def CommutatorRing (L : Type v) : Type v

Type synonym for turning a LieRing into a NonUnitalNonAssocRing.

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

Equations

• CommutatorRing L = L

instance instNonUnitalNonAssocRingCommutatorRing (L : Type v) [LieRing L] : NonUnitalNonAssocRing (CommutatorRing L)

Equations

• instNonUnitalNonAssocRingCommutatorRing L = LieRing.toNonUnitalNonAssocRing L

instance LieAlgebra.instNonemptyCommutatorRing (L : Type v) [Nonempty L] : Nonempty (CommutatorRing L)

instance LieAlgebra.instInhabitedCommutatorRing (L : Type v) [Inhabited L] : Inhabited (CommutatorRing L)

Equations

• LieAlgebra.instInhabitedCommutatorRing L = inst✝

instance LieAlgebra.instLieRingCommutatorRing (L : Type v) [LieRing L] : LieRing (CommutatorRing L)

Equations

• LieAlgebra.instLieRingCommutatorRing L = inferInstance

instance LieAlgebra.instCommutatorRing (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : LieAlgebra R (CommutatorRing L)

Equations

• LieAlgebra.instCommutatorRing R L = inferInstance

instance LieAlgebra.isScalarTower (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : IsScalarTower R (CommutatorRing L) (CommutatorRing L)

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

instance LieAlgebra.smulCommClass (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : SMulCommClass R (CommutatorRing L) (CommutatorRing L)

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

def LieHom.toNonUnitalAlgHom {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) : CommutatorRing L →ₙₐ[R] CommutatorRing L₂

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

Equations

• f.toNonUnitalAlgHom = { toFun := ⇑f, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

@[simp]

theorem LieHom.toNonUnitalAlgHom_apply {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (a : L) : f.toNonUnitalAlgHom a = f a

@[simp]

theorem LieHom.toNonUnitalAlgHom_toFun {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (a : L) : f.toNonUnitalAlgHom a = f a

theorem LieHom.toNonUnitalAlgHom_injective {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] : Function.Injective toNonUnitalAlgHom