The formal character of a highest weight module against the Weyl denominator #
Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over an algebraically
closed field of characteristic zero, let H be a Cartan subalgebra and b a base of its root
system. The Weyl character formula is the identity ch L(λ) · Δ = N(λ) in the integral group
algebra ℤ[Module.Dual K H], between the formal character of the irreducible module of highest
weight λ, the Weyl denominator Δ = ∏_{α>0}(1 - e^{-α}) and the Weyl numerator
N(λ) = ∑_w sgn(w) e^{w ⬝ λ}. This file establishes the three properties of the left-hand side
that the formula is read off from.
The first is universal: for any finite-dimensional module M the product ch M · Δ is
alternating for the dot action (TauCeti.isDotAlternating_formalCharacter_mul_weylDenominator),
because the character is invariant for the linear action
(TauCeti.isWeylInvariant_formalCharacter, which is the Weyl invariance of weight multiplicities,
proved in TauCeti/Algebra/Lie/Weights/WeylInvariance.lean directly from the rank-one theory) and
the denominator is alternating for the dot action.
The other two locate the product in the weight order, and they are what makes the alternating
element ch M · Δ a specific one. If M is generated by a highest weight vector of weight
lam, then ch M · Δ is supported in lam - Q⁺
(TauCeti.sub_mem_posRootCone_of_coeff_formalCharacter_mul_weylDenominator_ne_zero) and its
coefficient at lam itself is 1
(coeff_formalCharacter_mul_weylDenominator_eq_one_of_isHighestWeightVector_of_lieSpan_eq_top):
the top weight space of a highest weight module is a line and the constant term of Δ is 1, and
the positive root cone is pointed, so lam admits only the one decomposition.
Together these are the input to the alternation step of the character formula: ch M · Δ is an
alternating element, supported in lam - Q⁺, whose coefficient at lam is 1. Being alternating
and supported in lam - Q⁺ already pins the element down completely once its coefficients at the
dominant integral weights are known, and the last result below says so. Identifying it with
the Weyl numerator N(lam) therefore comes down to a single further statement, which is not
proved here: that no dominant integral weight other than lam carries a nonzero coefficient.
The determination is read off from
TauCeti.IsDotAlternating.eq_of_forall_coeff_dominantIntegral_eq rather than from the chamber
statement TauCeti.IsDotAlternating.eq_of_coeff_openDotDominantChamber_eq, whose fundamental
domain is cut out by inequalities and so needs a linear order on the coefficient ring compatible
with its ring structure: the ring here is an algebraically closed field, which carries no such
order.
Main results #
TauCeti.isWeylInvariant_formalCharacter: the formal character is Weyl-invariant.TauCeti.isDotAlternating_formalCharacter_mul_weylDenominator: the formal character times the Weyl denominator is alternating for the dot action.TauCeti.sub_mem_posRootCone_of_coeff_formalCharacter_mul_weylDenominator_ne_zero: for a highest weight module of weightlam, that product is supported inlam - Q⁺;coeff_formalCharacter_mul_weylDenominator_eq_one_of_isHighestWeightVector_of_lieSpan_eq_top: and its coefficient atlamis1.TauCeti.formalCharacter_mul_weylDenominator_eq_of_forall_coeff_isDominantIntegral_eq: that product is determined by its coefficients at the dominant integral weights, withTauCeti.exists_intCast_eq_coroot'_of_sub_mem_posRootConethe integrality of the weights belowlamthat the determination consumes.
References #
This builds towards the Weyl character formula of Layer 6 ("the Weyl character, dimension, and
Kostant formulas") of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md, whose
proof route is fixed there as "defining Verma characters, proving the Weyl denominator identity
combinatorially, and concluding by Weyl alternation".
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, Ch. VI, §24.
- J.-P. Serre, Complex Semisimple Lie Algebras, Ch. VII, §7.
The character of any finite-dimensional module #
The formal character of a finite-dimensional module is Weyl-invariant: the multiplicity of
a weight is unchanged by the linear action of the Weyl group. This is
TauCeti.formalCharacter_coeff_weylGroup_smul, packaged as the predicate.
The formal character of a finite-dimensional module times the Weyl denominator is alternating for the dot action.
This holds for every finite-dimensional module, with no highest weight hypothesis, and it is the
hypothesis TauCeti.IsDotAlternating.eq_weylNumerator consumes, which is what reduces the
character formula to a statement about the coefficients of the product on a fundamental domain of
the dot action.
The character of a highest weight module #
The formal character of a highest weight module is supported in lam - Q⁺. This is
TauCeti.sub_mem_posRootCone_of_genWeightSpace_ne_bot_of_isHighestWeightVector_of_lieSpan_eq_top,
read on the coefficients of the character.
The formal character of a highest weight module has coefficient 1 at its highest weight:
the top weight space is the line spanned by the generator, by
TauCeti.genWeightSpace_eq_span_singleton_of_isHighestWeightVector_of_lieSpan_eq_top.
The formal character of a highest weight module times the Weyl denominator is supported in
lam - Q⁺. Both factors are supported downwards from their own top weight, and the positive
root cone is closed under addition.
The formal character of a highest weight module times the Weyl denominator has coefficient
1 at the highest weight.
The only way to write lam as a weight of M plus a weight of the denominator is lam + 0: the
two summands are lam minus an element of the positive root cone and minus an element of that
cone, and the cone is pointed. The surviving term is the product of the two top coefficients, both
of which are 1.
Determination by the dominant integral coefficients #
Every simple coroot takes an integer value on a weight below lam. The difference
lam - chi lies in Q⁺, where the coroot functionals take integer values
(TauCeti.exists_intCast_eq_coroot'_of_mem_posRootCone), and lam itself takes natural values on
the simple coroots, being the weight of a highest weight vector in a finite-dimensional module.
This is the integrality that TauCeti.IsDotAlternating.eq_of_forall_coeff_dominantIntegral_eq
consumes, and it applies to ch M · Δ through
TauCeti.sub_mem_posRootCone_of_coeff_formalCharacter_mul_weylDenominator_ne_zero.
The product of the formal character of a highest weight module with the Weyl denominator is determined by its coefficients at the dominant integral weights.
This is what reduces the Weyl character formula ch L(lam) · Δ = N(lam) to a statement about the
dominant integral weights alone: the two sides are alternating for the dot action and supported in
lam - Q⁺, so TauCeti.IsDotAlternating.eq_of_forall_coeff_dominantIntegral_eq identifies them as
soon as their dominant integral coefficients agree. The two hypotheses on the comparison element
g are exactly the two properties of ch M · Δ proved above, so the statement is symmetric in the
two sides; beyond the dot alternation hgalt, no Weyl-orbit and no Weyl-group finiteness
hypothesis is asked of g. Its integrality on the simple coroots is not asked either: it already
follows from hgcone, by TauCeti.exists_intCast_eq_coroot'_of_sub_mem_posRootCone.