# mathlib3documentation

algebra.lie.non_unital_non_assoc_algebra

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• commutator_ring turns a Lie ring into a non_unital_non_assoc_semiring by turning its has_bracket (denoted ⁅, ⁆) into a has_mul (denoted *).
• lie_hom.to_non_unital_alg_hom

## Tags #

lie algebra, non-unital, non-associative

def commutator_ring (L : Type v) :

Type synonym for turning a lie_ring into a non_unital_non_assoc_semiring.

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
Instances for commutator_ring
@[protected, instance]

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
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
• = show , from _inst_2
@[protected, instance]
Equations
• = show L, from _inst_3
@[protected, instance]
def lie_algebra.is_scalar_tower (R : Type u) (L : Type v) [comm_ring R] [lie_ring 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.

@[protected, instance]
def lie_algebra.smul_comm_class (R : Type u) (L : Type v) [comm_ring R] [lie_ring 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₂) :

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₂] :