The Weyl dimension formula #
Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over an algebraically
closed field of characteristic zero, H a Cartan subalgebra, b a base of its root system with
Weyl vector ρ, and M a finite-dimensional module generated by a highest weight vector of
weight lam. The Weyl dimension formula computes the dimension of M:
dim M = ∏_{α>0} ⟨lam + ρ, α^∨⟩ / ⟨ρ, α^∨⟩.
Every factor is a quotient of integers, the coroot pairings TauCeti.coweightPairing of the
integral weights lam + ρ and ρ, and the denominators are nonzero, so the identity is stated
in ℚ; in its division-free form dim M · ∏_{α>0} ⟨ρ, α^∨⟩ = ∏_{α>0} ⟨lam + ρ, α^∨⟩ it is an
identity of integers.
The formula is the specialization of the Weyl character formula
TauCeti.formalCharacter_mul_weylDenominator_eq_weylNumerator along the exponential
e^ν ↦ e^{⟨ρ, ν⟩ X}, and that specialization is carried out for an abstract root pairing in
TauCeti/LinearAlgebra/RootSystem/Weyl/Dimension.lean. The root-pairing statement compares two
character identities, ch M · Δ = N(lam) and ch L(0) · Δ = N(0); this file supplies both from
the character formula, the second for the one-dimensional module L(0)
(TauCeti.finrank_irreducibleQuotient_zero), reads the sums of coefficients as dimensions, and
passes from the field K to the integers through TauCeti.intCast_coweightPairing.
Main results #
TauCeti.finrank_mul_prod_coweightPairing_weylVector_eq: the division-free formdim M · ∏_{α>0} ⟨ρ, α^∨⟩ = ∏_{α>0} ⟨lam + ρ, α^∨⟩of the dimension formula, inℤ.TauCeti.finrank_eq_prod_coweightPairing_div: the Weyl dimension formuladim M = ∏_{α>0} ⟨lam + ρ, α^∨⟩ / ⟨ρ, α^∨⟩, inℚ.
References #
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §24.3.
- W. Fulton and J. Harris, Representation Theory: A First Course, GTM 129, §24.2.
The Weyl dimension formula, division-free. For a finite-dimensional module M generated
by a highest weight vector of weight lam,
dim M · ∏_{α>0} ⟨ρ, α^∨⟩ = ∏_{α>0} ⟨lam + ρ, α^∨⟩,
an identity of integers, the coroot pairings being those of the integral weights ρ and
lam + ρ.
The Weyl dimension formula. For a finite-dimensional module M generated by a highest
weight vector of weight lam,
dim M = ∏_{α>0} ⟨lam + ρ, α^∨⟩ / ⟨ρ, α^∨⟩,
the product running over the positive roots, with ρ the Weyl vector of the base and
⟨·, α^∨⟩ the integer coroot pairing TauCeti.coweightPairing. Such an M is irreducible, so
this is the dimension of L(lam) for every dominant integral weight lam at which L(lam) is
nonzero.