Highest weight vectors and dominant integral weights #
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 and let b be a base of the root
system LieAlgebra.IsKilling.rootSystem H, so that the nilradicals and the Borel subalgebra of
TauCeti/Algebra/Lie/Weights/Borel.lean are available. This file introduces the two notions the
classification of the finite-dimensional irreducible modules is stated with, and proves the
implication between them that the rank-one theory already supplies.
A vector v of an L-module M is a highest weight vector of weight lam when it is
nonzero, when the Cartan subalgebra acts on it through the linear form lam, and when the whole
positive nilradical n⁺ annihilates it (Ado.IsHighestWeightVector). A linear form
lam : Module.Dual K H is dominant integral when its value on each simple coroot is a natural
number (Ado.IsDominantIntegral).
The main theorem is Ado.IsHighestWeightVector.isDominantIntegral: the weight of a highest
weight vector in a finite-dimensional module is dominant integral. The proof is the rank-one
reduction, one simple root at a time. A simple root αᵢ is positive, so the root space Lαᵢ
annihilates v, and v is an eigenvector of αᵢ^∨ with eigenvalue lam (αᵢ^∨); that is exactly
the hypothesis of
Ado.exists_nat_of_lie_coroot_eq_smul_of_forall_rootSpace_lie_eq_zero, which produces the
natural number through the sl₂ triple of αᵢ. Dominance then propagates from the simple coroots
to all the positive ones by pure root-system combinatorics
(Ado.IsDominantIntegral.exists_nat_apply_coroot), a positive coroot being a natural
combination of the simple coroots.
Main definitions #
Ado.IsHighestWeightVector b lam v:vis nonzero,Hacts on it bylam, and the positive nilradical ofbannihilates it.Ado.IsHighestWeightVector.weight: the weight ofMthat a highest weight vector exhibits.Ado.IsDominantIntegral b lam: the value oflamon every simple coroot is a natural number.
Main results #
Ado.rootSystem_coroot'_apply: the coroot functional of the abstract root-pairing API is evaluation at the coroot, the dictionary through which the general root-system results apply to dominance and integrality here.Ado.isHighestWeightVector_iff_forall_rootSpace: it is enough to check that each positive root space annihilatesv, the positive nilradical being spanned by them.Ado.IsHighestWeightVector.unique: a vector is a highest weight vector for at most one weight.Ado.IsHighestWeightVector.mapandAdo.IsHighestWeightVector.congr: morphisms with nonzero image, and in particular equivalences, preserve highest weight vectors and their weights.Ado.isHighestWeightVector_coe_iff: a vector of a Lie submodule is a highest weight vector there exactly when it is one in the ambient module.Ado.IsHighestWeightVector.mem_genWeightSpaceandAdo.IsHighestWeightVector.weight: a highest weight vector really does exhibitlamas a weight ofM, so the vocabulary is not vacuous.Ado.IsDominantIntegral.exists_nat_apply_coroot: a dominant integral weight takes natural values on every positive coroot, not only on the simple ones.Ado.IsDominantIntegral.isIntegralWeight: every dominant integral weight is integral.Ado.IsHighestWeightVector.isDominantIntegral: the weight of a highest weight vector in a finite-dimensional module is dominant integral.
Implementation notes #
Ado.IsHighestWeightVector is stated as the conjunction pinned by the roadmap rather than as a
structure, and Ado.isHighestWeightVector_iff together with the three projections
Ado.IsHighestWeightVector.ne_zero, Ado.IsHighestWeightVector.lie_eq_smul and
Ado.IsHighestWeightVector.lie_eq_zero_of_mem_positiveNilradical is its elimination API; no
consumer needs to take the conjunction apart by hand.
The canonical public helper Ado.lieAnnihilator in Ado.Algebra.Lie.Basic packages the
elements annihilating a vector as a Lie subalgebra. Here it lets
Ado.positiveNilradical_le_iff extend positive-root-space annihilation to the positive
nilradical; Ado.IsHighestWeightVector.lie_eq_zero_of_weight_zero uses the same helper with
Ado.negativeNilradical_le_iff for the negative nilradical.
Finite-dimensionality of M is a hypothesis of the dominance theorem alone: the definitions and
the elimination API are stated for an arbitrary L-module, since the Verma modules that Layer 3 of
the roadmap builds next are infinite-dimensional and carry highest weight vectors all the same.
References #
This file supplies the "highest weight vectors" item of Layer 3 and the IsDominantIntegral
definition of Layer 4 of
TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md, whose target signatures
IsHighestWeightVector and IsDominantIntegral are pinned in the accompanying Suggested.lean.
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §20.2.
Highest weight vectors #
A highest weight vector of weight lam, relative to the positive system determined by the
base b: a nonzero vector on which the Cartan subalgebra acts through the linear form lam and
which is annihilated by the positive nilradical n⁺.
For a single positive root this is IsSl2Triple.HasPrimitiveVectorWith, and that is how the
dominance theorem Ado.IsHighestWeightVector.isDominantIntegral below consumes it.
Equations
Instances For
The three defining conditions on a highest weight vector.
A highest weight vector is nonzero.
The Cartan subalgebra acts on a highest weight vector through its weight.
The positive nilradical annihilates a highest weight vector.
A morphism of Lie modules preserves a highest weight vector and its weight whenever its image is nonzero.
An equivalence of Lie modules preserves highest weight vectors and their weights.
Every positive root space annihilates a highest weight vector.
A highest weight vector determines its weight. A vector is a highest weight vector for at
most one linear form, since it is nonzero and each value lam x is read off the action of x.
Highest weight vectors of a Lie submodule #
A vector of a Lie submodule is a highest weight vector of that submodule exactly when it is one of the ambient module: both defining conditions are read off the ambient bracket.
Recognising a highest weight vector on the root spaces #
Positive root spaces suffice. A nonzero H-eigenvector annihilated by the root space of
every positive root is a highest weight vector: the positive nilradical is spanned by those root
spaces, and the annihilator of a vector is a Lie subalgebra, so the universal property
Ado.positiveNilradical_le_iff applies.
Being a highest weight vector is exactly being a nonzero H-eigenvector annihilated by every
positive root space.
The weight exhibited by a highest weight vector #
A nonzero rescaling of a highest weight vector is again one, of the same weight: the two conditions a highest weight vector satisfies are linear, so only the nonvanishing constrains the scale.
A highest weight vector lies in the generalized weight space of its weight; being an honest simultaneous eigenvector, it does so at nilpotency index one.
The weight of a highest weight vector is a weight of the module: the vocabulary is not vacuous.
The weight of M exhibited by a highest weight vector, packaging
Ado.IsHighestWeightVector.genWeightSpace_ne_bot so that Mathlib's weight API applies to it.
Instances For
Dominant integral weights #
The two coroot interfaces agree. The root system of a splitting Cartan subalgebra pairs a
weight with a coroot by evaluation, so the coroot functional RootPairing.coroot' i of the
abstract root-pairing API is evaluation at the coroot of i.
This is the dictionary between the root-pairing formulation of dominance and integrality, in which the general root-system results are stated, and the Lie-theoretic one used below.
A linear form on the Cartan subalgebra is dominant integral for the base b when its value
on the coroot of every simple root is a natural number.
Equations
- Ado.IsDominantIntegral b lam = ∀ i ∈ b.support, ∃ (n : ℕ), lam ((LieAlgebra.IsKilling.rootSystem H).coroot i) = ↑n
Instances For
The defining condition on a dominant integral weight.
The zero weight is dominant integral.
Dominant integral weights are closed under addition.
Dominance extends from the simple coroots to all the positive ones. A dominant integral
weight takes a natural value on the coroot of every positive root, because such a coroot is a
natural combination of the simple coroots
(Ado.exists_coroot_eq_sum_nat_of_mem_posRoots).
A dominant integral weight is integral: it takes integer values on every coroot, not just natural values on the simple ones. A coroot is the coroot of a positive root or the negative of one, and on a positive coroot dominance gives a natural value.
The weight of a highest weight vector is dominant integral #
The weight of a highest weight vector is dominant integral. For a highest weight vector v
in a finite-dimensional module and a simple root αᵢ, the vector v is an eigenvector of the
coroot αᵢ^∨ with eigenvalue lam (αᵢ^∨) and is annihilated by the root space Lαᵢ, simple roots
being positive; the sl₂ triple of αᵢ then forces the eigenvalue to be a natural number.
This is the half of the highest-weight classification that the rank-one theory supplies on its own. The converse, that every dominant integral weight is the weight of a highest weight vector in a finite-dimensional module, needs the Verma modules and is not proved here.