Existence and uniqueness of highest weights #
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, let b be a base of the root
system LieAlgebra.IsKilling.rootSystem H, and let M be a nonzero finite-dimensional L-module.
This file proves that M carries a highest weight vector for b
(Ado.exists_isHighestWeightVector), and hence, by
Ado.IsHighestWeightVector.isDominantIntegral, that M has a dominant integral weight.
For irreducible M, its highest weight is unique by
Ado.IsHighestWeightVector.unique_of_isIrreducible from
TauCeti/Algebra/Lie/HighestWeight/Module.lean.
The vector is produced from a maximal weight: a weight χ such that α + χ is a weight of M
for no positive root α (Ado.exists_weight_forall_genWeightSpace_add_eq_bot). Any nonzero
vector of the χ-weight space is then a highest weight vector, because a positive root space maps
the χ-weight space into the (α + χ)-weight space, which is zero. This second step uses the
diagonalizability theorem of TauCeti/Algebra/Lie/Weights/Diagonalizable.lean: the weight spaces
must be honest simultaneous eigenspaces for the Cartan action on the chosen vector to be through
a single linear form.
Maximality itself is a finiteness argument. Were there no maximal weight, every weight χ would
admit a positive root r χ with r χ + χ again a weight, and iterating the resulting successor
map on the finite set of weights would return to a weight already visited. Along such a cycle the
positive roots traversed would sum to zero, which
Ado.sum_root_ne_zero_of_mem_posRoots forbids: a nonempty sum of positive roots has positive
height.
Main results #
Ado.exists_weight_forall_genWeightSpace_add_eq_bot: a nonzero finite-dimensional module has a maximal weight, one that no positive root translates to another weight.Ado.isHighestWeightVector_of_forall_genWeightSpace_add_eq_bot: every nonzero vector of a maximal weight space is a highest weight vector.Ado.exists_isHighestWeightVector: a nonzero finite-dimensional module has a highest weight vector.Ado.exists_weight_isDominantIntegral: that highest weight vector has a dominant integral weight, so a nonzero finite-dimensional module always exhibits one.Ado.exists_isHighestWeightVector_and_lieSpan_eq_top: a finite-dimensional irreducible module is a highest weight module, being generated by a highest weight vector.Ado.exists_isHighestWeightVector_and_isDominantIntegral_of_irreducible: the corresponding roadmap statement for finite-dimensional irreducible modules.Ado.existsUnique_isDominantIntegral_highestWeight_of_finiteDimensional_irreducible: the dominant integral highest weight of a finite-dimensional irreducible module is unique.
Implementation notes #
The maximality statement is phrased on LieModule.genWeightSpace rather than on
LieModule.weightSpace, matching Mathlib's LieModule.Weight, whose defining condition is that the
generalized weight space is nonzero; the two agree here by
Ado.genWeightSpace_eq_weightSpace, and stating it on the generalized spaces is what lets the
proof feed LieModule.lie_mem_genWeightSpace_of_mem_genWeightSpace directly.
That the set of weights is nonempty to begin with is Ado.nonempty_weight, which mentions no
root system and so lives with the general weight theory in
TauCeti/Algebra/Lie/Weights/Diagonalizable.lean; the Killing-semisimple setting supplies the
LieModule.IsTriangularizable instance it wants through
LieModule.instIsTriangularizableOfIsAlgClosed.
The successor map is built by choose from the failure of maximality and iterated with
Function.iterate; the telescoping identity for its iterates is the only bookkeeping lemma the
argument needs, and it is kept inside the proof.
Lie's theorem (LieModule.exists_nontrivial_weightSpace_of_isSolvable) is the other classical route
to a highest weight vector: a common eigenvector for the Borel subalgebra 𝔟 = H ⊕ n⁺ is one, the
eigenvalue vanishing on n⁺. It is not taken here because it needs two theorems that are not yet
available (that 𝔟 is solvable, and that n⁺ lies in its derived subalgebra), whereas the
maximal-weight argument needs only the finiteness of the set of weights.
References #
This proves the existence and uniqueness of the dominant integral highest weight, one part of the
Layer 4 classification step in TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md.
The uniqueness statement is the target
existsUnique_isDominantIntegral_highestWeight_of_finiteDimensional_irreducible in
TauCetiRoadmap/RepresentationTheory/LieHighestWeight/Suggested.lean.
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §20.2 and §21.1.
A maximal weight exists. A nonzero finite-dimensional module has a weight χ such that
α + χ is a weight for no positive root α.
If not, choosing for each weight a positive root translating it to another weight gives a successor
map on the finite set of weights, whose iterates must eventually repeat. The positive roots
traversed between two equal iterates then sum to zero, contradicting
Ado.sum_root_ne_zero_of_mem_posRoots.
A nonzero vector of a maximal weight space is a highest weight vector. If no positive root
α translates lam to a weight of M, then a positive root space carries the lam-weight space
into a zero weight space, so it annihilates every one of its vectors; the Cartan subalgebra acts on
them through lam because the weight spaces are honest simultaneous eigenspaces
(Ado.mem_genWeightSpace_iff_forall_lie_eq_smul).
Existence of a highest weight vector. A nonzero finite-dimensional module over a Killing-semisimple Lie algebra carries a highest weight vector for any base of the root system.
Take a maximal weight (Ado.exists_weight_forall_genWeightSpace_add_eq_bot) and any nonzero
vector of its weight space
(Ado.isHighestWeightVector_of_forall_genWeightSpace_add_eq_bot).
A nonzero finite-dimensional module has a dominant integral weight, packaged as a weight of
the module rather than as a bare linear form: the weight of the highest weight vector produced by
Ado.exists_isHighestWeightVector, dominant by
Ado.IsHighestWeightVector.isDominantIntegral.
A finite-dimensional irreducible module is a highest weight module. It has a highest weight vector, and being irreducible it is generated by it.
This is the shape in which the classification of the finite-dimensional irreducibles consumes the existence theorem: the irreducible is a quotient of the Verma module of its highest weight.
Every finite-dimensional irreducible module has a dominant integral highest weight
vector. Here irreducibility supplies the nontriviality needed by
Ado.exists_isHighestWeightVector; its weight is dominant integral by
Ado.IsHighestWeightVector.isDominantIntegral. This is the form pinned by the roadmap.
Uniqueness of the dominant integral highest weight. A finite-dimensional irreducible module
has a unique dominant integral highest weight. The dominance conjunct is automatic from the highest
weight vector and is retained to match the roadmap target; uniqueness follows from
Ado.eq_of_isHighestWeightVector_of_lieSpan_eq_top.