Dividing by the Weyl denominator: the Kostant multiplicity

The Weyl character formula is the identity ch · Δ = N(λ) in the integral group algebra ℤ[M] of the weight space, between the formal character of a highest weight module, the Weyl denominator Δ = ∏_{α>0}(1 - e^{-α}) (TauCeti.weylDenominator) and the Weyl numerator N(λ) = ∑_{w ∈ W} sgn(w) e^{w ⬝ λ} (TauCeti.weylNumerator). Dividing by Δ recovers the individual coefficients of ch, that is, the individual weight multiplicities; this file performs that division at the level of the group algebra, where the divisor is not invertible and the quotient is expressed through the Kostant partition function.

The inverse of Δ is the formal series ∑_ν P(ν) e^{-ν}, whose coefficients are the Kostant partition function TauCeti.kostantPartition. The series is not an element of ℤ[M], so instead of a product we pair an element of ℤ[M] against it and read off the coefficient at μ: the pairing g ↦ ∑_ν g_ν P(ν - μ) is a finite sum, and RootPairing.sum_coeff_mul_weylDenominator_mul_kostantPartition says that applying it to f · Δ returns f_μ. That is division by Δ, coefficient by coefficient.

Applying the pairing to N(λ) instead gives the Kostant multiplicity RootPairing.kostantMultiplicity, the alternating sum ∑_{w ∈ W} sgn(w) P(w ⬝ λ - μ). So the two computations together turn the character formula into a closed formula for a single multiplicity: RootPairing.coeff_eq_kostantMultiplicity_of_mul_weylDenominator_eq_weylNumerator.

Everything here is combinatorics of the root pairing; no Lie algebra appears, and the Lie-theoretic reading of these statements — that the multiplicity of the weight μ in a finite-dimensional highest weight module of highest weight λ is ∑_{w ∈ W} sgn(w) P(w(λ+ρ) - (μ+ρ)) — is obtained by feeding in the character formula.

Main definitions

• RootPairing.kostantMultiplicity: the alternating sum ∑_{w ∈ W} sgn(w) P(w ⬝ λ - μ).

Main results

• RootPairing.sum_coeff_mul_weylDenominator_mul_kostantPartition: division by Δ, the pairing of f · Δ against the partition series at μ is the coefficient f_μ. It rests on the inversion identity TauCeti.sum_powerset_neg_one_pow_mul_kostantPartition, transcribed into the group algebra as the statement that pairing Δ itself against the series gives 1 at 0 and 0 elsewhere.
• RootPairing.sum_coeff_weylNumerator_mul_kostantPartition: the pairing of N(λ) against the partition series at μ is RootPairing.kostantMultiplicity.
• RootPairing.coeff_eq_kostantMultiplicity_of_mul_weylDenominator_eq_weylNumerator: Kostant's multiplicity formula, in the form it takes before a module is named: an element of ℤ[M] whose product with Δ is N(λ) has μ-th coefficient ∑_{w ∈ W} sgn(w) P(w ⬝ λ - μ).

References

• B. Kostant, A formula for the multiplicity of a weight, Trans. Amer. Math. Soc. 93 (1959).
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §24.2.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapter VIII, §9.

Pairing against the inverse of the Weyl denominator

theorem RootPairing.sum_coeff_mul_weylDenominator_mul_kostantPartition {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CharZero R] (P : RootPairing ι R M N) [Finite ι] (b : P.Base) (f : AddMonoidAlgebra ℤ M) (mu : M) : ((f * TauCeti.weylDenominator P b).coeff.sum fun (x : M) (c : ℤ) => c * ↑(TauCeti.kostantPartition P b (x - mu))) = f.coeff mu

Division by the Weyl denominator. Pairing f · Δ against the series ∑_ν P(ν) e^{-ν} at μ returns the coefficient of f at μ.

This is the sense in which ∑_ν P(ν) e^{-ν} is the inverse of Δ: the series is not an element of ℤ[M], but pairing against it undoes multiplication by Δ coefficient by coefficient.

The Kostant multiplicity

noncomputable def RootPairing.kostantMultiplicity {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CharZero R] (P : RootPairing ι R M N) [Finite ι] (b : P.Base) [IsDomain R] [Invertible 2] [P.IsCrystallographic] [P.IsReduced] [Fintype ↥P.weylGroup] (lam mu : M) : ℤ

The Kostant multiplicity ∑_{w ∈ W} sgn(w) P(w ⬝ λ - μ) of a pair of weights, an alternating sum of values of the Kostant partition function over the Weyl group. The dot action w ⬝ λ = w(λ + ρ) - ρ makes w ⬝ λ - μ = w(λ + ρ) - (μ + ρ), the shifted difference of Kostant's formula.

It is the multiplicity of the weight μ in the finite-dimensional highest weight module of highest weight λ, as soon as the Weyl character formula is available for that module.

Equations

• P.kostantMultiplicity b lam mu = ∑ w : ↥P.weylGroup, ↑((TauCeti.weylSign P b) w) * ↑(TauCeti.kostantPartition P b (TauCeti.dotAction P b w lam - mu))

theorem RootPairing.kostantMultiplicity_def {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CharZero R] (P : RootPairing ι R M N) [Finite ι] (b : P.Base) [IsDomain R] [Invertible 2] [P.IsCrystallographic] [P.IsReduced] [Fintype ↥P.weylGroup] (lam mu : M) : P.kostantMultiplicity b lam mu = ∑ w : ↥P.weylGroup, ↑((TauCeti.weylSign P b) w) * ↑(TauCeti.kostantPartition P b (TauCeti.dotAction P b w lam - mu))

The Kostant multiplicity is the alternating sum over the Weyl group, by definition.

theorem RootPairing.sum_coeff_weylNumerator_mul_kostantPartition {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CharZero R] (P : RootPairing ι R M N) [Finite ι] (b : P.Base) [IsDomain R] [Invertible 2] [P.IsCrystallographic] [P.IsReduced] [Fintype ↥P.weylGroup] (lam mu : M) : ((TauCeti.weylNumerator P b lam).coeff.sum fun (x : M) (c : ℤ) => c * ↑(TauCeti.kostantPartition P b (x - mu))) = P.kostantMultiplicity b lam mu

The Weyl numerator pairs to the Kostant multiplicity. Each term sgn(w) e^{w ⬝ λ} of N(λ) contributes sgn(w) P(w ⬝ λ - μ).

theorem RootPairing.coeff_eq_kostantMultiplicity_of_mul_weylDenominator_eq_weylNumerator {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CharZero R] (P : RootPairing ι R M N) [Finite ι] (b : P.Base) [IsDomain R] [Invertible 2] [P.IsCrystallographic] [P.IsReduced] [Fintype ↥P.weylGroup] {f : AddMonoidAlgebra ℤ M} {lam : M} (hf : f * TauCeti.weylDenominator P b = TauCeti.weylNumerator P b lam) (mu : M) : f.coeff mu = P.kostantMultiplicity b lam mu

Kostant's multiplicity formula, stated before any module is named: an element of ℤ[M] whose product with the Weyl denominator is the Weyl numerator of λ has μ-th coefficient ∑_{w ∈ W} sgn(w) P(w ⬝ λ - μ).

The hypothesis is exactly the Weyl character formula, so this turns that formula into a closed expression for one weight multiplicity at a time.