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 #
Tags #
lie algebra, lie character
@[reducible, inline]
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.
Equations
- LieAlgebra.LieCharacter R L = (L →ₗ⁅R⁆ R)
Instances For
theorem
LieAlgebra.lieCharacter_apply_lie
{R : Type u}
{L : Type v}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(χ : LieAlgebra.LieCharacter R L)
(x y : L)
:
@[simp]
theorem
LieAlgebra.lieCharacter_apply_lie'
{R : Type u}
{L : Type v}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(χ : LieAlgebra.LieCharacter R L)
(x y : L)
:
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
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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 := ψ, map_lie' := ⋯ }