mathlib documentation

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:

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 #

Tags #

lie algebra, non-unital, non-associative

@[instance]
def lie_algebra.is_scalar_tower (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R 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] [lie_algebra R 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] [lie_algebra R L] {L₂ : Type w} [lie_ring L₂] [lie_algebra R 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] [lie_algebra R L] {L₂ : Type w} [lie_ring L₂] [lie_algebra R 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] [lie_algebra R L] {L₂ : Type w} [lie_ring L₂] [lie_algebra R L₂] :