The formal character of a finite-dimensional Lie module

Let L be a nilpotent Lie algebra over a field K acting on a finite-dimensional module M with linear weights. The formal character of M is the multiplicity function χ ↦ dim Mχ, recorded as an element of the integral group algebra ℤ[Module.Dual K L] of the dual of L: it is the generating function of the weight-space dimensions, and the object in which the Weyl character formula is an identity.

The multiplicities are Mathlib's generalized weight spaces LieModule.genWeightSpace. Over an algebraically closed field of characteristic zero, for the Cartan subalgebra of a Killing-semisimple Lie algebra, these are honest simultaneous eigenspaces (Ado.genWeightSpace_eq_weightSpace), so the coefficients really are the honest weight multiplicities; that identification is recorded below rather than built into the definition, which needs no semisimplicity.

The group algebra as the carrier

The carrier is AddMonoidAlgebra ℤ (Module.Dual K L), the group algebra of the whole dual rather than of the weight lattice. Nothing is lost: for a module over a Killing-semisimple Lie algebra every coefficient of the character sits at an integral weight (Ado.isIntegralWeight_of_formalCharacter_coeff_ne_zero), so the character lands in the lattice part of the larger algebra. The convolution product of that algebra is what makes multiplicativity on tensor products expressible.

Main definitions

• Ado.formalCharacter: the formal character χ ↦ dim Mχ of a finite-dimensional module.

Main results

• Ado.formalCharacter_coeff: its coefficients are the weight-space dimensions.
• Ado.formalCharacter_congr: isomorphic modules have the same formal character.
• Ado.sum_formalCharacter_coeff_eq_finrank: when M is triangularizable, the coefficients sum to dim M, and Ado.formalCharacter_eq_zero_iff reads off that the character vanishes only for the zero module.
• Ado.formalCharacter_prod: additivity. The character of a product of modules is the sum of their characters. Its weight-theoretic input is Ado.mem_genWeightSpace_prod_iff, that a vector lies in a generalized weight space of a product exactly when both components lie in the corresponding generalized weight spaces, with Ado.genWeightSpace_prod_eq_bot_iff and Ado.instLinearWeightsProd the consequences a product of modules needs to have a character at all.
• Ado.formalCharacter_eq_sum_of_isInternal: additivity over an internal decomposition. The character of a module decomposed internally by finitely many Lie submodules is the sum of their characters, the character being read on a nilpotent Lie subalgebra of the acting algebra.
• Ado.formalCharacter_eq_add_of_exact: additivity on short exact sequences. The character of the middle module is the sum of the characters of the submodule and quotient.
• Ado.finrank_genWeightSpace_tensorProduct: the multiplicity of a tensor-product weight is the convolution of the multiplicities in the two factors.
• Ado.formalCharacter_tensor: multiplicativity. The character of a tensor product is the product of the characters.
• Ado.formalCharacter_coeff_eq_finrank_weightSpace: over an algebraically closed field of characteristic zero, for a Cartan subalgebra of a Killing-semisimple Lie algebra, the coefficients are the honest weight multiplicities.
• Ado.isIntegralWeight_of_formalCharacter_coeff_ne_zero: the character is supported on integral weights.
• Ado.formalCharacter_coeff_weylGroup_smul: Weyl invariance of the character.

Implementation notes

The support of the coefficient function is finite because it is contained in the image of the finite type LieModule.Weight K L M under LieModule.Weight.toLinear, so the coefficients are assembled with Finsupp.ofSupportFinite.

Additivity for a short exact sequence is proved directly, without choosing a splitting: a surjective Lie-module map is surjective on each generalized weight space by Ado.genWeightSpaceMap_surjective, and rank-nullity gives the coefficient identity.

References

This is the "formal characters" item of Layer 6 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md, whose target signature formalCharacter is pinned in the accompanying Suggested.lean. Its stated prerequisite is the Layer 2 diagonalizability theorem, which supplies the honest multiplicities, together with the Layer 2 Weyl invariance proved directly from sl₂; both are consumed here.

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §22.5.
• N. Bourbaki, Groupes et algèbres de Lie, Chapitre VIII, §7.

The formal character

theorem Ado.exists_weight_coe_eq (K : Type u) (L : Type v) (M : Type w) [Field K] [LieRing L] [LieAlgebra K L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [LieModule.LinearWeights K L M] {χ : Module.Dual K L} (h : LieModule.genWeightSpace M ⇑χ ≠ ⊥) : ∃ (w : LieModule.Weight K L M), LieModule.Weight.toLinear K L M w = χ

A nonzero generalized weight space determines a bundled weight whose underlying linear form is the given one.

noncomputable def Ado.formalCharacter (K : Type u) (L : Type v) (M : Type w) [Field K] [LieRing L] [LieAlgebra K L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [LieModule.LinearWeights K L M] [FiniteDimensional K M] : AddMonoidAlgebra ℤ (Module.Dual K L)

The formal character of a finite-dimensional Lie module: the element of the integral group algebra of Module.Dual K L whose coefficient at χ is the dimension of the χ-weight space of M.

Equations

• Ado.formalCharacter K L M = AddMonoidAlgebra.ofCoeff (Finsupp.ofSupportFinite (fun (χ : Module.Dual K L) => ↑(Module.finrank K ↥(LieModule.genWeightSpace M ⇑χ))) ⋯)

@[simp]

theorem Ado.formalCharacter_coeff {K : Type u} {L : Type v} {M : Type w} [Field K] [LieRing L] [LieAlgebra K L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [LieModule.LinearWeights K L M] [FiniteDimensional K M] (χ : Module.Dual K L) : (formalCharacter K L M).coeff χ = ↑(Module.finrank K ↥(LieModule.genWeightSpace M ⇑χ))

The coefficient of the formal character at a linear form is the dimension of the corresponding weight space.

theorem Ado.formalCharacter_coeff_nonneg {K : Type u} {L : Type v} {M : Type w} [Field K] [LieRing L] [LieAlgebra K L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [LieModule.LinearWeights K L M] [FiniteDimensional K M] (χ : Module.Dual K L) : 0 ≤ (formalCharacter K L M).coeff χ

The coefficients of a formal character are dimensions, hence nonnegative.

theorem Ado.formalCharacter_coeff_eq_zero_iff {K : Type u} {L : Type v} {M : Type w} [Field K] [LieRing L] [LieAlgebra K L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [LieModule.LinearWeights K L M] [FiniteDimensional K M] {χ : Module.Dual K L} : (formalCharacter K L M).coeff χ = 0 ↔ LieModule.genWeightSpace M ⇑χ = ⊥

A coefficient of the formal character vanishes exactly at a linear form that is not a weight.

theorem Ado.formalCharacter_eq_sum_single {K : Type u} {L : Type v} {M : Type w} [Field K] [LieRing L] [LieAlgebra K L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [LieModule.LinearWeights K L M] [FiniteDimensional K M] : formalCharacter K L M = ∑ w : LieModule.Weight K L M, AddMonoidAlgebra.single (LieModule.Weight.toLinear K L M w) ↑(Module.finrank K ↥(LieModule.genWeightSpace M ⇑w))

The formal character as a sum of basis elements. Each bundled weight contributes its generalized weight-space dimension at the corresponding element of the dual.

theorem Ado.formalCharacter_congr {K : Type u} {L : Type v} {M : Type w} [Field K] [LieRing L] [LieAlgebra K L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [LieModule.LinearWeights K L M] [FiniteDimensional K M] {N : Type w₁} [AddCommGroup N] [Module K N] [LieRingModule L N] [LieModule K L N] [LieModule.LinearWeights K L N] [FiniteDimensional K N] (e : M ≃ₗ⁅K,L⁆ N) : formalCharacter K L M = formalCharacter K L N

The formal character is an isomorphism invariant. An equivalence of Lie modules carries the χ-weight space of one onto the χ-weight space of the other.

The total dimension

theorem Ado.sum_formalCharacter_coeff_eq_finrank (K : Type u) (L : Type v) (M : Type w) [Field K] [LieRing L] [LieAlgebra K L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [LieModule.LinearWeights K L M] [FiniteDimensional K M] [LieModule.IsTriangularizable K L M] : ((formalCharacter K L M).coeff.sum fun (x : Module.Dual K L) (n : ℤ) => n) = ↑(Module.finrank K M)

The coefficients of the formal character sum to the dimension of the module. The weight spaces are the summands of an internal direct sum decomposition (Ado.isInternal_genWeightSpace), and the character has one coefficient for each weight.

@[simp]

theorem Ado.formalCharacter_eq_zero_iff (K : Type u) (L : Type v) (M : Type w) [Field K] [LieRing L] [LieAlgebra K L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [LieModule.LinearWeights K L M] [FiniteDimensional K M] [LieModule.IsTriangularizable K L M] : formalCharacter K L M = 0 ↔ Module.finrank K M = 0

The formal character vanishes only for the zero module.

Additivity

@[simp]

theorem Ado.formalCharacter_prod {K : Type u} {L : Type v} {M : Type w} {N : Type w₁} [Field K] [LieRing L] [LieAlgebra K L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [LieModule.LinearWeights K L M] [FiniteDimensional K M] [AddCommGroup N] [Module K N] [LieRingModule L N] [LieModule K L N] [LieModule.LinearWeights K L N] [FiniteDimensional K N] : formalCharacter K L (M × N) = formalCharacter K L M + formalCharacter K L N

Additivity of the formal character. The character of a product of two finite-dimensional modules is the sum of their characters.

Additivity over an internal decomposition

An L-module M decomposed internally by Lie submodules has, at every linear form on a nilpotent Lie subalgebra H of L, a weight space that is the direct sum of the weight spaces of the summands, so the weight multiplicities add. This is the two-algebra statement the highest weight theory calls for: the decomposition is by submodules for the whole of L, while the character is read on a Cartan subalgebra H.

theorem Ado.formalCharacter_eq_sum_of_isInternal {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] {H : LieSubalgebra K L} [LieRing.IsNilpotent ↥H] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {ι : Type w₁} {N : ι → LieSubmodule K L M} [FiniteDimensional K M] [LieModule.LinearWeights K (↥H) M] [∀ (i : ι), LieModule.LinearWeights K ↥H ↥(N i)] [Fintype ι] [DecidableEq ι] (h : DirectSum.IsInternal fun (i : ι) => ↑(N i)) : formalCharacter K (↥H) M = ∑ i : ι, formalCharacter K ↥H ↥(N i)

Formal characters are additive over an internal decomposition into Lie submodules. The chi-weight space of the ambient module is the direct sum of the chi-weight spaces of the summands, so the weight multiplicities add.

Additivity on short exact sequences

theorem Ado.formalCharacter_eq_add_of_exact {K : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type u_1} [Field K] [LieRing L] [LieAlgebra K L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [AddCommGroup N] [Module K N] [LieRingModule L N] [LieModule K L N] [AddCommGroup P] [Module K P] [LieRingModule L P] [LieModule K L P] [LieModule.LinearWeights K L M] [LieModule.LinearWeights K L N] [LieModule.LinearWeights K L P] [FiniteDimensional K M] [FiniteDimensional K N] [FiniteDimensional K P] [LieModule.IsTriangularizable K L N] [LieModule.IsTriangularizable K L P] (f : M →ₗ⁅K,L⁆ N) (g : N →ₗ⁅K,L⁆ P) (h : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) : formalCharacter K L N = formalCharacter K L M + formalCharacter K L P

Formal characters are additive on short exact sequences. If M → N → P is exact, the first map is injective and the second is surjective, then the character of N is the sum of the characters of M and P.

Multiplicativity

theorem Ado.finrank_genWeightSpace_tensorProduct {K : Type u} {L : Type v} {M : Type w} {N : Type w₁} [Field K] [LieRing L] [LieAlgebra K L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [LieModule.LinearWeights K L M] [FiniteDimensional K M] [LieModule.IsTriangularizable K L M] [AddCommGroup N] [Module K N] [LieRingModule L N] [LieModule K L N] [LieModule.LinearWeights K L N] [FiniteDimensional K N] [LieModule.IsTriangularizable K L N] (χ : Module.Dual K L) : Module.finrank K ↥(LieModule.genWeightSpace (TensorProduct K M N) ⇑χ) = ∑ p : LieModule.Weight K L M × LieModule.Weight K L N, if LieModule.Weight.toLinear K L M p.1 + LieModule.Weight.toLinear K L N p.2 = χ then Module.finrank K ↥(LieModule.genWeightSpace M ⇑p.1) * Module.finrank K ↥(LieModule.genWeightSpace N ⇑p.2) else 0

Weight multiplicities in a tensor product are the convolution of the multiplicities in its factors. The dimension of the generalized χ-weight space is the sum of dim Mμ * dim Nν over the pairs of weights satisfying μ + ν = χ.

The tensor products of the generalized weight spaces form an independent family because the generalized weight-space decompositions of both factors are internal; their tensor products therefore decompose the ambient tensor product internally.

@[simp]

theorem Ado.formalCharacter_tensor {K : Type u} {L : Type v} {M : Type w} {N : Type w₁} [Field K] [LieRing L] [LieAlgebra K L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [LieModule.LinearWeights K L M] [FiniteDimensional K M] [LieModule.IsTriangularizable K L M] [AddCommGroup N] [Module K N] [LieRingModule L N] [LieModule K L N] [LieModule.LinearWeights K L N] [FiniteDimensional K N] [LieModule.IsTriangularizable K L N] : formalCharacter K L (TensorProduct K M N) = formalCharacter K L M * formalCharacter K L N

Multiplicativity of formal characters. The formal character of a tensor product is the product of the formal characters of its two factors.

The Cartan subalgebra of a Killing-semisimple Lie algebra over an algebraically closed field

of characteristic zero

theorem Ado.formalCharacter_coeff_eq_finrank_weightSpace {K : Type u} {L : Type v} [Field K] [CharZero K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] (χ : Module.Dual K ↥H) : (formalCharacter K (↥H) M).coeff χ = ↑(Module.finrank K ↥(LieModule.weightSpace M ⇑χ))

The coefficients of the formal character are the honest weight multiplicities. Over a Cartan subalgebra of a Killing-semisimple Lie algebra the generalized weight spaces are simultaneous eigenspaces, by Ado.genWeightSpace_eq_weightSpace.

theorem Ado.isIntegralWeight_of_formalCharacter_coeff_ne_zero {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [LieModule.IsTriangularizable K (↥H) L] {χ : Module.Dual K ↥H} (hχ : (formalCharacter K (↥H) M).coeff χ ≠ 0) : IsIntegralWeight χ

The formal character is supported on integral weights. A linear form carrying a nonzero coefficient is a weight of M, and the weights of a finite-dimensional module are integral (Ado.isIntegralWeight_of_weight).

theorem Ado.formalCharacter_coeff_weylGroup_smul {K : Type u} {L : Type v} [Field K] [CharZero K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] (w : ↥(LieAlgebra.IsKilling.rootSystem H).weylGroup) (χ : Module.Dual K ↥H) : (formalCharacter K (↥H) M).coeff (w • χ) = (formalCharacter K (↥H) M).coeff χ

Weyl invariance of the formal character. The multiplicity of a weight is unchanged by the action of the Weyl group of the root system of H; this is Ado.finrank_weightSpace_weylGroup_smul, proved directly from the rank-one theory and not from Weyl's complete reducibility theorem.