Every finite-dimensional gl n-module has a dominant highest weight vector #
Let K be a field of characteristic zero and let M be a nonzero finite-dimensional module over
gl n K = Matrix n n K. This file proves that M carries a highest weight vector for the matrix
unit positive system, and that the weight of any highest weight vector of a finite-dimensional
module is dominant integral. Read for an irreducible M, the two statements say that every
finite-dimensional irreducible gl n-module has a dominant highest weight, which is the existence
half of the classification of the irreducibles of gl n.
The argument #
Existence is Lie's theorem followed by a maximality argument, and both halves are needed. Lie's theorem is applied to the abelian diagonal Cartan subalgebra rather than to the Borel subalgebra of upper triangular matrices, which is the other classical route: a common eigenvector of the Borel is a highest weight vector outright, but that route first needs the Borel to be solvable and its derived subalgebra to contain the raising matrix units, neither of which is available.
The diagonal Cartan subalgebra is abelian, hence solvable, so over an algebraically closed field
Lie's theorem (LieModule.exists_nontrivial_weightSpace_of_isSolvable) produces a nonzero
simultaneous eigenvector of the diagonal matrix units. Algebraic closure is not a convenience
here: over ℝ a simultaneous eigenvector need not exist at all. Neither may one replace this step
by the argument used for a semisimple Lie algebra, where the generalized weight spaces are refined
to honest eigenspaces once and for all: gl 1 acting on K² by a nilpotent Jordan block is a
finite-dimensional module on which the Cartan subalgebra does not act semisimply, so a highest
weight vector has to be produced one vector at a time rather than as a whole weight space.
Such an eigenvector need not be annihilated by the raising matrix units, and the second half of
the argument moves it up until it is. Bracketing with Eₚq sends an eigenvector of weight μ to
an eigenvector of weight μ + εₚ - ε_q, so, writing ht μ for the value of μ on the fixed
diagonal matrix ∑ i, -i · Eᵢᵢ, one raising step with p < q increases ht by the positive
natural number q - p. All the vectors so produced are eigenvectors of a single operator, the
action of that fixed diagonal matrix, with pairwise distinct eigenvalues, so there are only
finitely many of them: the set of naturals m for which an eigenvector of ht-value ht μ₀ + m
exists is finite. A vector realizing its greatest element is moved by no raising operator, which
is exactly a highest weight vector.
Dominance is the rank-one reduction. For p < q the matrix units Eₚq, E_qp and their
commutator Eₚₚ - E_qq form an sl₂ triple, and a highest weight vector is a primitive vector
for it with eigenvalue μ p - μ q; Mathlib's IsSl2Triple.HasPrimitiveVectorWith.exists_nat then
makes that eigenvalue a natural number. Only finite-dimensionality of M is used, so dominance
needs neither irreducibility nor an algebraically closed field.
Main results #
TauCeti.exists_isGlHighestWeightVector: a nonzero finite-dimensional module overgl n K, forKalgebraically closed of characteristic zero, has a highest weight vector.TauCeti.IsGlHighestWeightVector.isGlDominantIntegral: the weight of a highest weight vector in a finite-dimensionalgl n K-module is dominant integral.TauCeti.lie_single_self_lie_single_eq_smul: bracketing with a matrix unit shifts the weight of a simultaneous eigenvector of the diagonal.TauCeti.exists_isGlHighestWeightVector_and_isGlDominantIntegral: the two main results together.
References #
- W. Fulton, J. Harris, Representation Theory: A First Course, Springer GTM 129 (1991), §15.
- R. Goodman, N. R. Wallach, Symmetry, Representations, and Invariants, Springer GTM 255 (2009), Chapter 5.
This is the first target of the "classification and the named carrier" item of Layer 9 of
TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md: "Every finite-dimensional
gl_n-irreducible has a dominant highest weight".
Simultaneous eigenvectors of the diagonal #
Lie's theorem for the diagonal Cartan subalgebra: over an algebraically closed field of
characteristic zero a nonzero finite-dimensional gl n-module has a nonzero simultaneous
eigenvector of the diagonal matrix units.
The eigenvector is not asserted to be annihilated by the raising matrix units; that is what
TauCeti.exists_isGlHighestWeightVector adds.
Raising a weight vector. Bracketing a simultaneous eigenvector of the diagonal matrix units
of weight μ with the matrix unit Eₚq gives a simultaneous eigenvector of weight
μ + εₚ - ε_q, whenever the result is nonzero.
Existence of a highest weight vector #
Existence of a highest weight vector for gl n. Over an algebraically closed field of
characteristic zero every nonzero finite-dimensional gl N-module has a highest weight vector for
the matrix unit positive system.
Neither irreducibility nor a choice of generator is assumed; for irreducible M this is the
existence half of the classification of the finite-dimensional irreducibles of gl N.
Dominance of the highest weight #
The sl₂ triple of a pair of indices in gl n. For p ≠ q the matrix units Eₚq and
E_qp together with their commutator Eₚₚ - E_qq satisfy the sl₂ relations; this is the
rank-one subalgebra of gl n along which dominance is read off.
It is the standard triple TauCeti.isSl2Triple_single of sl n K, pushed forward along the
inclusion of sl n K in gl n K.
The weight of a highest weight vector is dominant integral. Restricting to the sl₂ triple
of a pair p < q makes the highest weight vector a primitive vector of eigenvalue μ p - μ q, and
the eigenvalue of a primitive vector in a finite-dimensional module is a natural number.
Neither irreducibility of M nor algebraic closure of K is used.
Every nonzero finite-dimensional gl N-module has a dominant highest weight vector. Over
an algebraically closed field of characteristic zero, combining the existence of a highest weight
vector with the dominance of its weight.
For an irreducible M this is the statement that a finite-dimensional irreducible gl N-module
has a dominant highest weight, the first half of the classification of the irreducibles of
gl N.