Freudenthal's multiplicity recursion #
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 Cartan subalgebra, b a base of its root
system, and let M be a finite-dimensional module generated by a highest weight vector of weight
λ. Freudenthal's formula computes the multiplicity of a weight μ of M from the
multiplicities lying above it along the positive root directions:
(⟨λ + ρ, λ + ρ⟩ - ⟨μ + ρ, μ + ρ⟩) · dim Mμ
= 2 ∑_{α > 0} ∑_{j ≥ 1} dim M_{μ + jα} · ⟨μ + jα, α⟩,
with ⟨·,·⟩ the invariant form TauCeti.invForm and ρ the Weyl vector TauCeti.weylVector.
The anchor at the top weight, dim Mλ = 1, is
TauCeti.formalCharacter_coeff_eq_one_of_isHighestWeightVector_of_lieSpan_eq_top. Reading the
formula downwards from there as a computation of the lower multiplicities needs one more
ingredient, namely that the scalar on the left is nonzero at every weight strictly below λ;
that nonvanishing is a separate prerequisite, and is not proved here.
The two halves #
The Casimir element Ω is central and M is generated by a highest weight vector, so Ω acts on
all of M by the single scalar ⟨λ + ρ, λ + ρ⟩ - ⟨ρ, ρ⟩
(TauCeti.casimir_smul_of_isHighestWeightVector_of_lieSpan_eq_top); its trace on Mμ is
therefore dim Mμ times that scalar. On the other hand TauCeti.trace_casimirGenWeightSpaceEnd
computes the same trace as
dim Mμ · ⟨μ, μ⟩ + ∑_{α ∈ roots} ∑_{j ≥ 1} dim M_{μ + jα} · ⟨μ + jα, α⟩,
the inner sums running over the α-string above μ (TauCeti.weightString). Equating the two is
already the recursion, except that its right-hand side runs over all roots rather than the
positive ones.
Passing from all roots to the positive ones is the second half, and it is
TauCeti.sum_weightString_neg_eq_add: the string sum in the direction -α exceeds the one in the
direction α by the single term dim Mμ · ⟨μ, α⟩. That comparison is the reflection symmetry of
the multiplicities (TauCeti.finrank_weightSpace_neg_sub_zsmul_add, proved directly from the
rank-one theory) read along the whole two-sided string: the summand at the rung i and the
summand at the reflected rung -i - ⟨μ, α^∨⟩ are negatives of one another, so the sum over the
two-sided string vanishes, and splitting that vanishing sum at the rung i = 0 — whose term is
dim Mμ · ⟨μ, α⟩ — is the comparison. Summing it over the positive roots turns ∑_{α ∈ roots}
into 2 ∑_{α > 0} at the cost of dim Mμ · ∑_{α > 0} ⟨μ, α⟩, which
TauCeti.casimirScalar_eq_add_sum recognises as the Casimir scalar of μ itself; that is where
the ⟨μ + ρ, μ + ρ⟩ of the statement comes from.
Main results #
TauCeti.sum_weightString_neg_eq_add: the two directions of a root string differ by the summand at the foot of the string, the reflection symmetry in the form the recursion consumes.TauCeti.freudenthal_multiplicity_formula: Freudenthal's multiplicity recursion for a finite-dimensional highest weight module.
Implementation notes #
Multiplicities are Module.finrank K (LieModule.genWeightSpace M μ) cast into K; the formal
character records the same numbers, by TauCeti.formalCharacter_coeff.
The hypothesis on M is cyclicity, not irreducibility: everything rests on the Casimir element
acting by a single scalar, which holds on any module generated by a highest weight vector. In
particular it applies to a finite-dimensional TauCeti.irreducibleQuotient.
References #
This is the "Freudenthal's multiplicity formula" item of Layer 7 of
TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md, whose target signature
freudenthal_multiplicity_formula is pinned in the accompanying Suggested.lean, with the
Freudenthal double sum packaged opaquely there "so the recursion is expressible before the
positive-root sum machinery is in place"; that machinery is in place, so the sum is written out.
- H. Freudenthal, Zur Berechnung der Charaktere der halbeinfachen Lieschen Gruppen I, Indag. Math. 16 (1954), 369--376.
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §22.3.
The two-sided root string #
A Freudenthal string sum telescopes along its own direction: after erasing the zeroth rung, the
sum above μ is the first summand at μ + β plus the corresponding sum above μ + β, also with
its zeroth rung erased.
The two directions of a root string differ by the summand at its foot. For a root α of
the Cartan subalgebra H and any linear form μ on H, the Freudenthal string sum in the
direction -α exceeds the one in the direction α by dim Mμ · ⟨μ, α⟩.
This is the reflection symmetry of the weight multiplicities
(TauCeti.finrank_weightSpace_neg_sub_zsmul_add) read along the whole two-sided string: the
summands cancel in reflected pairs, so their total vanishes, and splitting that total at the rung
μ itself leaves the stated comparison. It is what turns the sum over all roots in the trace of
the Casimir operator into twice the sum over the positive roots.
The recursion #
Freudenthal's multiplicity formula. Let M be a finite-dimensional module generated by a
highest weight vector of weight λ. Then for every linear form μ on the Cartan subalgebra,
(⟨λ + ρ, λ + ρ⟩ - ⟨μ + ρ, μ + ρ⟩) · dim Mμ = 2 ∑_{α > 0} ∑_{j ≥ 1} dim M_{μ + jα} · ⟨μ + jα, α⟩,
the inner sum running over the α-string above μ with the rung μ itself removed.
Together with dim Mλ = 1 at the top weight this is the recursion for the multiplicities below
λ. Running it as a downward computation of dim Mμ needs in addition that the scalar on the
left is nonzero there, which is not proved here.