The Weyl denominator

The Weyl denominator of a base of a root pairing is the element Δ = ∏_{α > 0} (1 - e^{-α}) of the integral group algebra ℤ[M] of the weight space. It is one of the two universal elements that the Weyl character formula compares, the other being the Weyl numerator TauCeti.weylNumerator; the formula is the identity ch L(λ) · Δ = N(λ) in ℤ[M].

This normalization is the one all of whose exponents lie in the weight lattice M. The symmetric form ∏_{α>0} (e^{α/2} - e^{-α/2}) is e^{ρ} times this one and needs the half-roots α/2, which need not belong to M — nothing in the hypotheses below makes a root divisible by two.

Only the positive roots of the base enter, so the denominator asks for far less than the numerator does: neither the crystallographic nor the reduced hypothesis, nor an invertible 2, only what TauCeti.posRootsFinset needs. That is why it lives in this file rather than beside the numerator, whose Weyl-group combinatorics is a much later dependency.

Main definitions

• TauCeti.weylDenominator: Δ = ∏_{α > 0} (1 - e^{-α}), an element of ℤ[M].

Main results

• TauCeti.weylDenominator_eq_sum_powerset: expanding the product, Δ is the signed sum ∑_{T ⊆ Φ⁺} (-1)^{|T|} e^{-∑_{α ∈ T} α} over the subsets of the positive roots; hence
• TauCeti.coeff_weylDenominator_eq_zero: Δ is supported on the negatives of the sums of sets of positive roots, which is the statement that it lives in the negative cone, and TauCeti.neg_mem_posRootCone_of_coeff_weylDenominator_ne_zero, that statement read against TauCeti.posRootCone; and
• TauCeti.coeff_weylDenominator_zero: the constant term of Δ is 1, the empty set being the only set of positive roots summing to 0.

References

This builds the weylDenominator target of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md, Layer 6 ("the character, dimension, and Kostant formulas"), whose Suggested.lean pins it on Module.Dual K H for the root system of a Cartan subalgebra. As with TauCeti.weylVector, the combinatorics lives at the level of an abstract root pairing, so the Lie-algebra target is a specialization rather than a rebuild.

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, Ch. VI, §24.
• J.-P. Serre, Complex Semisimple Lie Algebras, Ch. VII.

noncomputable def TauCeti.weylDenominator {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] (b : P.Base) : AddMonoidAlgebra ℤ M

The Weyl denominator Δ = ∏_{α > 0} (1 - e^{-α}) of a base, an element of the integral group algebra of the weight space.

This is the normalization all of whose exponents lie in the weight lattice; the symmetric form ∏_{α>0} (e^{α/2} - e^{-α/2}) is e^{ρ} times this one and needs the half-roots α/2, which need not lie in M.

Equations

• TauCeti.weylDenominator P b = ∏ i ∈ TauCeti.posRootsFinset P b, (1 - AddMonoidAlgebra.single (-P.root i) 1)

theorem TauCeti.weylDenominator_def {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] (b : P.Base) : weylDenominator P b = ∏ i ∈ posRootsFinset P b, (1 - AddMonoidAlgebra.single (-P.root i) 1)

Δ is the product of 1 - e^{-α} over the positive roots, by definition.

theorem TauCeti.weylDenominator_eq_sum_powerset {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] (b : P.Base) : weylDenominator P b = ∑ T ∈ (posRootsFinset P b).powerset, AddMonoidAlgebra.single (-∑ i ∈ T, P.root i) ((-1) ^ T.card)

The Weyl denominator, expanded. Multiplying out ∏_{α>0} (1 - e^{-α}) indexes the terms by the subsets T of the positive roots, the term of T being (-1)^{|T|} e^{-∑_{α ∈ T} α}.

Every exponent occurring is therefore minus a sum of positive roots, which is the statement that Δ lives in the negative cone; TauCeti.coeff_weylDenominator_eq_zero reads that off.

theorem TauCeti.coeff_weylDenominator_eq_zero {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] (b : P.Base) {x : M} (hx : ∀ T ⊆ posRootsFinset P b, x ≠ -∑ i ∈ T, P.root i) : (weylDenominator P b).coeff x = 0

The Weyl denominator is supported on the negative cone: a coefficient of Δ at a weight that is not minus the sum of a set of positive roots vanishes.

@[simp]

theorem TauCeti.coeff_weylDenominator_zero {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] (b : P.Base) : (weylDenominator P b).coeff 0 = 1

The constant term of the Weyl denominator is 1. Expanding ∏_{α>0}(1 - e^{-α}) indexes the terms by the sets of positive roots, and the empty set is the only one whose sum vanishes.

theorem TauCeti.neg_mem_posRootCone_of_coeff_weylDenominator_ne_zero {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] (b : P.Base) {x : M} (hx : (weylDenominator P b).coeff x ≠ 0) : -x ∈ posRootCone P b

The Weyl denominator is supported on the negative of the positive root cone: a weight carrying a nonzero coefficient of Δ is minus a nonnegative integer combination of the simple roots. This is TauCeti.coeff_weylDenominator_eq_zero read against TauCeti.posRootCone, in the form the weight-cone arguments of the highest weight theory consume.