The spectrum of the Cartan element of an sl₂ triple #
Fix an sl₂ triple t : IsSl2Triple h e f in a Lie algebra L and a finite-dimensional
L-module M. This file describes the spectrum of h on M: its eigenvalues are integers,
and — once the base field is algebraically closed — the eigenspaces span M, so h acts
diagonalizably.
Mathlib's IsSl2Triple.HasPrimitiveVectorWith.exists_nat pins the weight of a primitive vector
to a natural number, and TauCeti/Algebra/Lie/Sl2/Classification.lean reads the whole spectrum off
the classification for an irreducible module. Neither covers an arbitrary module: an eigenvector
of h need not be primitive, and a general module is not irreducible. The gap is closed by raising:
the raising operator e moves the μ-eigenspace into the μ + 2-eigenspace, so applying it
repeatedly to an eigenvector either produces eigenvectors for the infinitely many distinct
eigenvalues μ, μ + 2, μ + 4, … — impossible in finite dimension — or dies, and the last nonzero
vector is a primitive vector of weight μ + 2k. Since that weight is a natural number n, the
original eigenvalue is μ = n - 2k, an integer.
That argument needs neither irreducibility nor an algebraically closed field: it works over any
field of characteristic zero, which matters because it is exactly the form in which the
highest-weight theory consumes it, restricting a module over a semisimple Lie algebra to the sl₂
triple attached to a root in order to prove that weights pair integrally with coroots.
Diagonalizability is a genuinely stronger statement and costs more. The sum of the eigenspaces of
h is a Lie submodule for the subalgebra t.toLieSubalgebra K generated by the triple (e, f
and h shift the eigenvalue by 2, -2 and 0), so complete reducibility,
Ado.exists_isCompl_of_toLieSubalgebra_eq_top, supplies a complementary Lie submodule; over an
algebraically closed field a nonzero complement would contain an eigenvector of h, which already
lies in the sum. Hence the complement vanishes and the eigenspaces exhaust M. Only here is
IsAlgClosed needed. Since everything happens over the subalgebra generated by the triple — which
that triple does generate — the triple itself need not generate the ambient L.
Main results #
Ado.exists_hasPrimitiveVectorWith_pow_toEnd_e: raising an eigenvector to a primitive vector. Some power of the raising operator carries anh-eigenvector of weightμto a primitive vector of weightμ + 2k.Ado.exists_int_of_hasEigenvalue: the integer spectrum. Every eigenvalue of the Cartan element of ansl₂triple on a finite-dimensional module is an integer. Its refinementAdo.exists_nat_sub_two_mul_of_lie_h_eq_smulexhibits the eigenvalue asn - 2kwithn k : ℕ.Ado.eigenspace_toEnd_eq_bot_of_forall_ne_intCast: the eigenspaces at non-integer scalars vanish.Ado.iSup_eigenspace_toEnd_eq_top: diagonalizability. Over an algebraically closed field of characteristic zero, the eigenspaces of the Cartan element of ansl₂triple span the module.Ado.iSup_eigenspace_toEnd_intCast_eq_topandAdo.isInternal_eigenspace_toEnd_intCast: the two halves combined — such a module is the internal direct sum of the eigenspaces at the integers.
References #
This is the "diagonalizability and the integer spectrum" bullet of Layer 0 of
TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md, whose
sl2_hAction_eigenvalue_isInt is Ado.exists_int_of_hasEigenvalue.
- [J. E. Humphreys, Introduction to Lie Algebras and Representation Theory][humphreys1972], §7.2.
The raising argument in Ado.exists_hasPrimitiveVectorWith_pow_toEnd_e follows the proof of
Mathlib's IsSl2Triple.exists_hasPrimitiveVectorWith, which runs it from an eigenvector produced by
triangularizability; the version here starts from an eigenvector supplied by the caller, which is
what makes the eigenvalue statements below available without a triangularizability hypothesis.
Raising an eigenvector to a primitive vector #
Raising an eigenvector to a primitive vector. If m ≠ 0 is an h-eigenvector of weight
μ, then some power eᵏ • m is a primitive vector, of weight μ + 2k.
The raising operator shifts the weight by 2, so if no power of e killed m the vectors
m, e • m, e² • m, … would be eigenvectors for the pairwise distinct weights μ, μ + 2, μ + 4, …,
hence linearly independent — impossible in a Noetherian module. The last nonzero vector of the
string is therefore killed by e, which is precisely primitivity.
Mathlib's IsSl2Triple.exists_hasPrimitiveVectorWith is this argument started from an eigenvector
obtained from LieModule.IsTriangularizable; taking the eigenvector as input instead is what lets
the integrality statements below dispense with that hypothesis.
The eigenvalues of the Cartan element are integers, explicitly. An h-eigenvector of weight
μ in a finite-dimensional module raises to a primitive vector of weight μ + 2k, and the weight
of a primitive vector is a natural number n (IsSl2Triple.HasPrimitiveVectorWith.exists_nat), so
μ = n - 2k.
The integer spectrum, in eigenvector form. The weight of a nonzero h-eigenvector in a
finite-dimensional module is an integer.
The integer spectrum. Every eigenvalue of the Cartan element h of an sl₂ triple on a
finite-dimensional module is an integer.
No irreducibility is assumed, and the field need not be algebraically closed: this is the form in
which the highest-weight theory uses it, restricting a module over a semisimple Lie algebra to the
sl₂ triple attached to a root to see that its weights pair integrally with the coroot. It extends
IsSl2Triple.HasPrimitiveVectorWith.exists_nat from the primitive vectors to the whole spectrum.
No eigenvalues off the integers. The eigenspace of the Cartan element at a scalar that is not an integer is trivial.
This is deliberately not a simp lemma: the triple t mentions e and f, which do not occur
in the left-hand side, so simp cannot infer them (the simpNF linter rejects the tag).
The eigenspaces of the Cartan element form a Lie submodule #
The raising operator moves the μ-eigenspace of the Cartan element into the
μ + 2-eigenspace.
The lowering operator moves the μ-eigenspace of the Cartan element into the
μ - 2-eigenspace.
The Cartan element preserves its own eigenspaces.
The sum of the eigenspaces of the Cartan element, as a Lie submodule. The three generators
of the triple shift the eigenvalue by 2, -2 and 0, so the span of the eigenspaces is invariant
under the subalgebra t.toLieSubalgebra K they generate; it is not in general invariant under the
ambient Lie algebra L.
This is the object complete reducibility is applied to in
Ado.iSup_eigenspace_toEnd_eq_top; its underlying submodule is
Ado.eigenspaceSup_toSubmodule, which is the abstraction boundary importing modules should use
rather than unfolding the definition.
Equations
- Ado.eigenspaceSup t = t.lieSubmoduleOfStable (⨆ (ν : K), ((LieModule.toEnd K L M) h).eigenspace ν) ⋯ ⋯
Instances For
The submodule underlying Ado.eigenspaceSup is the sum of the eigenspaces of the Cartan
element. This is the abstraction boundary: it is how a downstream proof should pass between the
bundled Lie submodule and the eigenspaces, rather than unfolding the definition.
An eigenvector of the Cartan element lies in the sum of its eigenspaces,
Ado.eigenspaceSup.
Diagonalizability of the Cartan element #
The Cartan element acts diagonalizably. Over an algebraically closed field of characteristic
zero, the eigenspaces of the Cartan element of an sl₂ triple span every finite-dimensional module
over the ambient Lie algebra.
Only the action of the subalgebra t.toLieSubalgebra K generated by the triple is used, so the
triple need not generate L: the eigenspaces span a Lie submodule for that subalgebra
(Ado.eigenspaceSup), which by complete reducibility
(Ado.exists_isCompl_of_toLieSubalgebra_eq_top, applied over the subalgebra, which its own
triple does generate) has a complement. A nonzero complement is itself a finite-dimensional module
over an algebraically closed field, so h has an eigenvector in it — but every eigenvector already
lies in the span, and the two meet only in 0. So the complement is trivial.
The integral weight decomposition. The two halves of the layer meet: the eigenspaces of the
Cartan element span (Ado.iSup_eigenspace_toEnd_eq_top) and they are supported on the integers
(Ado.exists_int_of_hasEigenvalue), so a finite-dimensional module is spanned by the
eigenspaces at the integers.
The eigenspace decomposition at the integers. The internal direct sum form of
Ado.iSup_eigenspace_toEnd_intCast_eq_top.
The model sl₂ #
The integer spectrum for sl (Fin 2) K. Every eigenvalue of the Cartan element
h = E₀₀ - E₁₁ on a finite-dimensional sl (Fin 2) K-module is an integer.
Neither irreducibility nor an algebraically closed field is assumed, which is what distinguishes this from what the classification of the irreducibles delivers.
Diagonalizability for sl (Fin 2) K. Over an algebraically closed field of characteristic
zero, a finite-dimensional sl (Fin 2) K-module is the direct sum of the integer eigenspaces of the
Cartan element h = E₀₀ - E₁₁.