Documentation

Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra

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:

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

def CommutatorRing (L : Type v) :

Type synonym for turning a LieRing into a NonUnitalNonAssocRing.

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

Equations
Instances For

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

    Equations

    Regarding the LieRing of a LieAlgebra as a NonUnitalNonAssocRing, we can reinterpret the smul_lie law as an IsScalarTower.

    Equations
    • =

    Regarding the LieRing of a LieAlgebra as a NonUnitalNonAssocRing, 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) :
    f.toNonUnitalAlgHom 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) :
    f.toNonUnitalAlgHom 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₂) :

    Regarding the LieRing of a LieAlgebra as a NonUnitalNonAssocRing, we can regard a LieHom as a NonUnitalAlgHom.

    Equations
    • f.toNonUnitalAlgHom = { toFun := f, map_smul' := , map_zero' := , map_add' := , map_mul' := }
    Instances For
      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