The weight spaces of a highest weight module are finite-dimensional #
Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over a field of
characteristic zero, let H be a splitting Cartan subalgebra, let b be a base of its root system
and let M be a module generated by a highest weight vector v of weight lam. This file proves
that every weight space of M is finite-dimensional, so that the weight multiplicities
μ ↦ dim Mμ count something. No finiteness is assumed of M itself: a highest weight module is in
general infinite-dimensional, and its finite-dimensionality is the conclusion of a later milestone
rather than a hypothesis here.
The argument #
TauCeti/Algebra/Lie/HighestWeight/Module.lean shows that M is already exhausted by the negative
nilradical acting on v. Refining that statement weight by weight is the whole content of this
file: writing TauCeti.loweredWeightSpace M b chi for the sum, over the negative roots γ, of the
images of the weight space at chi - γ under the root vectors of γ, the family
chi ↦ (K ∙ v ⊓ Mchi) ⊔ loweredWeightSpace M b chi
is stable under the negative nilradical and contains v, so it spans M; each of its members sits
inside the corresponding weight space; and the weight spaces are independent. A family below an
independent family which still spans is equal to it (iSupIndep.le_iff_eq_of_iSup_eq_top), so at a
weight other than lam the weight space is exactly what the lowering operators produce from the
weights one root above it.
Finite-dimensionality then follows by induction on the height of lam - chi, which is a natural
number because lam - chi lies in the positive root cone
(TauCeti.exists_natCast_eq_heightLinearMap_of_mem_posRootCone). At the top weight the weight
space is the line K ∙ v. Below it, each of the finitely many summands of loweredWeightSpace is
a bilinear image of the root space, which is finite-dimensional, and of a weight space at a
strictly smaller height, a negative root having strictly negative height
(TauCeti.height_neg_of_mem_negRoots).
Main definitions #
TauCeti.loweredWeightSpace: what the negative root vectors produce at a given weight.
Main results #
TauCeti.genWeightSpace_eq_loweredWeightSpace_of_isHighestWeightVector_of_lieSpan_eq_top_of_ne: below the highest weight, a weight space of a highest weight module is exactly what the lowering operators produce from above.TauCeti.finiteDimensional_genWeightSpace_of_isHighestWeightVector_of_lieSpan_eq_top: every weight space of a highest weight module is finite-dimensional.
References #
This is the "each weight space is finite-dimensional" half of the finite-dimensionality
milestone of Layer 4, "the classification of finite-dimensional irreducibles", of
TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md. That milestone reads the
statement off the Poincaré--Birkhoff--Witt and Kostant partition bound of Layer 3; the proof here
reads it instead off the lowering description of the weight spaces, which is what makes it
available before the Poincaré--Birkhoff--Witt basis.
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §20.2.
What the lowering operators produce at a weight #
What the negative root vectors produce at the weight chi: the sum, over the negative
roots γ of the base b, of the images of the weight space at chi - γ under the root vectors of
γ. Since a root vector of γ carries the weight space at chi - γ into the one at chi, this
is a submodule of the weight space at chi.
Equations
- One or more equations did not get rendered due to their size.
Instances For
TauCeti.loweredWeightSpace written out as a supremum over the negative roots.
A lowering operator of a negative root lands in TauCeti.loweredWeightSpace: this is the
introduction rule for the definition.
TauCeti.loweredWeightSpace is generated by the lowering operators, so a submodule
contains it as soon as it absorbs every one of them: this is the elimination rule.
What the lowering operators produce at chi lies in the weight space at chi: a root
vector of γ carries the weight space at chi - γ into the weight space at γ + (chi - γ).
The weight spaces are what the lowering operators produce #
Below the highest weight, a weight space of a highest weight module is exactly what the lowering operators produce from the weights one negative root above it.
At the highest weight itself the weight space is instead the line spanned by the generator, by
TauCeti.genWeightSpace_eq_span_singleton_of_isHighestWeightVector_of_lieSpan_eq_top.
Finite-dimensionality #
Every weight space of a highest weight module is finite-dimensional, so its weight multiplicities are finite. The module itself is not assumed finite-dimensional.