The Weyl orbit and the Weyl numerator of a dominant integral weight #
A weight λ of a root pairing is dominant integral for a base b when every simple coroot
takes a natural value on it. This file proves, without any order on the coefficient ring, the
two facts about such a weight that the Weyl character formula needs about the Weyl numerator
N(λ) = ∑_{w ∈ W} sgn(w) e^{w ⬝ λ}: its dot orbit lies below λ in the positive root cone, and
it is free, so that N(λ) has coefficient 1 at λ and coefficient 0 at every other dominant
integral weight.
Both facts are already available over a linearly ordered ring, where the dominant weights form a
chamber: TauCeti.eq_one_of_smul_eq_self_of_mem_openDominantChamber is the freeness and
TauCeti.dotAction_eq_dotAction_iff_of_mem_dominantChamber its dot form. The Weyl character
formula, however, is an identity about a Lie module over an algebraically closed field, which
carries no linear order making it a strictly ordered ring, so the chamber statements do not apply
to it. As in TauCeti/LinearAlgebra/RootSystem/Weyl/IntegralDetermination.lean, the fundamental
domain is therefore described arithmetically: λ is dominant integral when ⟨λ, αᵢ^∨⟩ ∈ ℕ for
every simple root αᵢ.
The arguments #
Both go through the inversion set TauCeti.inversions of a Weyl-group element, whose cardinality
is its Coxeter length, rather than through chambers.
- Freeness. A weight
xwith⟨x, αᵢ^∨⟩ ∈ 1 + ℕat every simple root takes a value in1 + ℕat every positive coroot, because a positive coroot is a nonnegative integer combination of the simple ones with at least one nonzero coefficient. Ifw • x = xandw ≠ 1, thenwinverts some simple rootαᵢ(TauCeti.exists_mem_support_mem_inversions_of_ne_one), and⟨x, (w αᵢ)^∨⟩ = ⟨w x, (w αᵢ)^∨⟩ = ⟨x, αᵢ^∨⟩exhibits the same element ofRas a member of1 + ℕand as the negative of one, which characteristic zero forbids. - The orbit lies below. Induction on the number of inversions of
w. Ifw ≠ 1, pick a simple inversionαᵢand setv = w sᵢ, which has fewer inversions, so thatx - v xlies in the cone by induction. Thenx - w x = (x - v x) + ⟨x, αᵢ^∨⟩ · v αᵢ, andv αᵢis a positive root becausesᵢlengthensv.
The dot-action versions follow by applying these to the ρ-shift x = λ + ρ, which satisfies
⟨x, αᵢ^∨⟩ = ⟨λ, αᵢ^∨⟩ + 1 by TauCeti.coroot'_weylVector.
Main results #
TauCeti.eq_one_of_smul_eq_self_of_forall_coroot'_eq_natCast_add_one: the Weyl group acts freely on the strictly dominant integral weights, withTauCeti.dotAction_injective_of_dominantIntegralthe dot-action form at a dominant integral weight.TauCeti.sub_weylGroup_smul_mem_posRootCone_of_dominantIntegral: the Weyl orbit of a dominant integral weight lies below it in the positive root cone, withTauCeti.sub_dotAction_mem_posRootCone_of_dominantIntegralthe dot-action form.TauCeti.coeff_weylNumerator_self_of_dominantIntegral:N(λ)has coefficient1atλ, andTauCeti.coeff_weylNumerator_eq_zero_of_dominantIntegral_of_ne: coefficient0at every other dominant integral weight, withTauCeti.sub_mem_posRootCone_of_coeff_weylNumerator_ne_zeroplacing the whole support belowλ.
References #
These facts about the Weyl numerator match the corresponding facts about ch M · Δ and together
yield the Weyl character formula.
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §10.3 and §13.2 for the two arguments, and Ch. VI, §24 for their use.
Freeness on the strictly dominant integral weights #
Strict dominance extends from the simple coroots to all the positive ones. A weight taking
a value in 1 + ℕ on every simple coroot takes a value in 1 + ℕ on the coroot of every positive
root, because such a coroot is a nonnegative integer combination of the simple coroots
(TauCeti.exists_coroot'_eq_sum_nat_of_mem_posRoots) in which some coefficient is nonzero.
The Weyl group acts freely on the strictly dominant integral weights. If every simple
coroot takes a value in 1 + ℕ on x, then only the identity fixes x.
An element other than the identity inverts some simple root αᵢ
(TauCeti.exists_mem_support_mem_inversions_of_ne_one), and a weight fixed by it would take the
same value on αᵢ^∨ and on the coroot of the negative root w αᵢ; the first value lies in
1 + ℕ and the second is the negative of such a value, which is impossible in characteristic
zero.
The Weyl orbit of a dominant integral weight #
The Weyl orbit of a dominant integral weight lies below it in the positive root cone.
The induction is on the number of inversions of w: choosing a simple inversion αᵢ and writing
w = v sᵢ with v = w sᵢ shorter, the reflection formula gives
x - w x = (x - v x) + ⟨x, αᵢ^∨⟩ · v αᵢ, where v αᵢ is positive because sᵢ lengthens v
(TauCeti.lt_ncard_inversions_mul_ofIdx_iff).
The dot action #
The dot orbit of a dominant integral weight lies below it in the positive root cone: the
dot orbit of λ is the ρ-shift of the linear orbit of λ + ρ, which is dominant integral.
The dot action is free at a dominant integral weight: no two Weyl-group elements carry λ
to the same place, because the ρ-shift λ + ρ is strictly dominant integral.
The Weyl numerator #
The Weyl numerator of a dominant integral weight is supported in λ - Q⁺: it is supported
on the dot orbit of λ, which lies below λ.
The Weyl numerator of a dominant integral weight vanishes at every other dominant integral
weight. A weight of the dot orbit of λ lies below λ, and if it is itself dominant integral
then λ lies below it too, so the two agree because the positive root cone is pointed.
The Weyl numerator of a dominant integral weight has coefficient 1 there: the dot orbit
is free, so the term of the identity sits alone at λ.