# mathlibdocumentation

algebra.lie.non_unital_non_assoc_algebra

# Lie algebras as non-unital, non-associative algebras #

The definition of Lie algebras uses the has_bracket typeclass for multiplication whereas we have a separate has_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 has_mul and has_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 #

• lie_ring.to_non_unital_non_assoc_semiring
• lie_hom.to_non_unital_alg_hom

## Tags #

lie algebra, non-unital, non-associative

A lie_ring can be regarded as a non_unital_non_assoc_semiring by turning its has_bracket (denoted ⁅, ⁆) into a has_mul (denoted *).

Equations
@[instance]
def lie_algebra.is_scalar_tower (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] :
L

Regarding the lie_ring of a lie_algebra as a non_unital_non_assoc_semiring, we can reinterpret the smul_lie law as an is_scalar_tower.

@[instance]
def lie_algebra.smul_comm_class (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] :
L

Regarding the lie_ring of a lie_algebra as a non_unital_non_assoc_semiring, we can reinterpret the lie_smul law as an smul_comm_class.

def lie_hom.to_non_unital_alg_hom {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] {L₂ : Type w} [lie_ring L₂] [ L₂] (f : L →ₗ⁅R L₂) :
L₂

Regarding the lie_ring of a lie_algebra as a non_unital_non_assoc_semiring, we can regard a lie_hom as a non_unital_alg_hom.

Equations
@[simp]
theorem lie_hom.to_non_unital_alg_hom_apply {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] {L₂ : Type w} [lie_ring L₂] [ L₂] (f : L →ₗ⁅R L₂) (ᾰ : L) :
theorem lie_hom.to_non_unital_alg_hom_injective {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] {L₂ : Type w} [lie_ring L₂] [ L₂] :