Separation by the Casimir scalar #
Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over a field of
characteristic zero, let H be a splitting Cartan subalgebra and let base be a base of its root
system. TauCeti/Algebra/Lie/HighestWeight/Casimir.lean computes the scalar by which the Casimir
element Ω acts on a highest weight module of weight lam, namely
c(lam) = ⟨lam + ρ, lam + ρ⟩ - ⟨ρ, ρ⟩.
This file proves the two nonvanishing statements that make that scalar separate things. The second
of them additionally assumes that K is algebraically closed, because it compares the weights of a
module with each other.
The first is separation from the trivial module: c(lam) is nonzero as soon as lam is a
nonzero dominant integral weight (Ado.casimirScalar_ne_zero), while Ω acts by zero on a
module with trivial action
(Ado.representation_casimirElement_apply_eq_zero_of_isTrivial). Applying this to every
nontrivial finite-dimensional irreducible additionally requires the theorem that an irreducible
highest-weight module of highest weight zero is trivial; that theorem is not proved here.
The second is separation of the weights of one module, and here K is algebraically closed: on
a finite-dimensional module generated by a highest weight vector of weight lam, the scalars
c(mu) attached to the weights mu of the module are all different from c(lam) except at
mu = lam itself
(Ado.casimirScalar_ne_casimirScalar_of_genWeightSpace_ne_bot_of_isHighestWeightVector). This
is what turns Ado.freudenthal_multiplicity_formula into a downward computation of the weight
multiplicities: the coefficient that recursion divides by is
⟨lam + ρ, lam + ρ⟩ - ⟨mu + ρ, mu + ρ⟩ = c(lam) - c(mu).
The argument #
Expanding the square, c(lam) = ⟨lam, lam⟩ + ∑_{α > 0} ⟨lam, α⟩
(Ado.casimirScalar_eq_add_sum), and the summands are read off by the
positivity of TauCeti/Algebra/Lie/Weights/Positivity.lean. A dominant integral weight is integral
(Ado.IsDominantIntegral.isIntegralWeight, the passage from the simple coroots to all of them
going through Ado.IsDominantIntegral.exists_nat_apply_coroot and, for a negative root, the
sign change LieAlgebra.IsKilling.coroot_neg), so ⟨lam, lam⟩ is a positive rational when
lam ≠ 0. And ⟨lam, α⟩ = ⟨α, α⟩ lam(α^∨) / 2 is a nonnegative rational for a positive root α,
the root length being positive and lam(α^∨) a natural number by dominance. A positive rational
plus nonnegative rationals is nonzero, and a nonzero rational stays nonzero in a field of
characteristic zero. That is the first statement.
Dominance is essential, not decoration: for a general integral lam the two summands can have
opposite signs and c(lam) can vanish. For example, lam = -2ρ is integral and satisfies
lam + ρ = -ρ, hence c(lam) = 0.
The same expansion turns the difference into
c(lam) - c(mu) = (⟨lam, lam⟩ - ⟨mu, mu⟩) + ⟨2ρ, lam - mu⟩. The weights of a highest weight
module lie in lam - Q⁺, so lam - mu is a nonzero member of the positive root cone when
mu ≠ lam, and the second summand is a positive rational: 2ρ pairs with a simple root αᵢ in
⟨αᵢ, αᵢ⟩, a positive rational, because 2ρ(αᵢ^∨) = 2. The first summand is where dominance of
mu would be needed and is not available, so mu is replaced by a dominant conjugate: the weights
of a finite-dimensional module are Weyl stable and integral, so mu has a Weyl translate
nu = w · mu that is again a weight of the module and is dominant integral, by
Ado.exists_weylGroup_smul_isDominantIntegral_of_genWeightSpace_ne_bot of
TauCeti/Algebra/Lie/HighestWeight/Weight/Support.lean. The form is Weyl
invariant (RootPairing.InvariantForm.apply_weylGroup_smul), so
⟨mu, mu⟩ = ⟨nu, nu⟩ and the first summand is
⟨lam + nu, lam - nu⟩, which is nonnegative: lam + nu is dominant integral and lam - nu lies
in the cone. A nonnegative rational plus a positive one is nonzero.
Main results #
Ado.casimirScalar_ne_zeroandAdo.casimirScalar_eq_zero_iff: the Casimir scalar of a dominant integral weight vanishes exactly at the zero weight.Ado.casimir_apply_ne_zero_of_isHighestWeightVector_of_lieSpan_eq_top: on a highest weight module with nonzero dominant integral highest weight, the Casimir element kills no nonzero vector.Ado.representation_casimirElement_apply_eq_zero_of_isTrivial: on a module with trivial action the Casimir element acts by zero.Ado.IsDominantIntegral.exists_nonneg_rat_invForm_of_mem_posRootCone: a dominant integral weight pairs to a nonnegative rational with every member of the positive root cone.casimirScalar_ne_casimirScalar_of_isDominantIntegral_of_sub_mem_posRootCone_of_ne(in theAdo.IsDominantIntegralnamespace): the Casimir scalar separates a dominant integral weight from the dominant integral weights strictly below it.Ado.casimirScalar_ne_casimirScalar_of_genWeightSpace_ne_bot_of_isHighestWeightVector: over an algebraically closed field, the Casimir scalar of a weight of a finite-dimensional highest weight module differs from that of the highest weight, except at the highest weight itself.
References #
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §6.3, where
the separation is the engine of Weyl's theorem, and §13.4 and §22.3, where the comparison of
⟨lam + ρ, lam + ρ⟩with⟨mu + ρ, mu + ρ⟩is the input of Freudenthal's recursion.
This is the "the eigenvalue separates the trivial module from nontrivial irreducibles" step of
Layer 5 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md, together with the
nonvanishing that Layer 7's "Freudenthal's multiplicity formula" needs to be read as a recursion.
The Casimir scalar of a dominant integral weight #
A dominant integral weight pairs nonnegatively with a positive root. The normalisation
⟨lam, α⟩ = ⟨α, α⟩ lam(α^∨) / 2 has a positive root length and, by dominance, a natural value
lam(α^∨).
The Casimir scalar of a nonzero dominant integral weight is nonzero. Expanded, the scalar
is ⟨lam, lam⟩ + ∑_{α > 0} ⟨lam, α⟩: a positive rational plus a sum of nonnegative rationals.
This distinguishes such a highest-weight module from a trivial module, whose Casimir scalar is
0.
The Casimir scalar of a dominant integral weight vanishes exactly at the zero weight. The
converse direction is the computation ⟨ρ, ρ⟩ - ⟨ρ, ρ⟩ = 0.
Separation on modules #
The Casimir element kills no nonzero vector of a highest weight module whose highest weight
is a nonzero dominant integral weight. It acts by the scalar of
Ado.casimir_smul_of_isHighestWeightVector_of_lieSpan_eq_top, which
Ado.casimirScalar_ne_zero shows to be nonzero.
Pairings with the positive root cone #
A dominant integral weight pairs nonnegatively with the positive root cone. A member of
the cone is a natural combination of the simple roots, and a dominant integral weight pairs
nonnegatively with each of those by
Ado.IsDominantIntegral.exists_nonneg_rat_invForm_root.
Separating dominant integral weights #
The Casimir scalar separates a dominant integral weight from the dominant integral weights
below it: if lam and nu are dominant integral, lam - nu lies in the positive root cone and
nu ≠ lam, then c(lam) ≠ c(nu).
In the expansion c(lam) - c(nu) = ⟨lam + nu, lam - nu⟩ + ⟨2ρ, lam - nu⟩ the first summand is a
nonnegative rational, lam + nu being dominant integral, and the second a positive one, lam - nu
being a nonzero member of the cone.
Separating the weights of a highest weight module #
The Casimir scalar separates the highest weight of a highest weight module from its other
weights: over an algebraically closed field, on a finite-dimensional module generated by a
highest weight vector of weight lam, the scalar ⟨mu + ρ, mu + ρ⟩ attached to a weight
mu ≠ lam differs from ⟨lam + ρ, lam + ρ⟩.
This is what turns Ado.freudenthal_multiplicity_formula into a downward computation of the
weight multiplicities of M: the coefficient the recursion divides by,
⟨lam + ρ, lam + ρ⟩ - ⟨mu + ρ, mu + ρ⟩, is casimirScalar base lam - casimirScalar base mu, and
is nonzero at every weight other than lam itself.
Expanded, the difference is (⟨lam, lam⟩ - ⟨mu, mu⟩) + ⟨2ρ, lam - mu⟩. The second summand is
positive because lam - mu is a nonzero member of the positive root cone. For the first, replace
mu by the dominant integral conjugate nu = w · mu of
Ado.exists_weylGroup_smul_isDominantIntegral_of_genWeightSpace_ne_bot, which has the same
length by RootPairing.InvariantForm.apply_weylGroup_smul; then
⟨lam, lam⟩ - ⟨nu, nu⟩ = ⟨lam + nu, lam - nu⟩ is
nonnegative, lam + nu being dominant integral and lam - nu a member of the cone.