The Weyl character formula #
Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over an algebraically
closed field of characteristic zero, H a Cartan subalgebra, b a base of its root system, and
M a finite-dimensional module generated by a highest weight vector of weight lam. With
c(χ) = ⟨χ + ρ, χ + ρ⟩ - ⟨ρ, ρ⟩ the Casimir scalar (TauCeti.casimirScalar), this file proves
that c takes the single value c(lam) on the support of the product ch M · Δ of the formal
character with the Weyl denominator Δ = ∏_{α>0}(1 - e^{-α}).
Since c separates the dominant integral weights below lam, it follows that ch M · Δ vanishes
at every dominant integral weight other than lam, where its coefficient is 1. These are the
dominant integral coefficients through which
TauCeti.formalCharacter_mul_weylDenominator_eq_of_forall_coeff_isDominantIntegral_eq determines
ch M · Δ. The Weyl numerator N(lam) = ∑_{w ∈ W} sgn(w) e^{w ⬝ lam} has the very same dominant
integral coefficients, by TauCeti.coeff_weylNumerator_self_of_dominantIntegral and
TauCeti.coeff_weylNumerator_eq_zero_of_dominantIntegral_of_ne, and is supported in lam - Q⁺
as well, so the two are equal: that is the Weyl character formula, proved at the end of this
file.
The argument #
Write m(χ) = dim M_χ and σ_T = ∑_{α ∈ T} α for a set T of positive roots, so that the
coefficient of ch M · Δ at χ is ∑_T (-1)^{|T|} m(χ + σ_T). Multiply the T-th term by
c(lam) - c(χ) and split this as (c(lam) - c(χ + σ_T)) + (c(χ + σ_T) - c(χ)).
- By
TauCeti.freudenthal_multiplicity_formula,(c(lam) - c(μ)) m(μ)is twice the sum over the positive rootsαof the Freudenthal string sums∑_{j ≥ 1} m(μ + jα) ⟨μ + jα, α⟩. c(χ + σ) - c(χ) = 2⟨χ + σ, σ⟩ - c(-σ), and⟨χ + σ_T, σ_T⟩is the sum of the pairings with the rootsα ∈ T.
For each positive root α, the string sum at μ is the string sum at μ + α plus
m(μ + α) ⟨μ + α, α⟩; pairing the sets T ∌ α with T ∪ {α} therefore cancels the string sums
against the root pairings. What survives is -∑_T (-1)^{|T|} c(-σ_T) m(χ + σ_T), which groups
into -∑_x c(x) Δ_x m(χ - x). This vanishes because c vanishes on the support of Δ
(TauCeti.casimirScalar_eq_zero_of_coeff_weylDenominator_ne_zero): restricted to the weights
where c ≠ 0, the denominator is still alternating for the dot action (c is dot invariant),
lies in the negative root cone and has no dominant integral weight in its support, so it is zero
by TauCeti.IsDotAlternating.eq_zero_of_forall_coeff_dominantIntegral_eq_zero.
Main results #
TauCeti.casimirScalar_dotAction: the Casimir scalar is invariant under the dot action.TauCeti.casimirScalar_eq_zero_of_coeff_weylDenominator_ne_zero: the Casimir scalar vanishes on the support of the Weyl denominator.TauCeti.casimirScalar_eq_of_coeff_formalCharacter_mul_weylDenominator_ne_zero: the Casimir scalar is constant, equal toc(lam), on the support ofch M · Δ.TauCeti.coeff_formalCharacter_mul_weylDenominator_eq_zero_of_isDominantIntegral_of_ne:ch M · Δvanishes at every dominant integral weight other thanlam.TauCeti.formalCharacter_mul_weylDenominator_eq_weylNumerator: the Weyl character formulach M · Δ = N(lam), forMa finite-dimensional module generated by a highest weight vector.
References #
- V. G. Kac, Infinite dimensional Lie algebras, 3rd ed., Cambridge University Press (1990),
§10.4, where the character formula is derived from the equality
|λ + ρ|² = |Λ + ρ|²on the weightsλoccurring inch L(Λ) · Δ; there that equality comes from the Casimir operator on Verma modules, here it is derived from Freudenthal's formula. - J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §22.3 and §24.
The Casimir scalar and the dot action #
The Casimir scalar is invariant under the dot action: c(w ⬝ x) = c(x), since
w ⬝ x + ρ = w (x + ρ) and the invariant form is Weyl invariant.
The Casimir scalar vanishes on the support of the Weyl denominator.
The Weyl character formula #
The Casimir scalar is constant on the support of ch M · Δ: for a finite-dimensional
module generated by a highest weight vector of weight lam, every weight carrying a nonzero
coefficient of ch M · Δ has the Casimir scalar of lam.
ch M · Δ vanishes at every dominant integral weight other than the highest weight. A
dominant integral weight in the support lies below lam and has the Casimir scalar of lam, and
the Casimir scalar separates dominant integral weights along the root cone order.
The Weyl character formula #
The Weyl character formula. For a finite-dimensional module M generated by a highest
weight vector of weight lam, the formal character of M times the Weyl denominator is the Weyl
numerator of lam:
ch M · ∏_{α>0} (1 - e^{-α}) = ∑_{w ∈ W} sgn(w) e^{w(lam + ρ) - ρ}.
Both sides are alternating for the dot action and supported in lam - Q⁺, so
TauCeti.formalCharacter_mul_weylDenominator_eq_of_forall_coeff_isDominantIntegral_eq reduces the
identity to the coefficients at the dominant integral weights. There both sides are 1 at lam
and 0 elsewhere: on the left by the two coefficient computations above and
coeff_formalCharacter_mul_weylDenominator_eq_one_of_isHighestWeightVector_of_lieSpan_eq_top,
on the right because the dot orbit of a dominant integral weight is free and meets the dominant
integral weights only at lam.
Such an M is irreducible, by
TauCeti.isIrreducible_of_isHighestWeightVector_of_lieSpan_eq_top, so this is the character of
L(lam); it is stated for M itself so that no identification with L(lam) is needed to use
it.