Highest weight modules: the weight cone and the highest weight line #
A highest weight module of weight lam is a module generated by a highest weight vector v of
weight lam, that is one with LieSubmodule.lieSpan K L {v} = ⊤. This file proves the two
structural facts that make the notion useful, both for an arbitrary such module, finite-dimensional
or not.
- Its weights lie in
lam - Q⁺, whereQ⁺is the cone of nonnegative integer combinations of the simple roots (Ado.posRootCone): the weight spaces at those weights already exhaust the module, so no other weight can occur. - Its
lam-weight space is the lineK ∙ v, solamreally is the highest weight andvreally is its highest weight vector, up to a nonzero scalar.
The argument #
Neither statement follows from the weight-space decomposition alone: the span of the weight spaces
at the weights lam - ν with ν ∈ Q⁺ is not stable under L, a positive root vector moving the
top weight space out of the cone. What is true is that the module is already exhausted by the
negative nilradical n⁻ acting on v, which is the statement M = U(n⁻) · v written before the
enveloping algebra is available: the n⁻-submodule LieSubmodule.lieSpan K n⁻ {v} generated by
v is the whole of M.
The key point is that this n⁻-submodule is stable under the Borel subalgebra 𝔟 = H + n⁺, by
induction over the elements of a Lie span: moving x ∈ 𝔟 past a bracket with f ∈ n⁻ costs a term
⁅⁅x, f⁆, -⁆, and the triangular decomposition L = n⁻ + 𝔟
(Ado.negativeNilradical_sup_borelSubalgebra_eq_top) splits ⁅x, f⁆ into a piece that stays
inside the span and a piece the inductive hypothesis handles. With 𝔟 and n⁻ both preserving it,
the n⁻-span is an L-submodule containing v, hence everything. That is
Ado.lieSpan_toSubmodule_le_of_isHighestWeightVector, and every result below is read off it by
exhibiting one n⁻-stable submodule.
The rest is bookkeeping against the cone. The span of the weight spaces at the weights lam - ν
with ν ∈ Q⁺ is such a submodule, so it is everything, and the independence of the weight spaces
(LieModule.iSupIndep_genWeightSpace) converts that into a statement about individual weights.
Taking the indexing set to exclude lam itself is what isolates the highest weight line, and it is
legitimate because a positive root is never cancelled inside the cone
(Ado.root_add_ne_zero_of_mem_posRoots_of_mem_posRootCone).
Main results #
Ado.lieSpan_toSubmodule_le_of_isHighestWeightVectorandAdo.eq_top_of_isHighestWeightVector_of_lieSpan_eq_top: a submodule containing a highest weight vector and stable under the negative nilradical already contains everything that vector generates under all ofL, so in a highest weight module it is the whole module.Ado.iSup_genWeightSpace_sub_posRootCone_eq_top_of_isHighestWeightVector_of_lieSpan_eq_top: the weight spaces at the weightslam - ν,ν ∈ Q⁺, span a highest weight module.Ado.exists_sub_eq_of_genWeightSpace_ne_bot_of_isHighestWeightVector_of_lieSpan_eq_top: hence every weight of a highest weight module is of the formlam - νwithν ∈ Q⁺;Ado.sub_mem_posRootCone_of_genWeightSpace_ne_bot_of_isHighestWeightVector_of_lieSpan_eq_toprestates that for a weight given as a linear form, andAdo.eq_of_isHighestWeightVector_of_lieSpan_eq_topdeduces that a module is a highest weight module for at most one weight;Ado.IsHighestWeightVector.unique_of_isIrreduciblespecializes this to irreducible modules.Ado.genWeightSpace_eq_span_singleton_of_isHighestWeightVector_of_lieSpan_eq_top: thelam-weight space of a highest weight module is the line spanned by its highest weight vector.Ado.exists_eq_smul_of_isHighestWeightVector_of_lieSpan_eq_top: consequently any highest weight vector of weightlamin it is a nonzero multiple of the generating one.
References #
This file supplies the "highest weight modules" half of the "highest weight vectors and modules"
item of Layer 3 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md: "a highest
weight module of weight λ is one generated by such a v; its weights all lie in λ - (ℕ-span of simple roots), and its λ-weight space is the line K·v".
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §20.2.
The triangular decomposition of a stability condition #
The submodule generated by the lowering operators #
A submodule containing a highest weight vector and stable under the negative nilradical
contains everything that vector generates under all of L. This is the content of
M = U(n⁻) · v, written before the enveloping algebra is available: no hypothesis on the module is
needed, only that v is a highest weight vector.
A highest weight module is exhausted by the negative nilradical acting on its generator. A
submodule containing the generator and stable under n⁻ is the whole module.
The weights below the highest weight #
The weights of a highest weight module #
The weight spaces below lam span a highest weight module. Their span contains the
generator and is stable under the negative nilradical, because adding a negative root to a weight
below lam keeps it below lam.
The weights of a highest weight module lie in lam - Q⁺. A weight outside the cone would
have its weight space disjoint from the ones that already exhaust the module.
The weight is taken to be an arbitrary function chi : H → K rather than a linear form, because
LieModule.Weight K H M is only known to be linear when M is finite-dimensional; the conclusion
says in particular that every weight of a highest weight module is linear.
The weights of a highest weight module lie in lam - Q⁺, for a weight presented as a
linear form on the Cartan subalgebra.
A module is a highest weight module for at most one weight. If two highest weight vectors
both generate M, each of their weights lies below the other, and the cone is sharp.
An irreducible module carries highest weight vectors of at most one weight.
The highest weight line #
The top weight space of a highest weight module is a line. Splitting off the weight spaces
strictly below lam, what is left of the module at weight lam is the span of the generator.
A highest weight vector of weight lam in a highest weight module is a nonzero multiple of
the generator. It lies in the lam-weight space, which is the line the generator spans.