# mathlib3documentation

algebra.lie.character

# Characters of Lie algebras #

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

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 #

• lie_algebra.lie_character
• lie_algebra.lie_character_equiv_linear_dual

## Tags #

lie algebra, lie character

@[reducible]
def lie_algebra.lie_character (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] :
Type (max v u)

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

@[simp]
theorem lie_algebra.lie_character_apply_lie {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (χ : L) (x y : L) :
χ x, y = 0
theorem lie_algebra.lie_character_apply_of_mem_derived {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (χ : L) {x : L} (h : x ) :
χ x = 0
@[simp]
@[simp]
theorem lie_algebra.lie_character_equiv_linear_dual_symm_apply_apply {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (ψ : L) (ᾰ : L) :

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

Equations
@[simp]
theorem lie_algebra.lie_character_equiv_linear_dual_apply {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (χ : L) :