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

source

def commutator_ring (L : Type v) :

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

commutator_ring L = L

Instances for commutator_ring

source

@[protected, instance]

def commutator_ring.non_unital_non_assoc_semiring (L : Type v) [lie_ring L] :

non_unital_non_assoc_semiring (commutator_ring L)

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

commutator_ring.non_unital_non_assoc_semiring L = show non_unital_non_assoc_semiring L, from {add := add_comm_monoid.add infer_instance, add_assoc := _, zero := add_comm_monoid.zero infer_instance, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul infer_instance, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_bracket.bracket lie_ring_module.to_has_bracket, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _}

source

@[protected, instance]

def lie_algebra.commutator_ring.nonempty (L : Type v) [nonempty L] :

nonempty (commutator_ring L)

source

@[protected, instance]

def lie_algebra.commutator_ring.inhabited (L : Type v) [inhabited L] :

inhabited (commutator_ring L)

Equations

lie_algebra.commutator_ring.inhabited L = _inst_4

source

@[protected, instance]

def lie_algebra.commutator_ring.lie_ring (L : Type v) [lie_ring L] :

lie_ring (commutator_ring L)

Equations

lie_algebra.commutator_ring.lie_ring L = show lie_ring L, from _inst_2

source

@[protected, instance]

def lie_algebra.commutator_ring.lie_algebra (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :

lie_algebra R (commutator_ring L)

Equations

lie_algebra.commutator_ring.lie_algebra R L = show lie_algebra R L, from _inst_3

source

@[protected, instance]

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

is_scalar_tower R (commutator_ring L) (commutator_ring 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.

source

@[protected, instance]

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

smul_comm_class R (commutator_ring L) (commutator_ring 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.

source

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

commutator_ring L →ₙₐ[R] commutator_ring 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

f.to_non_unital_alg_hom = {to_fun := ⇑f, map_smul' := _, map_zero' := _, map_add' := _, map_mul' := _}

source

@[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) :

⇑(f.to_non_unital_alg_hom) ᾰ = ⇑f ᾰ

source

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

function.injective lie_hom.to_non_unital_alg_hom