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

@[inline, reducible]

abbrev LieAlgebra.LieCharacter (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : Type (max v u)

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

theorem LieAlgebra.lieCharacter_apply_lie {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (χ : LieAlgebra.LieCharacter R L) (x : L) (y : L) : ↑χ ⁅x, y⁆ = 0

@[simp]

theorem LieAlgebra.lieCharacter_apply_lie' {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (χ : LieAlgebra.LieCharacter R L) (x : L) (y : L) : ⁅↑χ x, ↑χ y⁆ = 0

theorem LieAlgebra.lieCharacter_apply_of_mem_derived {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (χ : LieAlgebra.LieCharacter R L) {x : L} (h : x ∈ LieAlgebra.derivedSeries R L 1) : ↑χ x = 0

@[simp]

theorem LieAlgebra.lieCharacterEquivLinearDual_apply {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] [IsLieAbelian L] (χ : LieAlgebra.LieCharacter R L) : ↑LieAlgebra.lieCharacterEquivLinearDual χ = ↑χ

@[simp]

theorem LieAlgebra.lieCharacterEquivLinearDual_symm_apply {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] [IsLieAbelian L] (ψ : Module.Dual R L) : ↑LieAlgebra.lieCharacterEquivLinearDual.symm ψ = { toLinearMap := { toAddHom := ψ.toAddHom, map_smul' := (_ : ∀ (r : R) (x : L), AddHom.toFun ψ.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }, map_lie' := (_ : ∀ {x y : L}, AddHom.toFun { toAddHom := ψ.toAddHom, map_smul' := (_ : ∀ (r : R) (x : L), AddHom.toFun ψ.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom ⁅x, y⁆ = ⁅AddHom.toFun { toAddHom := ψ.toAddHom, map_smul' := (_ : ∀ (r : R) (x : L), AddHom.toFun ψ.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom x, AddHom.toFun { toAddHom := ψ.toAddHom, map_smul' := (_ : ∀ (r : R) (x : L), AddHom.toFun ψ.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom y⁆) }

def LieAlgebra.lieCharacterEquivLinearDual {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] [IsLieAbelian L] : LieAlgebra.LieCharacter R L ≃ Module.Dual R L

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