The Weyl denominator identity #
The Weyl denominator identity is the equality
∏_{α > 0} (1 - e^{-α}) = ∑_{w ∈ W} sgn(w) e^{w ⬝ 0}
in the integral group algebra ℤ[M] of the weight space of a root system: the Weyl denominator
TauCeti.weylDenominator is the Weyl numerator TauCeti.weylNumerator of the weight 0. Written
without the dot action w ⬝ 0 = w(ρ) - ρ it is the familiar
∏_{α>0}(1 - e^{-α}) = ∑_w sgn(w) e^{w(ρ) - ρ}, or, after multiplying by e^{ρ}, the symmetric
form ∏_{α>0}(e^{α/2} - e^{-α/2}) = ∑_w sgn(w) e^{w(ρ)}.
It is the case λ = 0 of the Weyl character formula, which identifies the product of a formal
character with the denominator with the numerator of a dominant weight. Thus the identity is proved
first and on its own, with no representation theory involved.
The argument #
Δ is alternating for the dot action (TauCeti.isDotAlternating_weylDenominator), so
TauCeti.IsDotAlternating.eq_weylNumerator reduces the identity to two coefficient computations on
the open chamber of the dot action: the constant term of Δ is 1
(TauCeti.coeff_weylDenominator_zero, an elementary expansion proved with the denominator itself),
and 0 is the only weight of that chamber where Δ does not vanish.
The second computation is the geometric heart of the identity, and is the only step specific to the
denominator. An exponent of Δ is -ν for a sum ν of positive roots; lying in the open dot
chamber makes ρ - ν strictly dominant, which bounds every ⟨ν, αᵢ^∨⟩ above by 1; these
pairings are integers, hence nonpositive; and the only antidominant member of the positive root
cone is 0 (TauCeti.eq_zero_of_mem_posRootCone_of_forall_coroot'_nonpos).
The coefficient ring #
Everything below is stated over a linearly ordered coefficient ring, which is where the chamber
geometry the proof runs through lives: TauCeti.openDotDominantChamber is defined through
RootPairing.openDominantChamber, whose orbit-existence theorem asks for [LinearOrder R], and
TauCeti.IsDotAlternating.eq_weylNumerator is stated over an ordered ring. The identity therefore
specializes directly to an ordered root pairing — a rational or a real one — but not, without a
base change, to one over an unordered field such as ℂ. Carrying it there is a scalar-restriction
question about RootPairing.restrictScalars', which produces a pairing on the span of the roots
rather than on the ambient weight module, and is not attempted here.
Main results #
TauCeti.weylDenominator_eq_weylNumerator_zero: the Weyl denominator identity,Δ = N(0).TauCeti.support_coeff_weylDenominatorandTauCeti.card_support_coeff_weylDenominator: consequentlyΔis supported on the dot orbit of0and has exactly|W|terms.
References #
This is the "Weyl denominator identity, proved combinatorially" step of Layer 6 ("the Weyl
character, dimension, and Kostant formulas") of
TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md.
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, Ch. VI, §24.3.
- J.-P. Serre, Complex Semisimple Lie Algebras, Ch. VII, §7.
The Weyl denominator identity: the Weyl denominator is the Weyl numerator of the weight
0,
∏_{α > 0} (1 - e^{-α}) = ∑_{w ∈ W} sgn(w) e^{w ⬝ 0},
an identity in the integral group algebra of the weight space. Written without the dot action, the
right-hand side is ∑_{w ∈ W} sgn(w) e^{w(ρ) - ρ}.
This is the case λ = 0 of the Weyl character formula, in which the character of the trivial
module is 1.
The Weyl denominator is supported exactly on the dot orbit of 0, one term for each
element of the Weyl group.
The Weyl denominator has exactly |W| terms. Expanding the product over the positive roots
gives 2^{|Φ⁺|} terms, which collapse to one for each element of the Weyl group.