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 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

• CommutatorRing L = L

instance instNonUnitalNonAssocSemiringCommutatorRing (L : Type v) [LieRing L] : NonUnitalNonAssocSemiring (CommutatorRing L)

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

Equations

• instNonUnitalNonAssocSemiringCommutatorRing L = let_fun this := let __src := inferInstance; NonUnitalNonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯; this

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

Equations

• ⋯ = inst

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 = let_fun this := inferInstance; this

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

Equations

• LieAlgebra.instLieAlgebraCommutatorRingInstLieRingCommutatorRing R L = let_fun this := inferInstance; this

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 NonUnitalNonAssocSemiring, we can reinterpret the smul_lie law as an IsScalarTower.

Equations

• ⋯ = ⋯

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 NonUnitalNonAssocSemiring, we can reinterpret the lie_smul law as an SMulCommClass.

Equations

• ⋯ = ⋯

@[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) : (LieHom.toNonUnitalAlgHom f) 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) : (LieHom.toNonUnitalAlgHom f) a = f a

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 NonUnitalNonAssocSemiring, we can regard a LieHom as a NonUnitalAlgHom.

Equations

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

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 LieHom.toNonUnitalAlgHom