Integrality of the weights of a module over a semisimple Lie algebra #
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 M be a finite-dimensional
L-module. This file defines when a linear form is an integral weight and proves that module
weights are integral: for every weight χ of M and every root α, the scalar χ (α^∨) is an
integer.
The proof here is the standard reduction to rank one that organises the whole highest-weight
theory. A nonzero root α carries an sl₂ triple ⟨eₐ, hₐ, fₐ⟩ with eₐ ∈ Lα, fₐ ∈ L₍₋α₎ and,
by Mathlib's IsSl2Triple.h_eq_coroot, hₐ = α^∨. Restricting M along that triple turns
χ (α^∨) into an eigenvalue of the Cartan element of an sl₂ triple on a finite-dimensional
module, and those are integers by Ado.exists_int_of_hasEigenvalue.
Two hypotheses that might be expected are absent. The base field is not assumed algebraically
closed: only the existence of the root system and of the triple attached to α is needed, and both
are available as soon as H is splitting (LieModule.IsTriangularizable K H L). And the weight
spaces are Mathlib's generalized weight spaces, which is all that is available before the
diagonalizability theorem for the Cartan action; a weight χ enters the argument only through
LieModule.Weight.hasEigenvalueAt, which extracts an honest eigenvector of a single x : H from a
nonzero generalized weight space.
The refinements Ado.exists_nat_of_lie_coroot_eq_smul_of_forall_rootSpace_lie_eq_zero and
Ado.exists_nat_neg_of_lie_coroot_eq_smul_of_forall_rootSpace_neg_lie_eq_zero replace ℤ by
ℕ and by -ℕ for a vector on which α^∨ acts by a scalar and which is killed by the root space
Lα, respectively by L₍₋α₎: that is, for a highest, respectively lowest, weight vector in the
α direction. The first is the form in which the classification of the finite-dimensional
irreducibles consumes integrality: restricting a highest weight vector to the sl₂ of each simple
root is what forces its weight to be dominant integral.
Main results #
Ado.IsIntegralWeight: a linear form takes integer values on every coroot. The integral weights contain0and are closed under addition, negation, subtraction andℤ-scaling (Ado.isIntegralWeight_zero,Ado.IsIntegralWeight.add,Ado.IsIntegralWeight.neg,Ado.IsIntegralWeight.sub,Ado.IsIntegralWeight.zsmul).Ado.exists_int_of_hasEigenvalue_coroot: every eigenvalue of a corootα^∨acting on a finite-dimensional module is an integer.Ado.exists_int_apply_coroot: integrality of weights. For a weightχof a finite-dimensional module and a rootα, the valueχ (α^∨)is an integer.Ado.isIntegralWeight_of_weight: a weight of a finite-dimensional module is an integral weight.Ado.exists_int_apply_of_mem_span_coroot: a weight of a finite-dimensional module isℤ-valued on the whole coroot lattice, theℤ-span of the coroots.Ado.exists_nat_of_lie_coroot_eq_smul_of_forall_rootSpace_lie_eq_zeroandAdo.exists_nat_neg_of_lie_coroot_eq_smul_of_forall_rootSpace_neg_lie_eq_zero: a nonzero vector on whichα^∨acts by the scalarμand which is killed by the root spaceLα, respectivelyL₍₋α₎, forcesμto be a natural number, respectively minus a natural number.Ado.forall_rootSpace_neg_lie_eq_zero_of_lie_coroot_eq_zero_of_forall_rootSpace_lie_eq_zero: a finite-dimensionalsl₂string starting at coroot weight zero stops immediately in the negative-root direction.Ado.forall_rootSpace_lie_eq_zero_of_lie_coroot_eq_zero_of_forall_rootSpace_neg_lie_eq_zero: the corresponding statement in the positive-root direction.Ado.genWeightSpaceOf_coroot_eq_bot_of_forall_ne_intCast: the generalized eigenspace of a coroot at a non-integer scalar vanishes.
References #
This is the "integrality of weights (the sl₂ reduction)" item of Layer 2 of
TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md, whose target signature
weight_apply_coroot_isInt is Ado.exists_int_apply_coroot.
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, Chapter VI, §20.
Ado.genWeightSpaceOf_coroot_eq_bot_of_forall_ne_intCast extracts an honest eigenvector from a
nonzero generalized weight space by the argument of Mathlib's LieModule.Weight.hasEigenvalueAt.
The spectrum of a coroot #
The eigenvalues of a coroot are integers. Every eigenvalue of the action of a coroot α^∨
on a finite-dimensional module is an integer.
The weight α is arbitrary: the roots carry the content, while the coroot of a zero weight is zero
and has only the eigenvalue 0.
No generalized eigenvalues of a coroot off the integers. The generalized eigenspace of the
coroot α^∨ on a finite-dimensional module vanishes at every scalar that is not an integer.
This is deliberately not a simp lemma: the hypothesis hμ cannot be discharged by simp from the
left-hand side alone.
Integrality of weights #
A weight is integral when it takes integer values on every coroot.
Equations
- Ado.IsIntegralWeight lam = ∀ (α : LieModule.Weight K (↥H) L), ∃ (n : ℤ), lam (LieAlgebra.IsKilling.coroot α) = ↑n
Instances For
A linear form is integral if it takes an integer value on every coroot.
An integral weight takes an integer value on each coroot.
The zero weight is integral.
A sum of integral weights is integral.
The negative of an integral weight is integral.
A difference of integral weights is integral.
An integer multiple of an integral weight is integral.
Integrality of the weights of a finite-dimensional module. For every weight χ of a
finite-dimensional module M over a Killing-semisimple Lie algebra and every root α, the value
χ (α^∨) is an integer.
The nonzero weights α of L are the roots and carry the content; a zero weight has zero coroot,
and is allowed here only so that no side condition is carried around.
By LieAlgebra.IsKilling.rootSystem_coroot_apply the element α^∨ is the coroot of the Mathlib
root system LieAlgebra.IsKilling.rootSystem H, so this is integrality in the sense that the
dominance conditions of the highest-weight classification use.
The weights of a finite-dimensional module are integral.
A weight is ℤ-valued on the coroot lattice. The coroots of a Killing-semisimple Lie
algebra span a ℤ-lattice in the Cartan subalgebra, and every weight of a finite-dimensional
module takes integer values on it.
The span is over all weights of L rather than over the roots alone; the two agree, the coroot of
the zero weight being zero.
Dominance along a root #
A highest weight vector in the α direction has a natural coroot value. If a nonzero v is
an eigenvector of the coroot α^∨ of a nonzero root α, of eigenvalue μ, and is annihilated by
the root space Lα, then μ is a natural number.
This is the step that turns the highest weight of a finite-dimensional irreducible into a dominant
integral weight, applied to each simple root in turn. Only the action of α^∨ on v is
constrained, and it is constrained by a genuine eigenvector equation, which is strictly stronger
than membership of a generalized weight space.
A lowest weight vector in the α direction has a non-positive coroot value. If a nonzero
v is an eigenvector of the coroot α^∨ of a nonzero root α, of eigenvalue μ, and is
annihilated by the root space L₍₋α₎, then μ is minus a natural number.
A primitive vector of coroot weight zero is also killed in the negative direction. If a
vector is annihilated by Lα and has eigenvalue zero under α^∨, the finite-dimensional sl₂
string through it stops immediately, so L₍₋α₎ also annihilates it.
A lowest-weight vector of coroot weight zero is also killed in the positive direction. If a
vector is annihilated by L₍₋α₎ and has eigenvalue zero under α^∨, the finite-dimensional sl₂
string through it stops immediately, so Lα also annihilates it.