The Kostant partition function inverts the Weyl denominator

The Weyl denominator Δ = ∏_{α > 0} (1 - e^{-α}) of TauCeti.weylDenominator expands, by TauCeti.weylDenominator_eq_sum_powerset, as the signed sum ∑_{T ⊆ Φ⁺} (-1)^{|T|} e^{-∑_{α ∈ T} α} over the subsets of the positive roots. Formally inverting each factor, (1 - e^{-α})⁻¹ = ∑_{k ≥ 0} e^{-kα}, gives the series ∑_ν P(ν) e^{-ν} whose coefficients are the Kostant partition function TauCeti.kostantPartition. This file proves that the two are indeed inverse, in the only form in which the statement makes sense inside the honest group algebra ℤ[M]: coefficient by coefficient,

∑_{T ⊆ Φ⁺} (-1)^{|T|} P(ν - ∑_{α ∈ T} α) = δ_{ν, 0}.

Both sides are finite. The series ∑_ν P(ν) e^{-ν} itself is not an element of ℤ[M] as soon as there is a positive root, so no statement of the form Δ * K = 1 is available without a completion; the identity above is what such a statement would say about the coefficient at -ν, and it is what the applications use. Read with ν = λ - x, it says that the character of a module whose weight multiplicities are the values P(λ - x), which is what a Verma module M(λ) has, satisfies ch M(λ) · Δ = e^λ; read directly, it is the expansion of the inverse denominator against which the Weyl character formula is developed into Kostant's multiplicity formula.

The argument

The proof is an induction over the set of positive roots that are allowed to occur, which forces a relative version of the partition function: TauCeti.kostantPartitionOn P b S ν counts the Kostant partitions of ν whose multiplicities are supported in a subset S of the positive roots, so that S = Φ⁺ recovers TauCeti.kostantPartition and S = ∅ leaves only the empty partition of 0.

The step is the recursion TauCeti.kostantPartitionOn_eq_erase_add_sub_root: for i ∈ S, a partition supported in S either does not use αᵢ, and is a partition supported in S with i erased, or uses it, and then raising the multiplicity of αᵢ by one matches the partitions that use it bijectively with the partitions of ν - αᵢ supported in S. Splitting the sum over subsets of insert i S into those subsets containing i and those not turns the alternating sum into a sum of differences P_S(ν - σ) - P_S(ν - σ - αᵢ), which the recursion identifies with the values of the partition function of S with i erased, and the induction hypothesis applies.

Main definitions

• TauCeti.IsKostantPartitionOn and TauCeti.kostantPartitionOn: the Kostant partitions whose multiplicities are supported in a prescribed set of positive roots, and their number.

Main results

• TauCeti.kostantPartitionOn_eq_erase_add_sub_root: the recursion in the set of allowed roots.
• TauCeti.sum_powerset_neg_one_pow_mul_kostantPartitionOn and TauCeti.sum_powerset_neg_one_pow_mul_kostantPartition: the inversion identity, the second being the case S = Φ⁺ that inverts the Weyl denominator.

Roadmap

The Kostant partition function is asked for in Layer 3 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md, to be consumed by the Verma weight multiplicities of that layer and by Kostant's multiplicity formula in Layer 6, whose stated proof is "by expanding the character formula against the geometric-series expansion of the inverse denominator (whose coefficients are P)". This file is that expansion. As with TauCeti.weylDenominator and TauCeti.kostantPartition, nothing here uses the Lie algebra, so it is stated for a base of an arbitrary root pairing.

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.

Kostant partitions supported in a set of positive roots

def TauCeti.IsKostantPartitionOn {ι : 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) (b : P.Base) [Finite ι] (S : Finset ι) (ν : M) (c : ι → ℕ) : Prop

A Kostant partition of ν supported in S: a Kostant partition of ν all of whose multiplicities are carried by the root indices in S.

Equations

• TauCeti.IsKostantPartitionOn P b S ν c = (TauCeti.IsKostantPartition P b ν c ∧ Function.support c ⊆ ↑S)

theorem TauCeti.isKostantPartitionOn_iff {ι : 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) (b : P.Base) [Finite ι] (S : Finset ι) (ν : M) (c : ι → ℕ) : IsKostantPartitionOn P b S ν c ↔ IsKostantPartition P b ν c ∧ Function.support c ⊆ ↑S

A multiplicity function is a Kostant partition supported in S exactly when it is a Kostant partition and is supported in S.

instance TauCeti.instFiniteSubtypeIsKostantPartitionOn {ι : 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) (b : P.Base) [Finite ι] (S : Finset ι) (ν : M) : Finite { c : ι → ℕ // IsKostantPartitionOn P b S ν c }

The Kostant partitions supported in a set form a finite type, so their Nat.card is their finite cardinality.

noncomputable def TauCeti.kostantPartitionOn {ι : 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) (b : P.Base) [Finite ι] (S : Finset ι) (ν : M) : ℕ

The Kostant partition function of a set of positive roots P_S(ν): the number of ways of writing ν as a sum, with multiplicity, of the positive roots indexed by S.

Equations

• TauCeti.kostantPartitionOn P b S ν = Nat.card { c : ι → ℕ // TauCeti.IsKostantPartitionOn P b S ν c }

theorem TauCeti.kostantPartitionOn_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) (b : P.Base) [Finite ι] (S : Finset ι) (ν : M) : kostantPartitionOn P b S ν = Nat.card { c : ι → ℕ // IsKostantPartitionOn P b S ν c }

The relative Kostant partition function counts the Kostant partitions supported in its set.

@[simp]

theorem TauCeti.isKostantPartitionOn_posRootsFinset_iff {ι : 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) (b : P.Base) [Finite ι] {ν : M} {c : ι → ℕ} : IsKostantPartitionOn P b (posRootsFinset P b) ν c ↔ IsKostantPartition P b ν c

Being supported in the whole set of positive roots is no condition at all.

@[simp]

theorem TauCeti.kostantPartitionOn_posRootsFinset {ι : 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) (b : P.Base) [Finite ι] (ν : M) : kostantPartitionOn P b (posRootsFinset P b) ν = kostantPartition P b ν

The relative Kostant partition function of the full set of positive roots is the Kostant partition function.

@[simp]

theorem TauCeti.isKostantPartitionOn_empty_iff {ι : 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) (b : P.Base) [Finite ι] {ν : M} {c : ι → ℕ} : IsKostantPartitionOn P b ∅ ν c ↔ c = 0 ∧ ν = 0

The only Kostant partition using no positive root at all is the empty partition of 0.

@[simp]

theorem TauCeti.kostantPartitionOn_empty {ι : 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) (b : P.Base) [Finite ι] (ν : M) : kostantPartitionOn P b ∅ ν = if ν = 0 then 1 else 0

P_∅(ν) is 1 at 0 and 0 elsewhere: the base case of the inversion identity.

The recursion in the set of allowed roots

theorem TauCeti.kostantPartitionOn_eq_erase_add_sub_root {ι : 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} {b : P.Base} [Finite ι] [DecidableEq ι] {S : Finset ι} {i : ι} (hiS : i ∈ S) (hi : i ∈ posRootsFinset P b) (ν : M) : kostantPartitionOn P b S ν = kostantPartitionOn P b (S.erase i) ν + kostantPartitionOn P b S (ν - P.root i)

The recursion for the Kostant partition function in the set of allowed roots. A partition supported in S either avoids the positive root αᵢ, and so is supported in S with i erased, or uses it, and then lowering the multiplicity of αᵢ by one is a bijection onto the partitions of ν - αᵢ supported in S.

The inversion identity

theorem TauCeti.sum_powerset_neg_one_pow_mul_kostantPartitionOn {ι : 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) (b : P.Base) [Finite ι] {S : Finset ι} (hS : S ⊆ posRootsFinset P b) (ν : M) : ∑ T ∈ S.powerset, (-1) ^ T.card * ↑(kostantPartitionOn P b S (ν - ∑ i ∈ T, P.root i)) = if ν = 0 then 1 else 0

The Kostant partition function of a set of positive roots inverts the corresponding denominator. The alternating sum, over the subsets T of S, of the number of partitions of ν - ∑_{α ∈ T} α supported in S is 1 at ν = 0 and 0 elsewhere.

theorem TauCeti.sum_powerset_neg_one_pow_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) (b : P.Base) [Finite ι] (ν : M) : ∑ T ∈ (posRootsFinset P b).powerset, (-1) ^ T.card * ↑(kostantPartition P b (ν - ∑ i ∈ T, P.root i)) = if ν = 0 then 1 else 0

The Kostant partition function inverts the Weyl denominator. Since Δ = ∑_{T ⊆ Φ⁺} (-1)^{|T|} e^{-∑_{α ∈ T} α} by TauCeti.weylDenominator_eq_sum_powerset, this is the statement that the coefficient at e^{-ν} of the product of Δ with the formal series ∑_ν P(ν) e^{-ν} is 1 at ν = 0 and 0 elsewhere.