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 #

Tags #

lie algebra, lie character

source

@[reducible]

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

Type (max v u)

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

source

@[simp]

theorem lie_algebra.lie_character_apply_lie {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (χ : lie_algebra.lie_character R L) (x y : L) :

⇑χ ⁅x, y⁆ = 0

source

theorem lie_algebra.lie_character_apply_of_mem_derived {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (χ : lie_algebra.lie_character R L) {x : L} (h : x ∈ lie_algebra.derived_series R L 1) :

⇑χ x = 0

source

@[simp]

theorem lie_algebra.lie_character_equiv_linear_dual_symm_apply_to_linear_map_apply {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] [is_lie_abelian L] (ψ : module.dual R L) (ᾰ : L) :

⇑((⇑(lie_algebra.lie_character_equiv_linear_dual.symm) ψ).to_linear_map) ᾰ = ψ.to_fun ᾰ

source

@[simp]

theorem lie_algebra.lie_character_equiv_linear_dual_symm_apply_apply {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] [is_lie_abelian L] (ψ : module.dual R L) (ᾰ : L) :

⇑(⇑(lie_algebra.lie_character_equiv_linear_dual.symm) ψ) ᾰ = ψ.to_fun ᾰ

source

def lie_algebra.lie_character_equiv_linear_dual {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] [is_lie_abelian L] :

lie_algebra.lie_character R L ≃ module.dual R L

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

Equations

lie_algebra.lie_character_equiv_linear_dual = {to_fun := λ (χ : lie_algebra.lie_character R L), ↑χ, inv_fun := λ (ψ : module.dual R L), {to_linear_map := {to_fun := ψ.to_fun, map_add' := _, map_smul' := _}, map_lie' := _}, left_inv := _, right_inv := _}

source

@[simp]

theorem lie_algebra.lie_character_equiv_linear_dual_apply {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] [is_lie_abelian L] (χ : lie_algebra.lie_character R L) :

⇑lie_algebra.lie_character_equiv_linear_dual χ = ↑χ