The α-string of weights above a weight

Let M be a finite-dimensional module over a nilpotent Lie algebra H -- in practice a Cartan subalgebra -- and let μ and α be linear forms on H. The α-string above μ is the set of j for which μ + j • α is a weight of M. Because M has only finitely many weights and, for α ≠ 0, the forms μ + j • α are pairwise distinct, the string is finite: this is the statement that makes the inner sum of Freudenthal's multiplicity recursion a sum over a Finset.

This file proves that finiteness, packages the string as Ado.weightString, records the resulting uniform bound (μ + j • α is not a weight once j is large), and computes the string in the degenerate direction α = 0, where it is all of ℕ as soon as μ is a weight.

Main definitions

• Ado.weightString M hα μ: the α-string above μ, as a Finset ℕ.

Main results

• Ado.finite_setOf_genWeightSpace_add_nsmul_ne_bot: for α ≠ 0 the α-string above μ is finite. This is the finiteness the Freudenthal recursion's inner sum rests on.
• Ado.exists_genWeightSpace_add_nsmul_eq_bot_of_le: the string terminates -- past some N, no μ + j • α is a weight.
• Ado.sum_finrank_genWeightSpace_weightString_le: the multiplicities along the string add up to at most Module.finrank K M, because distinct members of the string are distinct weights and the weight spaces of M are independent.
• Ado.weightString_congr: the string is an isomorphism invariant of the Lie module.
• Ado.sum_weightString_eq_sum_of_subset: a sum over the string may be replaced by a sum over any finite superset of it, the form in which a Freudenthal-style double sum is manipulated.

Implementation notes

The string is indexed by j : ℕ and the displacement is the ℕ-scalar multiple j • α in Module.Dual K H; Nat.cast_smul_eq_nsmul converts to the (j : K) • α spelling where a computation in the base field is wanted.

The index j = 0 is included: 0 ∈ weightString M hα μ exactly when μ itself is a weight, so weightString is the whole α-string above μ and mem_weightString_iff characterises membership with no side condition on j. Freudenthal's inner sum runs over j ≥ 1 instead, i.e. over (weightString M hα μ).erase 0; being a subset of the string, that index set is finite for the same reason, which is the finiteness this file supplies. Restricting the definition itself to j ≥ 1 would lose the j = 0 term, which is the multiplicity mult_μ standing on the left of the recursion, and would make every statement below carry a 0 < j hypothesis.

Ado.weightString carries the hypothesis α ≠ 0 as an explicit argument rather than choosing a junk value, because the α = 0 case is genuinely infinite (whenever μ is a weight) rather than merely uninteresting; Ado.infinite_setOf_genWeightSpace_add_nsmul_zero_ne_bot records that degenerate case separately.

References

• 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, where the finiteness of the string is what makes the multiplicity recursion effective.
• Highest-weight roadmap, Layer 7, whose freudenthalRHS is pinned with the note that "the inner sum over j ≥ 1 is finite because μ + j • α leaves the (finite) weight set for large j, so it ranges over a finite Finset". That finiteness is what this file supplies.

theorem Ado.injective_add_nsmul {K : Type u} {H : Type v} [Field K] [CharZero K] [AddCommMonoid H] [Module K H] {alpha : Module.Dual K H} (halpha : alpha ≠ 0) (mu : Module.Dual K H) : Function.Injective fun (j : ℕ) => ⇑(mu + j • alpha)

Translating μ by the multiples of a nonzero α gives pairwise distinct linear forms. Only the K-module structure of H is involved, so no Lie bracket is assumed here.

theorem Ado.finite_setOf_genWeightSpace_add_nsmul_ne_bot {K : Type u} {H : Type v} (M : Type w) [Field K] [CharZero K] [LieRing H] [LieAlgebra K H] [LieRing.IsNilpotent H] [AddCommGroup M] [Module K M] [LieRingModule H M] [LieModule K H M] [FiniteDimensional K M] {alpha : Module.Dual K H} (halpha : alpha ≠ 0) (mu : Module.Dual K H) : {j : ℕ | LieModule.genWeightSpace M ⇑(mu + j • alpha) ≠ ⊥}.Finite

The α-string above μ is finite for α ≠ 0: the forms μ + j • α are pairwise distinct, and a finite-dimensional module has only finitely many weights.

noncomputable def Ado.weightString {K : Type u} {H : Type v} (M : Type w) [Field K] [CharZero K] [LieRing H] [LieAlgebra K H] [LieRing.IsNilpotent H] [AddCommGroup M] [Module K M] [LieRingModule H M] [LieModule K H M] [FiniteDimensional K M] {alpha : Module.Dual K H} (halpha : alpha ≠ 0) (mu : Module.Dual K H) : Finset ℕ

The α-string above μ: the j : ℕ for which μ + j • α is a weight of M. The hypothesis α ≠ 0 is what makes the string finite. The index j = 0 is included, so this is the full string; the j ≥ 1 index set of Freudenthal's inner sum is the subset (weightString M halpha mu).erase 0.

Equations

• Ado.weightString M halpha mu = ⋯.toFinset

@[simp]

theorem Ado.mem_weightString_iff {K : Type u} {H : Type v} {M : Type w} [Field K] [CharZero K] [LieRing H] [LieAlgebra K H] [LieRing.IsNilpotent H] [AddCommGroup M] [Module K M] [LieRingModule H M] [LieModule K H M] [FiniteDimensional K M] {alpha : Module.Dual K H} (halpha : alpha ≠ 0) (mu : Module.Dual K H) {j : ℕ} : j ∈ weightString M halpha mu ↔ LieModule.genWeightSpace M ⇑(mu + j • alpha) ≠ ⊥

theorem Ado.mem_weightString_iff_formalCharacter_coeff_ne_zero {K : Type u} {H : Type v} {M : Type w} [Field K] [CharZero K] [LieRing H] [LieAlgebra K H] [LieRing.IsNilpotent H] [AddCommGroup M] [Module K M] [LieRingModule H M] [LieModule K H M] [FiniteDimensional K M] [LieModule.LinearWeights K H M] {alpha : Module.Dual K H} (halpha : alpha ≠ 0) (mu : Module.Dual K H) {j : ℕ} : j ∈ weightString M halpha mu ↔ (formalCharacter K H M).coeff (mu + j • alpha) ≠ 0

Membership in the string, read off the formal character.

theorem Ado.weightString_congr {K : Type u} {H : Type v} {M : Type w} [Field K] [CharZero K] [LieRing H] [LieAlgebra K H] [LieRing.IsNilpotent H] [AddCommGroup M] [Module K M] [LieRingModule H M] [LieModule K H M] [FiniteDimensional K M] {N : Type w₁} [AddCommGroup N] [Module K N] [LieRingModule H N] [LieModule K H N] [FiniteDimensional K N] (e : M ≃ₗ⁅K,H⁆ N) {alpha : Module.Dual K H} (halpha : alpha ≠ 0) (mu : Module.Dual K H) : weightString M halpha mu = weightString N halpha mu

The string is an isomorphism invariant: an equivalence of Lie modules carries the χ-weight space of one onto the χ-weight space of the other, so the two modules have the same α-string above any μ.

theorem Ado.exists_genWeightSpace_add_nsmul_eq_bot_of_le {K : Type u} {H : Type v} {M : Type w} [Field K] [CharZero K] [LieRing H] [LieAlgebra K H] [LieRing.IsNilpotent H] [AddCommGroup M] [Module K M] [LieRingModule H M] [LieModule K H M] [FiniteDimensional K M] {alpha : Module.Dual K H} (halpha : alpha ≠ 0) (mu : Module.Dual K H) : ∃ (N : ℕ), ∀ (j : ℕ), N ≤ j → LieModule.genWeightSpace M ⇑(mu + j • alpha) = ⊥

The string terminates: past some N, no μ + j • α is a weight. This is the bound that turns the Freudenthal inner sum into a finite one.

theorem Ado.weightString_subset_range {K : Type u} {H : Type v} {M : Type w} [Field K] [CharZero K] [LieRing H] [LieAlgebra K H] [LieRing.IsNilpotent H] [AddCommGroup M] [Module K M] [LieRingModule H M] [LieModule K H M] [FiniteDimensional K M] {alpha : Module.Dual K H} (halpha : alpha ≠ 0) (mu : Module.Dual K H) : weightString M halpha mu ⊆ Finset.range ((weightString M halpha mu).sup id + 1)

The string is contained in an initial segment of ℕ.

theorem Ado.weightString_eq_empty_iff {K : Type u} {H : Type v} {M : Type w} [Field K] [CharZero K] [LieRing H] [LieAlgebra K H] [LieRing.IsNilpotent H] [AddCommGroup M] [Module K M] [LieRingModule H M] [LieModule K H M] [FiniteDimensional K M] {alpha : Module.Dual K H} (halpha : alpha ≠ 0) (mu : Module.Dual K H) : weightString M halpha mu = ∅ ↔ ∀ (j : ℕ), LieModule.genWeightSpace M ⇑(mu + j • alpha) = ⊥

The string is empty exactly when no translate of μ by a multiple of α is a weight.

theorem Ado.sum_finrank_genWeightSpace_weightString_le {K : Type u} {H : Type v} {M : Type w} [Field K] [CharZero K] [LieRing H] [LieAlgebra K H] [LieRing.IsNilpotent H] [AddCommGroup M] [Module K M] [LieRingModule H M] [LieModule K H M] [FiniteDimensional K M] {alpha : Module.Dual K H} (halpha : alpha ≠ 0) (mu : Module.Dual K H) : ∑ j ∈ weightString M halpha mu, ↑(Module.finrank K ↥(LieModule.genWeightSpace M ⇑(mu + j • alpha))) ≤ ↑(Module.finrank K M)

The multiplicities along the string add up to at most the dimension of M. The forms μ + j • α for j in the string are pairwise distinct, so the corresponding weight spaces are an independent family of subspaces of M; their span therefore has the sum of their dimensions, and that span sits inside M.

theorem Ado.sum_weightString_eq_sum_of_subset {K : Type u} {H : Type v} {M : Type w} [Field K] [CharZero K] [LieRing H] [LieAlgebra K H] [LieRing.IsNilpotent H] [AddCommGroup M] [Module K M] [LieRingModule H M] [LieModule K H M] [FiniteDimensional K M] {A : Type u_1} [AddCommMonoid A] {alpha : Module.Dual K H} (halpha : alpha ≠ 0) (mu : Module.Dual K H) (f : ℕ → A) {s : Finset ℕ} (hs : weightString M halpha mu ⊆ s) (hf : ∀ j ∈ s, LieModule.genWeightSpace M ⇑(mu + j • alpha) = ⊥ → f j = 0) : ∑ j ∈ weightString M halpha mu, f j = ∑ j ∈ s, f j

A sum over the string is a sum over any finite superset of it, the terms off the string vanishing. This is how a Freudenthal-style double sum is compared with a sum over a common index set.

theorem Ado.infinite_setOf_genWeightSpace_add_nsmul_zero_ne_bot {K : Type u} {H : Type v} {M : Type w} [Field K] [LieRing H] [LieAlgebra K H] [LieRing.IsNilpotent H] [AddCommGroup M] [Module K M] [LieRingModule H M] [LieModule K H M] (mu : Module.Dual K H) (h : LieModule.genWeightSpace M ⇑mu ≠ ⊥) : {j : ℕ | LieModule.genWeightSpace M ⇑(mu + j • 0) ≠ ⊥}.Infinite

The hypothesis α ≠ 0 cannot be dropped: in the degenerate direction α = 0 every j translates μ to itself, so the string above a weight is all of ℕ.