The Weyl vector of a base #

The Weyl vector ρ of a base of a root pairing is the half-sum of the positive roots. It is the shift that turns the Weyl group action on weights into the dot action, and it appears in the Weyl character, dimension and Kostant formulas as the correction λ ↦ λ + ρ.

Which roots are positive is defined only over a coefficient ring of characteristic zero, and halving asks for 2 to be invertible on top of that. So the sum of the positive roots is introduced first, as Ado.twoWeylVector, over a characteristic-zero coefficient ring, and the Weyl vector itself only once 2 is invertible as well. The simple-coroot pairing and the simple reflection identity are proved for the sum first and then divided by two; the statements that speak of ρ alone — the dot action and the dominance results — are proved only in the halved form. So nothing below assumes more of the coefficient ring than its own statement needs.

The one theorem the notion exists for is that ρ pairs to 1 with every simple coroot, equivalently that the simple reflection sᵢ sends ρ to ρ - αᵢ. Its proof is the classical one: sᵢ negates αᵢ and permutes the remaining positive roots, so the pairings of those remaining roots with αᵢ^∨ cancel in pairs and only ⟨αᵢ, αᵢ^∨⟩ = 2 survives.

Those values on the simple coroots determine the values on all of them, and the answer is the height of the coroot: expanding α^∨ in the simple coroots and pairing termwise gives ⟨ρ, α^∨⟩ = ht(α^∨), the sum of the coefficients. Two consequences of that identity are recorded below. First, ⟨ρ, α^∨⟩ is never zero, because no root has height zero — so ρ is a regular weight, with no order on the coefficient ring needed. Over a linearly ordered ring that already follows from strict dominance, but a root system attached to a Lie algebra over an algebraically closed field carries no order, and it is there that the Weyl dimension formula needs its denominators ⟨ρ, α^∨⟩ to be invertible. Second, where there is an order, the pairing with a positive coroot is not merely positive but at least 1, being a positive integer.

Main definitions #

Ado.twoWeylVector: the sum of the positive roots, that is 2ρ.
Ado.weylVector: the Weyl vector ρ, the half-sum of the positive roots, defined when 2 is invertible in the coefficient ring.

Main results #

Ado.coroot'_twoWeylVector and Ado.coroot'_weylVector: ⟨2ρ, αᵢ^∨⟩ = 2 and ⟨ρ, αᵢ^∨⟩ = 1 for every simple root αᵢ.
Ado.reflection_twoWeylVector and Ado.reflection_weylVector: sᵢ(2ρ) = 2ρ - 2αᵢ and sᵢ(ρ) = ρ - αᵢ.
Ado.sum_root_negRootsFinset: the sum of the negative roots is -2ρ.
Ado.coroot'_twoWeylVector_eq_two_mul_height_flip and Ado.coroot'_weylVector_eq_height_flip: ⟨2ρ, α^∨⟩ = 2 ht(α^∨) and ⟨ρ, α^∨⟩ = ht(α^∨) for an arbitrary root α, the general form of the two preceding identities.
Ado.isRegularWeight_twoWeylVector and Ado.isRegularWeight_weylVector: 2ρ and ρ are regular weights, needing no order on the coefficient ring, with Ado.coroot'_twoWeylVector_ne_zero and Ado.coroot'_weylVector_ne_zero the pairings that witness it and Ado.twoWeylVector_ne_zero, Ado.weylVector_ne_zero the resulting nonvanishing.
Ado.reflection_add_weylVector_sub_weylVector: the dot action of a simple reflection, sᵢ ⬝ λ = λ - (⟨λ, αᵢ^∨⟩ + 1) αᵢ.
Ado.add_weylVector_mem_openDominantChamber and Ado.weylVector_mem_openDominantChamber: over a linearly ordered coefficient ring the ρ-shift of a dominant weight is strictly dominant, and ρ itself is a regular weight.
Ado.openDominantChamber_nonempty: consequently the open dominant chamber has a point, which over a general coefficient ring is a genuine hypothesis rather than a formality.
Ado.one_le_coroot'_weylVector_of_mem_posRoots and Ado.coroot'_weylVector_le_neg_one_of_mem_negRoots: over a linearly ordered coefficient ring ⟨ρ, α^∨⟩ ≥ 1 for a positive root and ≤ -1 for a negative one.

References #

This file supplies the root-pairing-level prerequisite of the Weyl vector of the highest-weight theory: the nonvanishing and integrality of ⟨ρ, α^∨⟩ proved below are what makes the denominator of the Weyl dimension formula dim L(λ) = ∏_{α>0} ⟨λ+ρ, α^∨⟩ / ⟨ρ, α^∨⟩ meaningful. Nothing here is a Lie-algebra-level declaration: ρ is built for an abstract root pairing, where the positive-root combinatorics it needs already lives, so that the Lie-algebra version is a specialization rather than a rebuild.

The argument is the one in J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, Ch. III, §10.2 and §13.3.