# Characters of Lie algebras #

A character of a Lie algebra L over a commutative ring R is a morphism of Lie algebras L → R, where R is regarded as a Lie algebra over itself via the ring commutator. For an Abelian Lie algebra (e.g., a Cartan subalgebra of a semisimple Lie algebra) a character is just a linear form.

## Main definitions #

• LieAlgebra.LieCharacter
• LieAlgebra.lieCharacterEquivLinearDual

## Tags #

lie algebra, lie character

@[reducible, inline]
abbrev LieAlgebra.LieCharacter (R : Type u) (L : Type v) [] [] [] :
Type (max v u)

A character of a Lie algebra is a morphism to the scalars.

Equations
Instances For
theorem LieAlgebra.lieCharacter_apply_lie {R : Type u} {L : Type v} [] [] [] (χ : ) (x : L) (y : L) :
χ x, y = 0
@[simp]
theorem LieAlgebra.lieCharacter_apply_lie' {R : Type u} {L : Type v} [] [] [] (χ : ) (x : L) (y : L) :
χ x, χ y = 0
theorem LieAlgebra.lieCharacter_apply_of_mem_derived {R : Type u} {L : Type v} [] [] [] (χ : ) {x : L} (h : x ) :
χ x = 0
@[simp]
theorem LieAlgebra.lieCharacterEquivLinearDual_apply {R : Type u} {L : Type v} [] [] [] [] (χ : ) :
LieAlgebra.lieCharacterEquivLinearDual χ = χ
@[simp]
theorem LieAlgebra.lieCharacterEquivLinearDual_symm_apply {R : Type u} {L : Type v} [] [] [] [] (ψ : ) :
LieAlgebra.lieCharacterEquivLinearDual.symm ψ = { toLinearMap := ψ, map_lie' := }
def LieAlgebra.lieCharacterEquivLinearDual {R : Type u} {L : Type v} [] [] [] [] :

For an Abelian Lie algebra, characters are just linear forms.

Equations
• One or more equations did not get rendered due to their size.
Instances For