Kostant's multiplicity 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. Kostant's multiplicity formula computes each weight multiplicity of M in closed form: with P the Kostant partition function of the positive roots and ρ the half-sum of the positive roots,

dim M_μ = ∑_{w ∈ W} sgn(w) P(w(lam + ρ) - (μ + ρ)).

It is the weight-by-weight refinement of the Weyl character formula TauCeti.formalCharacter_mul_weylDenominator_eq_weylNumerator, which records the same information as a single identity ch M · Δ = N(lam) in the group algebra ℤ[Module.Dual K H]. Passing from one to the other is division by the Weyl denominator Δ, and that division is performed at the level of an abstract root pairing in TauCeti/LinearAlgebra/RootSystem/KostantPartition/Multiplicity.lean: pairing an element of the group algebra against the formal series ∑_ν P(ν) e^{-ν} inverse to Δ recovers a single coefficient. This file only feeds the character formula into that division, so all of the content here is the identification of the two sides, not the combinatorics.

The right-hand side is RootPairing.kostantMultiplicity, whose shifted differences w ⬝ lam - μ are the differences w(lam + ρ) - (μ + ρ) of the classical statement, the dot action of the Weyl group being w ⬝ x = w(x + ρ) - ρ.

Main results

• TauCeti.formalCharacter_coeff_eq_kostantMultiplicity: the coefficients of the formal character of a highest weight module are the Kostant multiplicities.
• TauCeti.finrank_weightSpace_eq_kostantMultiplicity: Kostant's multiplicity formula, the same statement read as the dimension of a weight space.

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.

theorem TauCeti.formalCharacter_coeff_eq_kostantMultiplicity {K : Type u} {L : Type v} [Field K] [CharZero K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [Fintype ↥(LieAlgebra.IsKilling.rootSystem H).weylGroup] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} {v : M} (hv : IsHighestWeightVector b lam v) (hgen : LieSubmodule.lieSpan K L {v} = ⊤) (mu : Module.Dual K ↥H) : (formalCharacter K (↥H) M).coeff mu = (LieAlgebra.IsKilling.rootSystem H).kostantMultiplicity b lam mu

Kostant's multiplicity formula, read off the formal character: for a finite-dimensional module generated by a highest weight vector of weight lam, the coefficient of ch M at mu is ∑_{w ∈ W} sgn(w) P(w ⬝ lam - mu).

It is the Weyl character formula ch M · Δ = N(lam) read one coefficient at a time.

theorem TauCeti.finrank_weightSpace_eq_kostantMultiplicity {K : Type u} {L : Type v} [Field K] [CharZero K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [Fintype ↥(LieAlgebra.IsKilling.rootSystem H).weylGroup] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} {v : M} (hv : IsHighestWeightVector b lam v) (hgen : LieSubmodule.lieSpan K L {v} = ⊤) (mu : Module.Dual K ↥H) : ↑(Module.finrank K ↥(LieModule.weightSpace M ⇑mu)) = (LieAlgebra.IsKilling.rootSystem H).kostantMultiplicity b lam mu

Kostant's multiplicity formula. The multiplicity of the weight mu in a finite-dimensional module generated by a highest weight vector of weight lam is the alternating sum ∑_{w ∈ W} sgn(w) P(w(lam + ρ) - (mu + ρ)) of values of the Kostant partition function.