The trace of a pair of opposite root vectors on a weight space #
Let H be a nilpotent Lie subalgebra of L acting on a module M that is finite and free over a
principal ideal domain K, let α : H → K be a linear form, and let x and y be root vectors of
weights α and -α whose bracket ⁅x, y⁆ lies in H, say ⁅x, y⁆ = z. Acting first by x and
then by y carries the χ-weight space of M back to itself; write Ado.raiseLowerEnd for
the resulting endomorphism. Given a rung N at which the space M_{χ + Nα} vanishes, this file
computes its trace:
tr_{Mχ}(y ∘ x) = Σ_{1 ≤ j < N} dim M_{χ + jα} · (χ + jα)(z).
Over a field of characteristic zero and for a nonzero α, the α-string above χ is finite, and
the same computation takes the unbounded shape Σ_{j ≥ 1} that Freudenthal's formula uses, indexed
by that string with its bottom rung removed.
The argument is a ladder, with no sl₂ representation theory and no complete reducibility. Acting
by x and by y gives maps Mχ → M_{α+χ} and M_{α+χ} → Mχ, and swapping the two factors of a
composite does not change its trace, so tr_{Mχ}(y ∘ x) = tr_{M_{α+χ}}(x ∘ y). On M_{α+χ} the
Leibniz identity gives x ∘ y - y ∘ x = z, and the trace of z there is dim M_{α+χ} · (α+χ)(z),
because z acts on a generalized weight space with the single generalized eigenvalue (α+χ)(z)
(LieModule.trace_toEnd_genWeightSpace). Together these give the step
tr_{Mχ}(y ∘ x) = tr_{M_{α+χ}}(y ∘ x) + dim M_{α+χ} · (α+χ)(z),
which telescopes down from a rung where the weight space is trivial: there raiseLowerEnd is
itself 0, so the ladder terminates and the rungs beyond it never enter the telescope. The
initial-segment formulation assumes such a vanishing rung explicitly. When K is a field of
characteristic zero and α is a nonzero linear form, the string leaves the weights of M
after finitely many steps;
TauCeti/Algebra/Lie/Weights/String.lean packages that finite index set as Ado.weightString.
The identity is the computational input to Freudenthal's multiplicity formula: taking x and
y to be the root vectors of an sl₂ triple attached to a positive root α, so that z = α^∨,
the right-hand side is 2 / ⟨α, α⟩ times the inner sum Σ_{j ≥ 1} m_{μ + jα} ⟨μ + jα, α⟩ of that
recursion, by the normalization ⟨λ, α^∨⟩⟨α, α⟩ = 2⟨λ, α⟩ of the invariant form.
Main definitions #
Ado.raiseLowerEnd: acting by a root vector of weightαand then by one of weight-α, as an endomorphism of theχ-weight space.
Main results #
Ado.trace_raiseLowerEnd_eq_trace_add_nsmul: the ladder step, expressing the trace atχin terms of the trace atα + χ.Ado.trace_raiseLowerEnd_eq_sum_Ico: the closed form, as a sum overFinset.Ico 1 Nfor a rungNat which theα-string aboveχhas a trivial weight space.Ado.trace_raiseLowerEnd_eq_sum_weightString_erase_zero: the same closed form, summed over theα-string aboveχwith its bottom index removed, which is the index set of the inner sum of Freudenthal's formula.
References #
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §22.3, where this trace computation is the lemma behind Freudenthal's formula.
- Highest-weight roadmap,
Layer 7, "Freudenthal's multiplicity formula", to be proved "from the Casimir eigenvalue and the
sl₂-string action of each⟨eₐ, hₐ, fₐ⟩on the weight spaces". The string action is what is computed here.
Acting by a root vector on a weight vector is the bracket. Mathlib states this elementwise
description only for the bundled rootSpaceWeightSpaceProduct, in
coe_rootSpaceWeightSpaceProduct_tmul, so the auxiliary bilinear map that this file uses is
unfolded once, here.
Acting by a root vector x of weight α and then by a root vector y of weight -α, as an
endomorphism of the χ-weight space of M.
Equations
- Ado.raiseLowerEnd M hx hy χ = (LieAlgebra.rootSpaceWeightSpaceProductAux K L H M ⋯) ⟨y, hy⟩ ∘ₗ (LieAlgebra.rootSpaceWeightSpaceProductAux K L H M ⋯) ⟨x, hx⟩
Instances For
raiseLowerEnd is the composite of the two root-vector actions, in that order.
raiseLowerEnd is the restriction to the χ-weight space of the composite of the two actions
on M, which is the shape in which a trace computation over a basis of L produces it.
On a trivial weight space the raise-lower endomorphism vanishes.
The ladder step. The trace of y ∘ x on the χ-weight space exceeds its trace on the
(α + χ)-weight space by dim M_{α+χ} · (α+χ)(z), where z = ⁅x, y⁆.
The closed form of the trace, as a sum over Finset.Ico 1 N, for any rung N at which the
α-string above χ has a trivial weight space. The ladder terminates there, so nothing beyond
that rung is assumed.
The closed form of the trace, summed over the α-string above χ with its bottom index
removed. This is the index set of the inner sum of Freudenthal's multiplicity formula.