The trace of the Casimir operator on a weight space #
Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over an algebraically
closed field of characteristic zero, let H be a splitting Cartan subalgebra, and let M be a
finite-dimensional L-module. The Casimir element Ω ∈ U(L) is central
(Ado.casimirElement_mem_center), so the operator it induces on M commutes with the action
and therefore preserves each weight space Mμ. This file computes the trace of its restriction:
tr_{Mμ}(Ω) = dim Mμ · ⟨μ, μ⟩
+ ∑_{α ∈ roots} ∑_{j ∈ weightString(M, α, μ) \ {0}} dim M_{μ + jα} · ⟨μ + jα, α⟩,
with ⟨·,·⟩ the invariant form Ado.invForm on Module.Dual K H and weightString(M, α, μ)
the α-string above μ of Ado.weightString, a Finset ℕ whose index j = 0 is the μ
rung itself.
The argument #
Ado.casimirElement_eq_sum evaluates Ω against any basis x of L and its Killing-dual
basis y, so the operator Ω acts as ∑ᵢ π(xᵢ) π(yᵢ). Inserting the root-space projections of
TauCeti/Algebra/Lie/Weights/Projection.lean into both slots and using that the χ- and
ψ-root spaces pair to zero under the Killing form unless χ + ψ = 0 leaves only the opposite
pairs (π_χ, π_{-χ}); this is Ado.sum_apply_killingDualBasis_eq_sum_weight, stated for an
arbitrary bilinear map so that both the operator identity here and the Casimir eigenvalue of
TauCeti/Algebra/Lie/HighestWeight/Casimir.lean are instances of it.
Each surviving summand acts by a vector of one root space followed by a vector of the opposite
root space, so it preserves Mμ and is a Ado.raiseLowerEnd of
TauCeti/Algebra/Lie/Weights/Trace.lean. The two kinds of summand are then read off:
- the summands at a zero weight are built from two elements of
H, which act onMμby the scalarsμgives them (the honest weight spaces ofTauCeti/Algebra/Lie/Weights/Diagonalizable.lean), so their traces sum todim Mμ · ⟨μ, μ⟩; - the summands at a root
αhave⁅x, y⁆ = κ(x, y) α^♯, and the coefficientsκ(x, y)sum to the trace1of a root-space projection, so the string formulaAdo.trace_raiseLowerEnd_eq_sum_weightString_erase_zeroturns their traces into∑_{j ∈ weightString(M, α, μ) \ {0}} dim M_{μ + jα} · ⟨μ + jα, α⟩.
Main definitions #
Ado.casimirGenWeightSpaceEnd: the Casimir operator ofM, restricted to a generalized weight space.
Main results #
Ado.sum_apply_killingDualBasis_eq_sum_weight: a sum along a basis and its Killing-dual basis splits along the opposite pairs of root-space projections.Ado.representation_casimirElement_eq_sum_weight: the Casimir operator ofM, split along the root spaces.Ado.representation_casimirElement_mem_genWeightSpace: the Casimir operator preserves every generalized weight space.Ado.casimirGenWeightSpaceEnd_eq_sum: the restriction to a weight space, as a sum of raise-lower endomorphisms.Ado.trace_casimirGenWeightSpaceEnd: the trace of the Casimir operator on a weight space.
References #
This is the Casimir half of the "Freudenthal's multiplicity recursion" item of Layer 7 of
TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md; the string half is
TauCeti/Algebra/Lie/Weights/Trace.lean. Combining the trace computed here with the Casimir
eigenvalue ⟨λ + ρ, λ + ρ⟩ - ⟨ρ, ρ⟩ of a highest weight module is what produces the recursion
itself.
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §22.3.
Splitting a Killing-dual-basis sum along the root spaces #
A Killing-dual-basis sum splits along the root spaces. For a bilinear map f, the sum
∑ᵢ f xᵢ yᵢ along a basis of L and its Killing-dual basis is the sum over the weights χ of
H on L of the same expression with π_χ inserted in the first slot and π_{-χ} in the
second. Only these opposite pairs survive, because the Killing form pairs the χ-root space with
the -χ-root space alone.
The Casimir operator, split along the root spaces. For any basis x of L and its
Killing-dual basis y, the operator by which the Casimir element acts on M is the sum over the
weights χ of H on L of ∑ᵢ π(π_χ xᵢ) π(π_{-χ} yᵢ).
Sums built from the extended weight #
The extension Ado.killingExtend of a weight to a linear form on L lives in
TauCeti/Algebra/Lie/Weights/InvariantForm.lean; the two sums below are the ones that need the
root-space projections and the Killing-dual basis as well.
The extension of a weight sees only the zero weight, so the products of its values on the root-space projections of two vectors telescope to the product of its values on the vectors.
The squared length of a weight, read along a Killing-dual pair of bases. The extension of
lam is the pairing with the vector representing lam, so expanding that vector in the basis
gives ⟨lam, lam⟩.
The Casimir operator on a weight space #
The Casimir operator preserves every generalized weight space. It commutes with the Lie
action (Ado.representation_casimirElement_lie), hence with every power of
toEnd x - mu x.
The Casimir operator of a weight space: the operator by which the Casimir element acts on
M, restricted to the generalized mu-weight space, which it preserves.
Equations
Instances For
The Casimir operator of a weight space is the restriction of the Casimir operator of M.
The Casimir operator of a weight space, split along the root spaces. Each summand raises
by a vector of the χ-root space and lowers by one of the -χ-root space, so it is a
Ado.raiseLowerEnd.
The two kinds of summand #
The zero-weight summands are scalars. A raise-lower endomorphism built from two elements
of the Cartan subalgebra acts on the mu-weight space by the scalar mu gives them, because the
weight spaces are honest simultaneous eigenspaces.
The summands at a root sum to a string sum. Each summand at the root chi lowers and
raises by root vectors whose bracket is a multiple of the vector representing chi, so the string
formula applies; the multiples sum to the trace 1 of a root-space projection.
The trace #
The trace of the Casimir operator on a weight space. For a finite-dimensional module M
over a Killing-semisimple Lie algebra and a linear form mu on the Cartan subalgebra, the trace
of the Casimir operator on the mu-weight space of M is
dim M_mu ⟨mu, mu⟩ + ∑_{α ∈ roots} ∑_{j ∈ weightString(M, α, mu) \ {0}} dim M_{mu + jα} ⟨mu + jα, α⟩.
The inner sums run over the α-string above mu (Ado.weightString, a Finset ℕ) with the
mu rung j = 0 removed, which is where the terms with a zero weight space are already absent.