The Kostant partition function

The Kostant partition function P(ν) counts the ways of writing an element ν of the ambient root module as a sum of positive roots with multiplicity. This file defines it for a base of an arbitrary root pairing, together with the finiteness statement that makes the count meaningful.

The multiplicities are recorded as a function c : ι → ℕ on root indices, supported on the positive roots, and TauCeti.IsKostantPartition P b ν c says that ∑ᵢ cᵢ αᵢ = ν. There are not necessarily finitely many functions ι → ℕ when the index type is finite, so finiteness must be proved before Nat.card represents the intended finite cardinality. The theorem TauCeti.finite_setOf_isKostantPartition supplies this proof.

The bound comes from a fact about heights proved in TauCeti/LinearAlgebra/RootSystem/Height.lean, since it has nothing to do with positivity: TauCeti.sum_mul_height_eq_zero_of_sum_zsmul_root_eq_zero says that height respects every integral relation among roots, so the total height ∑ᵢ cᵢ ht(αᵢ) depends only on ν and not on the partition. Fixing one partition of ν, its total height therefore bounds the total multiplicity, and hence each multiplicity, of every other partition of ν.

Main definitions

• TauCeti.IsKostantPartition: the predicate that a multiplicity function writes ν as a sum of positive roots.
• TauCeti.kostantPartition: the Kostant partition function, the number of such multiplicity functions.

Main results

• TauCeti.sum_natCast_mul_height_eq_of_isKostantPartition: two Kostant partitions of the same element have the same total height.
• TauCeti.finite_setOf_isKostantPartition: an element has only finitely many Kostant partitions.
• TauCeti.kostantPartition_zero: P(0) = 1, the empty partition being the only one.
• TauCeti.kostantPartition_root_of_mem_support: P(αᵢ) = 1 for a simple root αᵢ, which is the statement that a simple root is a sum of positive roots in only the obvious way.

Roadmap

This is the “Kostant partition function” item of Layer 3 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md, which asks for it “here in Layer 3 as a combinatorial object attached to the positive roots”, to be consumed by the weight multiplicities of a Verma module in that layer and by Kostant's multiplicity formula in Layer 6. The target signature in that roadmap's Suggested.lean is kostantPartition base nu for a base of the root system of a Killing-semisimple Lie algebra; nothing in the definition uses the Lie algebra, so it is stated here for a base of an arbitrary root pairing, alongside TauCeti.posRoots in TauCeti/LinearAlgebra/RootSystem/Positive.lean, and specializes to that signature.

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.

Kostant partitions

def TauCeti.IsKostantPartition {ι : 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 : ι → ℕ) : Prop

A Kostant partition of ν: a multiplicity function c on root indices, supported on the positive roots, whose weighted sum of positive roots is ν.

Equations

• TauCeti.IsKostantPartition P b ν c = (Function.support c ⊆ TauCeti.posRoots P b ∧ ∑ i ∈ TauCeti.posRootsFinset P b, c i • P.root i = ν)

theorem TauCeti.isKostantPartition_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 : ι → ℕ) : IsKostantPartition P b ν c ↔ Function.support c ⊆ posRoots P b ∧ ∑ i ∈ posRootsFinset P b, c i • P.root i = ν

A multiplicity function is a Kostant partition exactly when it is supported on the positive roots and its weighted root sum is the element being partitioned.

This is deliberately not a simp lemma: unfolding the predicate on sight would put every other statement about it — isKostantPartition_zero_iff first of all — out of simp normal form.

theorem TauCeti.sum_zsmul_root_of_isKostantPartition {ι : 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 : ι → ℕ} (hc : IsKostantPartition P b ν c) : ∑ i ∈ posRootsFinset P b, ↑(c i) • P.root i = ν

The defining sum of a Kostant partition, with the multiplicities read as integers.

theorem TauCeti.sum_natCast_mul_height_eq_of_isKostantPartition {ι : 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 c' : ι → ℕ} (hc : IsKostantPartition P b ν c) (hc' : IsKostantPartition P b ν c') : ∑ i ∈ posRootsFinset P b, ↑(c i) * b.height i = ∑ i ∈ posRootsFinset P b, ↑(c' i) * b.height i

The total height of a Kostant partition depends only on the element partitioned. This is what bounds the multiplicities, and hence what makes the partitions finite in number.

theorem TauCeti.finite_setOf_isKostantPartition {ι : 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 : ι → ℕ | IsKostantPartition P b ν c}.Finite

An element has only finitely many Kostant partitions.

instance TauCeti.instFiniteSubtypeIsKostantPartition {ι : 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) : Finite { c : ι → ℕ // IsKostantPartition P b ν c }

The Kostant partitions of an element form a finite type, so their Nat.card is their finite cardinality.

noncomputable def TauCeti.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) : ℕ

The Kostant partition function P(ν): the number of ways of writing ν as a sum of positive roots with multiplicity.

Equations

• TauCeti.kostantPartition P b ν = Nat.card { c : ι → ℕ // TauCeti.IsKostantPartition P b ν c }

theorem TauCeti.kostantPartition_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 ι] (ν : M) : kostantPartition P b ν = Nat.card { c : ι → ℕ // IsKostantPartition P b ν c }

The Kostant partition function counts the Kostant partitions of its argument.

@[simp]

theorem TauCeti.kostantPartition_pos_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) : 0 < kostantPartition P b ν ↔ ∃ (c : ι → ℕ), IsKostantPartition P b ν c

The Kostant partition function is positive exactly on the elements that are a sum of positive roots.

@[simp]

theorem TauCeti.kostantPartition_eq_zero_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) : kostantPartition P b ν = 0 ↔ ¬∃ (c : ι → ℕ), IsKostantPartition P b ν c

The Kostant partition function vanishes exactly off the set of sums of positive roots.

The two smallest values

@[simp]

theorem TauCeti.isKostantPartition_zero_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 ι] {c : ι → ℕ} : IsKostantPartition P b 0 c ↔ c = 0

The zero multiplicity function is the unique Kostant partition of zero.

@[simp]

theorem TauCeti.kostantPartition_zero {ι : 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 ι] : kostantPartition P b 0 = 1

P(0) = 1.

theorem TauCeti.isKostantPartition_single {ι : 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 ι] {i : ι} (hi : i ∈ posRoots P b) : IsKostantPartition P b (P.root i) (Pi.single i 1)

A positive root is a sum of positive roots, namely of itself.

theorem TauCeti.kostantPartition_root_pos {ι : 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 ι] {i : ι} (hi : i ∈ posRoots P b) : 0 < kostantPartition P b (P.root i)

The Kostant partition function is positive on every positive root.

theorem TauCeti.eq_single_of_isKostantPartition_root_of_mem_support {ι : 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 ι] {i : ι} (hi : i ∈ b.support) {c : ι → ℕ} (hc : IsKostantPartition P b (P.root i) c) : c = Pi.single i 1

Every Kostant partition of a simple root is its singleton partition.

@[simp]

theorem TauCeti.kostantPartition_root_of_mem_support {ι : 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 ι] {i : ι} (hi : i ∈ b.support) : kostantPartition P b (P.root i) = 1

P(αᵢ) = 1 for a simple root αᵢ.