The Weyl numerator #
The Weyl character formula is an identity in the integral group algebra ℤ[M] of the weight space
of a root pairing, between the formal character of an irreducible module and two universal
elements of that algebra: the Weyl numerator N(λ) and the Weyl denominator Δ. As soon as there
is a positive root, Δ is not invertible in ℤ[M] — it then augments to 0, whereas a unit
augments to ±1 — so the formula is read there in the cross-multiplied form
ch L(λ) · Δ = N(λ), the familiar quotient N(λ) / Δ living in a localization where Δ becomes
invertible. This file builds the Weyl numerator
N(λ) = ∑_{w ∈ W} sgn(w) e^{w ⬝ λ}, the alternating sum over the dot orbit of λ, and its
combinatorics, with no Lie algebra in sight. The denominator Δ = ∏_{α > 0} (1 - e^{-α}) is
TauCeti.weylDenominator, which needs far less and lives in its own earlier file.
Writing the numerator through the dot action w ⬝ λ = w(λ + ρ) - ρ (TauCeti.dotAction) rather
than as ∑ sgn(w) e^{w(λ+ρ)} is what keeps every exponent inside the weight lattice, matching the
normalization ∏_{α>0}(1 - e^{-α}) of the denominator rather than the symmetric one
∏_{α>0}(e^{α/2} - e^{-α/2}), which needs half-roots. The two normalizations differ by the factor
e^{ρ}.
The signs come from TauCeti.weylSign, the character w ↦ (-1)^{ℓ(w)} of the Weyl group; they
are what makes the numerator alternating, which is the content of
TauCeti.weylNumerator_dotAction and of everything derived from it.
Main definitions #
TauCeti.weylNumerator:N(λ) = ∑_{w ∈ W} sgn(w) e^{w ⬝ λ}, an element ofℤ[M].
Main results #
TauCeti.weylNumerator_dotAction: the numerator is alternating,N(v ⬝ λ) = sgn(v) · N(λ);TauCeti.coeff_weylNumerator_dotActionis the corresponding coefficient transformation rule.TauCeti.weylNumerator_eq_zero_of_dotAction_eq_self: a weight fixed by an odd element of the Weyl group has vanishing numerator, andTauCeti.weylNumerator_eq_zero_of_coroot'_eq_neg_one: so does a weight on a wall⟨λ, αᵢ^∨⟩ = -1of a simple reflection for the dot action, which is the case the highest-weight theory meets.TauCeti.coeff_weylNumerator_dotAction_of_injective,TauCeti.support_coeff_weylNumerator_of_injective,TauCeti.card_support_coeff_weylNumerator_of_injectiveandTauCeti.weylNumerator_ne_zero_of_injective: when the dot orbit mapw ↦ w ⬝ λis injective the|W|terms sit at|W|distinct weights, so the coefficient atw ⬝ λissgn(w), the support is exactly the dot orbit and has|W|elements, and the numerator does not vanish. A dominant weight has an injective dot orbit map byTauCeti.dotAction_eq_dotAction_iff_of_mem_dominantChamber, whenceTauCeti.support_coeff_weylNumerator,TauCeti.card_support_coeff_weylNumeratorandTauCeti.weylNumerator_ne_zero_of_mem_dominantChamber.
Implementation notes #
TauCeti.weylNumerator sums over Finset.univ and so carries [Fintype P.weylGroup] rather than
[Finite P.weylGroup]. The Weyl group of a finite root system is finite
(RootPairing.finite_weylGroup), and a consumer holding only that instance
supplies the Fintype with Fintype.ofFinite; the value of the sum does not depend on which one,
since Fintype is a subsingleton.
The freeness statements are proved from the injectivity of the dot orbit map, which is all they
use; dominance enters only through the corollaries of the last section, which is also the only
place the ordered hypotheses appear. Those hypotheses already supply IsDomain R through
IsStrictOrderedRing.isDomain, so it is not repeated there.
References #
This builds the weylNumerator 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 and TauCeti.dotAction, 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.
The Weyl numerator N(λ) = ∑_{w ∈ W} sgn(w) e^{w ⬝ λ} of a weight, the alternating sum
over the dot orbit of λ.
The dot action w ⬝ λ = w(λ + ρ) - ρ (TauCeti.dotAction) is the ρ-shifted form: the
un-shifted numerator ∑_w sgn(w) e^{w(λ+ρ)} is e^{ρ} times this one, and matches the symmetric
normalization of the denominator rather than TauCeti.weylDenominator.
Equations
- TauCeti.weylNumerator P b lam = ∑ w : ↥P.weylGroup, AddMonoidAlgebra.single (TauCeti.dotAction P b w lam) ↑((TauCeti.weylSign P b) w)
Instances For
N(λ) is the signed sum ∑_{w ∈ W} sgn(w) e^{w ⬝ λ} over the dot orbit, by definition.
The numerator is supported on the dot orbit: its coefficient at a weight outside the orbit
of λ vanishes, since no term of the sum sits there.
The Weyl numerator is alternating: replacing λ by its dot translate v ⬝ λ multiplies
the numerator by sgn(v).
This is the reindexing w ↦ w * v of the defining sum, and it is the source of every vanishing
statement below: a weight fixed by an odd element of the Weyl group is one where the sum cancels
against itself.
The coefficients of the Weyl numerator transform by the sign character under the dot
action: [e^{w ⬝ x}] N(λ) = sgn(w) [e^x] N(λ).
A weight fixed by an odd Weyl-group element has vanishing numerator. The alternating
identity turns such a fixed point into N(λ) = -N(λ), and ℤ[M] is torsion-free.
A weight on a wall of the dot action has vanishing numerator. The wall of the simple
reflection sᵢ for the dot action is ⟨λ, αᵢ^∨⟩ = -1 (TauCeti.dotAction_ofIdx_eq_self_iff), and
a simple reflection is odd. This is the case the highest-weight theory meets.
Weights with a free dot orbit #
Nothing below asks for more than the injectivity of the dot orbit map w ↦ w ⬝ λ: it makes the
|W| terms of the numerator sit at |W| distinct weights, so none of them cancels. A dominant
weight is the case of interest, and is treated in the last section.
The coefficients of the numerator along a free dot orbit are the signs. No two Weyl-group
elements carry λ to the same place, so the term of w sits alone at w ⬝ λ.
A numerator with a free dot orbit is supported exactly on that orbit.
A numerator with a free dot orbit has exactly |W| terms, one for each element of the
Weyl group.
A numerator with a free dot orbit does not vanish: its coefficient at λ itself is 1.
Dominant weights #
For a dominant weight the dot action is free
(TauCeti.eq_one_of_dotAction_eq_self_of_mem_dominantChamber), so the results of the previous
section apply verbatim. The linearly ordered hypotheses of this section already supply
IsDomain R through IsStrictOrderedRing.isDomain, so it is not repeated.
The numerator of a weight of the open dot chamber has coefficient 1 there.
The numerator of a dominant weight is supported exactly on its dot orbit.
The numerator of a dominant weight has exactly |W| terms, one for each element of the
Weyl group.
The numerator of a dominant weight does not vanish: its coefficient at λ itself is 1.
With TauCeti.weylNumerator_eq_zero_of_coroot'_eq_neg_one this says the numerator vanishes on the
walls of the simple reflections for the dot action, and on no dominant weight.