The weight string of a primitive vector for an sl₂ triple #
Fix an sl₂ triple t : IsSl2Triple h e f in a Lie algebra L over a commutative ring K, and a
primitive vector m of weight μ in an L-module M. Mathlib supplies the ladder calculus for
the vectors fⁱ • m: their h-eigenvalues (lie_h_pow_toEnd_f), the effect of the
raising operator (lie_e_pow_succ_toEnd_f), the integrality μ = n of the weight of a primitive
vector of a Noetherian torsion-free module (exists_nat), and the two endpoint statements
pow_toEnd_f_ne_zero_of_eq_nat and pow_toEnd_f_eq_zero_of_eq_nat saying that the string
m, f • m, …, fⁿ • m consists of nonzero vectors and stops immediately afterwards.
This file first packages the primitive-vector calculus into the generic conversion and endpoint
forms used by higher Serre relations. It then assembles the string vectors into a submodule: their
span is a Lie submodule for the subalgebra t.toLieSubalgebra K generated by the triple
(Ado.weightStringSubmodule), because each of e, f and h carries a string vector to a
multiple of a string vector. The string vectors lie in distinct h-eigenspaces, so they are
linearly independent; as soon as M is irreducible over that subalgebra the string is therefore a
basis, and M is the standard (n+1)-dimensional irreducible V(n). The span is a Lie submodule
over any commutative coefficient ring. Over a domain of characteristic zero the string of a
torsion-free module is linearly independent; the end of the string, the ladder basis, and the
dimension and classification read off from that basis ask in addition, exactly as Mathlib's
endpoint statements do, that the module be Noetherian — for the classification, both modules.
Irreducibility over t.toLieSubalgebra K — not over the ambient L — is the correct hypothesis:
the adjoint module of sl₃ is irreducible over sl₃ and contains a primitive vector of weight 1
for the sl₂ triple of a simple root, yet has dimension 8, not 2. The two hypotheses agree
when t.toLieSubalgebra K = ⊤, which Ado.toLieSubalgebra_isSl2Triple_single_eq_top
verifies for the standard triple of sl (Fin 2) K.
Main definitions #
Ado.weightStringSubmodule: the span of the weight stringm, f • m, f² • m, …of a primitive vector, as a Lie submodule for the subalgebra generated by the triple.Ado.lieModuleEquivOfHasPrimitiveVectorWith: the classification. Two modules irreducible over the subalgebra of the triple with primitive vectors of the same weight are equivalent over that subalgebra, soV(n)is determined byn. Underlying it is the linear equivalence matching the two ladder bases position by position.
Main results #
Ado.hasPrimitiveVectorWith_symm_of_ne_zero_of_lie_h_eq_smul_of_lie_f_eq_zero: a nonzero weight vector killed by the lowering element is primitive for the symmetric triple, at the negated scalar weight.Ado.pow_toEnd_f_toNat_add_one_eq_zero_of_hasPrimitiveVectorWith: the endpoint of an integral-weight string in a torsion-free Noetherian module, withAdo.ad_pow_lie_eq_zero_of_isSl2Triple_of_lie_h_eq_smul_of_lie_f_eq_zeroas the consumer-facing adjoint consequence.Ado.pow_toEnd_f_eq_zero_of_lt: the string of a primitive vector of weightn : ℕstops afternsteps, not merely at stepn + 1.Ado.linearIndependent_pow_toEnd_f: then + 1vectors of the string are linearly independent, being eigenvectors ofhfor the distinct eigenvaluesn, n - 2, …, -n.Ado.weightStringSubmodule_eq_top: a primitive vector of an irreducible module generates it.Ado.pow_toEnd_e_pow_toEnd_f_selfandAdo.pow_toEnd_e_pow_toEnd_f_eq_zero: raising a string vector back up returns a multiple of the primitive vector, with the explicit ladder coefficient, and raising it further gives zero.Ado.basisOfHasPrimitiveVectorWith: the resulting ladder basis of an irreducible module, with the action of the triple on it read off inAdo.lie_h_basisOfHasPrimitiveVectorWith,Ado.lie_f_basisOfHasPrimitiveVectorWithandAdo.lie_e_basisOfHasPrimitiveVectorWith.Ado.finrank_eq_of_hasPrimitiveVectorWith: the dimension ofV(n). A Noetherian module irreducible over the subalgebra of the triple, with a primitive vector of weightn, has rankn + 1.
References #
This is Layer 0 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md, whose
sl2_finrank_of_hasPrimitiveVector is Ado.finrank_eq_of_hasPrimitiveVectorWith.
- [J. E. Humphreys, Introduction to Lie Algebras and Representation Theory][humphreys1972], §7.2.
A nonzero weight vector killed by the lowering element is primitive for the symmetric
sl₂-triple, with the negated scalar weight.
The weight string as a Lie submodule #
The span of the weight string m, f • m, f² • m, … of a primitive vector m, as a Lie
submodule for the subalgebra t.toLieSubalgebra K generated by the triple. Each of the three
generators of that subalgebra carries a string vector to a multiple of a string vector, so the span
is invariant; it is not in general invariant under the ambient Lie algebra L.
Equations
- Ado.weightStringSubmodule P = t.lieSubmoduleOfStable (Submodule.span K (Set.range fun (i : ℕ) => ((LieModule.toEnd K L M) f ^ i) m)) ⋯ ⋯
Instances For
The underlying submodule of the weight string is the span of the string.
This is the abstraction boundary: importing modules should reason through this lemma rather than
unfold weightStringSubmodule, which is why the definition is not @[expose].
The weight string submodule is nontrivial, the primitive vector m witnessing it: m lies in
the string and is nonzero. This is what lets irreducibility hypotheses be applied to the weight
string.
A primitive vector of an irreducible module generates it: its weight string spans.
Climbing back up the string #
Raising a string vector back to the top. Applying the raising operator j times to the
j-th vector fʲ • m of the weight string of a primitive vector of weight μ returns m, scaled
by the product of the ladder coefficients (i + 1)(μ - i) picked up on the way up.
Raising past the top of the string gives zero. Applying the raising operator more times than the string vector has been lowered lands above the primitive vector, which the raising operator kills.
The string below a primitive vector of integer eigenvalue n stops after n.toNat lowering
steps in any torsion-free Noetherian module.
The higher-string relation supplied by an sl₂-triple: if m has integral weight a for
h and is killed by f, then one bracket with e followed by (-a).toNat further adjoint
applications vanishes.
The end of the string #
The weight string of a primitive vector of weight n : ℕ has length n + 1: lowering past
step n gives zero. Mathlib's
IsSl2Triple.HasPrimitiveVectorWith.pow_toEnd_f_eq_zero_of_eq_nat is the first such step.
The weight string of a primitive vector of weight n : ℕ may be truncated to its n + 1
nonzero positions without changing its span: everything past step n is zero.
Linear independence of the string #
The n + 1 vectors of the weight string of a primitive vector of weight n are linearly
independent: fⁱ • m is a nonzero eigenvector of h for the eigenvalue n - 2i, and these
eigenvalues are distinct.
The ladder basis and the dimension of V(n) #
The weight string of a primitive vector of weight n in an irreducible module spans it, as a
family indexed by the n + 1 positions of the string.
The ladder basis. A module irreducible over the subalgebra of an sl₂ triple, with a
primitive vector m of weight n : ℕ, has the weight string m, f • m, …, fⁿ • m as a basis.
Equations
Instances For
The dimension of V(n). A Noetherian module irreducible over the subalgebra of an sl₂
triple, carrying a primitive vector of weight n, has rank n + 1.
On the ladder basis, h acts diagonally with the eigenvalues n, n - 2, …, -n.
On the ladder basis, f is the lowering operator, moving one step down the string.
The lowering operator kills the bottom of the ladder basis.
On the ladder basis, e is the raising operator, moving one step up the string with the
Casimir-type coefficient (i + 1)(n - i).
The raising operator kills the primitive vector at the top of the ladder basis.
The classification: the highest weight determines the module #
The highest weight determines the irreducible. Two modules irreducible over the subalgebra
of an sl₂ triple, each carrying a primitive vector of the same weight n, are equivalent as
modules over that subalgebra: the linear equivalence matching the two ladder bases position by
position intertwines the action of the triple, because the ladder relations depend only on n.
The conclusion is an equivalence over t.toLieSubalgebra K, not over the ambient L; outside the
subalgebra the two actions have nothing to do with one another.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The classifying equivalence carries the ladder basis to the ladder basis.
The classifying equivalence carries the weight string to the weight string, position by position and past the end of the string too.