Weight-space multiplicities in isotypic Lie modules

This file connects the dimension of an honest weight space with the number of irreducible summands in an isotypic Lie module. A Lie-module equivalence preserves every weight space, while an internal direct sum of Lie submodules decomposes each weight space into the corresponding weight spaces of the summands. Consequently, the dimension of each ambient weight space is the isotypic multiplicity times its dimension in the irreducible type. In particular, a weight of multiplicity one reads off the isotypic multiplicity.

The statements concern simultaneous eigenspaces LieModule.weightSpace, not generalized weight spaces. They therefore require neither nilpotence of the acting Lie algebra nor triangularizability of the module.

Main results

• DirectSum.IsInternal.finrank_weightSpace_eq_sum: weight-space dimensions add over a finite internal decomposition by Lie submodules.
• LieModule.IsIsotypicOfType.finrank_weightSpace_eq_isotypicMultiplicity_mul: the dimension of an isotypic weight space is the number of summands times its dimension in the irreducible type.
• LieModule.IsIsotypicOfType.isotypicMultiplicity_eq_finrank_weightSpace: a weight of multiplicity one in the irreducible type reads off the isotypic multiplicity.

theorem DirectSum.IsInternal.finrank_weightSpace_eq_sum {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] {H : LieSubalgebra K L} {M : Type u_3} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {ι : Type u_4} {N : ι → LieSubmodule K L M} [Fintype ι] {dec_ι : DecidableEq ι} (h : IsInternal fun (i : ι) => ↑(N i)) (χ : ↥H → K) [∀ (i : ι), FiniteDimensional K ↥(LieModule.weightSpace (↥(N i)) χ)] : Module.finrank K ↥(LieModule.weightSpace M χ) = ∑ i : ι, Module.finrank K ↥(LieModule.weightSpace (↥(N i)) χ)

Weight-space dimensions are additive over an internal decomposition. If a finite family of L-submodules is an internal direct sum of M, then the dimension of the χ-weight space for any Lie subalgebra H is the sum of the dimensions of the summands' χ-weight spaces.

theorem LieModule.IsIsotypicOfType.finrank_weightSpace_eq_isotypicMultiplicity_mul {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] {H : LieSubalgebra K L} {M : Type u_3} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {S : Type u_4} [AddCommGroup S] [Module K S] [LieRingModule L S] [LieModule K L S] [IsAlgClosed K] [FiniteDimensional K M] [FiniteDimensional K S] [IsIrreducible K L S] [ComplementedLattice (LieSubmodule K L M)] (h : IsIsotypicOfType K L M S) (χ : ↥H → K) : Module.finrank K ↥(weightSpace M χ) = isotypicMultiplicity K L M S * Module.finrank K ↥(weightSpace S χ)

Weight-space dimension in an isotypic module. Suppose M is a finite-dimensional completely reducible module, isotypic of an irreducible type S. The dimension of every weight space of M is the number of copies of S times the dimension of the corresponding weight space of S.

theorem LieModule.IsIsotypicOfType.isotypicMultiplicity_eq_finrank_weightSpace {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] {H : LieSubalgebra K L} {M : Type u_3} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {S : Type u_4} [AddCommGroup S] [Module K S] [LieRingModule L S] [LieModule K L S] [IsAlgClosed K] [FiniteDimensional K M] [FiniteDimensional K S] [IsIrreducible K L S] [ComplementedLattice (LieSubmodule K L M)] (h : IsIsotypicOfType K L M S) (χ : ↥H → K) (hone : Module.finrank K ↥(weightSpace S χ) = 1) : isotypicMultiplicity K L M S = Module.finrank K ↥(weightSpace M χ)

A multiplicity-one weight reads off the isotypic multiplicity. Suppose M is a finite-dimensional completely reducible module, isotypic of an irreducible type S. If the χ-weight space of S is one-dimensional, then the dimension of the χ-weight space of M is the number of copies of S in M.