The Casimir eigenvalue on a highest weight module #
Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over a field of
characteristic zero, H a splitting Cartan subalgebra, and base a base of its root system. The
Casimir element Ω = ∑ᵢ xᵢ yᵢ ∈ U(L) is central (Ado.casimirElement_mem_center), so it acts
on any module by a module endomorphism. This file computes that endomorphism on a highest weight
module: on a module generated by a highest weight vector of weight λ, the Casimir element acts
by the scalar
⟨λ + ρ, λ + ρ⟩ - ⟨ρ, ρ⟩,
where ⟨·,·⟩ is Ado.invForm and ρ is Ado.weylVector.
The computation is the classical one. Because Ado.casimirElement_eq_sum evaluates Ω
against an arbitrary basis, the sum ∑ᵢ ⁅xᵢ, ⁅yᵢ, v⁆⁆ can be split along the root-space
decomposition of L using the projections Ado.genWeightSpaceProjection. Since the χ- and
ψ-root spaces pair to zero under the Killing form unless χ + ψ = 0, only the opposite pairs
(π_χ, π_{-χ}) survive, and the resulting sum over the weights of H on L splits in three:
- the zero weight contributes
⟨λ, λ⟩, becauseHacts onvthroughλ; - a negative root
χcontributes nothing, becauseπ_{-χ} yᵢlies inn⁺and killsv; - a positive root
χcontributes⟨λ, χ⟩, because⁅π_χ xᵢ, v⁆ = 0turns the term into⁅⁅π_χ xᵢ, π_{-χ} yᵢ⁆, v⁆, the bracket isκ (π_χ xᵢ) (π_{-χ} yᵢ)times the vector representingχ, and those coefficients sum to the trace1ofπ_χ.
Summing gives ⟨λ, λ⟩ + ∑_{α > 0} ⟨λ, α⟩, which is ⟨λ + ρ, λ + ρ⟩ - ⟨ρ, ρ⟩ because the cross
terms of the square contribute 2⟨λ, ρ⟩ = ⟨λ, 2ρ⟩, the pairing of λ with the sum of the positive
roots.
Cyclicity, not irreducibility, is the right hypothesis for the statement about the whole module:
the scalar statement holds for every highest weight module, since the kernel of Ω - c is a Lie
submodule by centrality and it contains the generator.
Main results #
Ado.casimirScalar: the Casimir eigenvalue attached to a highest weight.Ado.casimirScalar_def: its defining formula⟨λ + ρ, λ + ρ⟩ - ⟨ρ, ρ⟩.Ado.casimir_smul_of_isHighestWeightVector: the Casimir element sends a highest weight vector of weightλtocasimirScalar base λ • v.Ado.casimir_smul_of_isHighestWeightVector_of_lieSpan_eq_top: on a highest weight module the Casimir element acts by that scalar on every vector.Ado.casimirScalar_eq_add_sum: the scalar expanded as⟨λ, λ⟩ + ∑_{α > 0} ⟨λ, α⟩, the shape in which its sign is read off.Ado.casimirScalar_zero: the scalar of the zero weight is0.Ado.casimirScalar_sub_casimirScalar: the difference of two scalars,c(λ) - c(μ) = (⟨λ, λ⟩ - ⟨μ, μ⟩) + ⟨2ρ, λ - μ⟩.Ado.casimirScalar_add_sub_casimirScalar: the scalar along a translation,c(χ + σ) - c(χ) = 2⟨χ + σ, σ⟩ - c(-σ).
Implementation notes #
The module M is not assumed finite-dimensional: only L is, which is all the basis and the
Killing-dual basis need. The U(L)-action is the algebra homomorphism
Ado.UniversalEnvelopingAlgebra.representation, that is,
UniversalEnvelopingAlgebra.lift K (LieModule.toEnd K L M).
The weight λ is extended from H to a linear form on the whole of L by pairing with the vector
representing it under the Killing form (Ado.killingExtend). That extension agrees with
λ on H and vanishes on every root space, which is what lets the zero-weight term be summed
without a case distinction on whether the zero functional is a weight at all.
References #
This is the "Casimir element" item of Layer 5 of
TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md, whose target signature
casimir_smul_of_isHighestWeightVector is pinned in the accompanying Suggested.lean. The
unadorned name goes to the statement on the generator, from which the statement on the whole
module, casimir_smul_of_isHighestWeightVector_of_lieSpan_eq_top, follows by adding the
cyclicity hypothesis its name records.
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §22.1, where
the Casimir element is shown to act on a standard cyclic module of highest weight
λby the scalar⟨λ, λ + 2ρ⟩; the Casimir element itself is §6.2.
The bilinear map through which the Casimir element acts #
The three kinds of term #
The Casimir eigenvalue #
The Casimir scalar of a highest weight. This is the scalar by which the Casimir element
acts on a highest weight module of weight lam.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The defining formula of the Casimir scalar: the difference of the squared lengths of
lam + ρ and of ρ. The definition is sealed, so this is the equation through which the scalar
is unfolded, here and downstream.
The Casimir scalar of the zero weight vanishes: it is ⟨ρ, ρ⟩ - ⟨ρ, ρ⟩. This is the
scalar by which the Casimir element acts on the trivial module.
The Casimir scalar, expanded. The scalar is ⟨lam, lam⟩ plus the sum of the pairings of
lam with the positive roots, the cross terms of the square contributing
2⟨lam, ρ⟩ = ⟨lam, 2ρ⟩.
The difference of two Casimir scalars, split into a quadratic part and a root part:
c(lam) - c(mu) = (⟨lam, lam⟩ - ⟨mu, mu⟩) + ⟨2ρ, lam - mu⟩.
The Casimir scalar along a translation:
c(χ + σ) - c(χ) = 2⟨χ + σ, σ⟩ - c(-σ).
The Casimir eigenvalue on a highest weight vector. The Casimir element sends a highest
weight vector of weight lam to casimirScalar base lam • v.
The Casimir eigenvalue on a highest weight module. On a module generated by a highest
weight vector of weight lam, the Casimir element acts by the scalar
⟨lam + ρ, lam + ρ⟩ - ⟨ρ, ρ⟩. Centrality of the Casimir element makes the set where it acts by
that scalar a Lie submodule, and it contains the generator.