The weights of a Verma module and their multiplicities #

Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over a field K of characteristic zero, H a splitting Cartan subalgebra and b a base of its root system. The Verma module M(lam) is a free U(n⁻)-module of rank one on its canonical generator v_lam (TauCeti.universalEnvelopingEquivVermaModule), so a Poincaré--Birkhoff--Witt basis of U(n⁻) gives a basis of M(lam): the vectors

f_{i₁} ⋯ f_{iₖ} · v_lam, i₁ ≤ ⋯ ≤ iₖ,

for an ordered basis (f_i) of the negative nilradical n⁻. When every f_i is an H-eigenvector of weight w_i, the vector attached to the exponent n is an H-eigenvector of weight lam + ∑ᵢ nᵢ wᵢ, so the weight space M(lam)_mu is spanned by the basis vectors of that weight and its dimension is the number of exponents n with lam + ∑ᵢ nᵢ wᵢ = mu (TauCeti.finrank_weightSpace_vermaModule_eq_natCard).

The negative nilradical has such a basis made of root vectors, one for each positive root α, lying in the line L_{-α} (TauCeti.negativeNilradicalBasis). With it the count becomes the number of ways of writing lam - mu as a sum of positive roots with multiplicity, which is the Kostant partition function: the weight multiplicities of a Verma module are

dim M(lam)_mu = P(lam - mu)

(TauCeti.finrank_weightSpace_vermaModule). In particular the weights of M(lam) are exactly the elements of lam minus the monoid generated by the positive roots (TauCeti.weightSpace_vermaModule_ne_bot_iff), and M(lam) is the direct sum of its weight spaces (TauCeti.isInternal_weightSpace_vermaModule).

Main definitions #

TauCeti.vermaBasis: the basis of M(lam) obtained by applying the ordered monomials in a basis of n⁻ to the canonical generator.

Main results #

TauCeti.vermaBasis_mem_weightSpace: for a basis of n⁻ made of weight vectors, every vector of the associated basis of M(lam) is a weight vector, of the weight read off its exponent.
TauCeti.weightSpace_vermaModule_eq_span and TauCeti.finrank_weightSpace_vermaModule_eq_natCard: a weight space of M(lam) is spanned by the basis vectors of that weight, so its dimension counts the exponents of that weight.
TauCeti.finrank_weightSpace_vermaModule: dim M(lam)_mu = P(lam - mu), the Kostant partition function of lam - mu.
TauCeti.weightSpace_vermaModule_ne_bot_iff: mu is a weight of M(lam) exactly when lam - mu is a sum of positive roots.
TauCeti.iSup_weightSpace_vermaModule_eq_top and TauCeti.isInternal_weightSpace_vermaModule: the Verma module is the sum, indeed the internal direct sum, of its weight spaces.

References #

J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §20.3 and §24.1.
J. E. Humphreys, Representations of Semisimple Lie Algebras in the BGG Category O, §1.3.

The Poincaré--Birkhoff--Witt basis of a Verma module #

source

noncomputable def TauCeti.vermaBasis {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) (lam : Module.Dual K ↥H) {σ : Type w} [LinearOrder σ] (B : Module.Basis σ K ↥(negativeNilradical H b)) :

Module.Basis (σ →₀ ℕ) K (VermaModule b lam)

The Poincaré--Birkhoff--Witt basis of the Verma module attached to an ordered basis B of the negative nilradical: the vector of exponent n is the ordered monomial of Module.Basis.pbwBasis in B, with exponent n, applied to the canonical generator v_lam (TauCeti.vermaBasis_apply). It is a basis because M(lam) is a free U(n⁻)-module of rank one on v_lam.

Equations

TauCeti.vermaBasis b lam B = B.pbwBasis.map (TauCeti.universalEnvelopingEquivVermaModule b lam)

Instances For

source

theorem TauCeti.vermaBasis_apply {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) (lam : Module.Dual K ↥H) {σ : Type w} [LinearOrder σ] (B : Module.Basis σ K ↥(negativeNilradical H b)) (n : σ →₀ ℕ) :

(vermaBasis b lam B) n = (UniversalEnvelopingAlgebra.map K (negativeNilradical H b).incl) (B.pbwBasis n) • vermaGenerator b lam

The basis vector of exponent n is the ordered monomial of exponent n in B, applied to the canonical generator.

source

theorem TauCeti.vermaBasis_mem_weightSpace {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) (lam : Module.Dual K ↥H) {σ : Type w} [LinearOrder σ] (B : Module.Basis σ K ↥(negativeNilradical H b)) {w : σ → Module.Dual K ↥H} (hB : ∀ (i : σ) (h : ↥H), ⁅↑h, ↑(B i)⁆ = (w i) h • ↑(B i)) (n : σ →₀ ℕ) :

(vermaBasis b lam B) n ∈ LieModule.weightSpace (VermaModule b lam) ⇑(lam + n.sum fun (i : σ) (k : ℕ) => k • w i)

The basis vectors of a Verma module are weight vectors. If the Cartan subalgebra acts on each vector B i of the basis of n⁻ through w i, then the basis vector of exponent n has weight lam + ∑ᵢ nᵢ w i.

source

theorem TauCeti.weightSpace_vermaModule_eq_span {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) (lam : Module.Dual K ↥H) {σ : Type w} [LinearOrder σ] (B : Module.Basis σ K ↥(negativeNilradical H b)) {w : σ → Module.Dual K ↥H} (hB : ∀ (i : σ) (h : ↥H), ⁅↑h, ↑(B i)⁆ = (w i) h • ↑(B i)) (mu : Module.Dual K ↥H) :

↑(LieModule.weightSpace (VermaModule b lam) ⇑mu) = Submodule.span K (⇑(vermaBasis b lam B) '' {n : σ →₀ ℕ | (lam + n.sum fun (i : σ) (k : ℕ) => k • w i) = mu})

A weight space of a Verma module is spanned by the basis vectors of that weight. If the Cartan subalgebra acts on each vector B i of the basis of n⁻ through w i, the weight space M(lam)_mu is spanned by the basis vectors whose exponent n satisfies lam + ∑ᵢ nᵢ w i = mu.

source

theorem TauCeti.finrank_weightSpace_vermaModule_eq_natCard {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) (lam : Module.Dual K ↥H) {σ : Type w} [LinearOrder σ] (B : Module.Basis σ K ↥(negativeNilradical H b)) {w : σ → Module.Dual K ↥H} (hB : ∀ (i : σ) (h : ↥H), ⁅↑h, ↑(B i)⁆ = (w i) h • ↑(B i)) (mu : Module.Dual K ↥H) :

Module.finrank K ↥(LieModule.weightSpace (VermaModule b lam) ⇑mu) = Nat.card { n : σ →₀ ℕ // (lam + n.sum fun (i : σ) (k : ℕ) => k • w i) = mu }

The weight multiplicities of a Verma module count exponents. If the Cartan subalgebra acts on each vector B i of the basis of n⁻ through w i, then the weight space M(lam)_mu has dimension the number of exponents n with lam + ∑ᵢ nᵢ w i = mu. When there are infinitely many such exponents both sides are 0.

source

theorem TauCeti.weightSpace_vermaModule_ne_bot_iff_exists {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) (lam : Module.Dual K ↥H) {σ : Type w} [LinearOrder σ] (B : Module.Basis σ K ↥(negativeNilradical H b)) {w : σ → Module.Dual K ↥H} (hB : ∀ (i : σ) (h : ↥H), ⁅↑h, ↑(B i)⁆ = (w i) h • ↑(B i)) (mu : Module.Dual K ↥H) :

LieModule.weightSpace (VermaModule b lam) ⇑mu ≠ ⊥ ↔ ∃ (n : σ →₀ ℕ), (lam + n.sum fun (i : σ) (k : ℕ) => k • w i) = mu

The weights of a Verma module. If the Cartan subalgebra acts on each vector B i of the basis of n⁻ through w i, then mu is a weight of M(lam) exactly when it is lam + ∑ᵢ nᵢ w i for some exponent n.

The multiplicities are given by the Kostant partition function #

source

theorem TauCeti.finrank_weightSpace_vermaModule {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) (lam mu : Module.Dual K ↥H) :

Module.finrank K ↥(LieModule.weightSpace (VermaModule b lam) ⇑mu) = kostantPartition (LieAlgebra.IsKilling.rootSystem H) b (lam - mu)

The weight multiplicities of a Verma module are given by the Kostant partition function: the weight space M(lam)_mu has dimension P(lam - mu), the number of ways of writing lam - mu as a sum of positive roots with multiplicity.

source