Formal characters from a weight basis

A basis of simultaneous eigenvectors makes every acting endomorphism diagonalizable, so its honest and generalized weight spaces agree over the original field. The formal character is the sum of the corresponding group-algebra basis elements, counting repeated weights with their multiplicities. If the basis weights are pairwise distinct, each occurring weight space is a line and each weight has coefficient one.

These results connect explicit diagonal actions, such as the exterior model of spinors, to TauCeti.formalCharacter without requiring algebraic closedness or characteristic zero.

theorem Module.Basis.genWeightSpace_eq_weightSpace_of_weight_basis {K : Type u} [Field K] {L : Type v} [LieRing L] [LieAlgebra K L] [LieRing.IsNilpotent L] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {ι : Type t} (b : Basis ι K M) {μ : ι → Dual K L} (hb : ∀ (i : ι) (x : L), ⁅x, b i⁆ = (μ i) x • b i) (χ : L → K) : LieModule.genWeightSpace M χ = LieModule.weightSpace M χ

A basis of weight vectors makes generalized weight spaces equal to honest weight spaces.

theorem Module.Basis.weightSpace_eq_span_singleton_of_weight_basis {K : Type u} [Field K] {L : Type v} [LieRing L] [LieAlgebra K L] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {ι : Type t} (b : Basis ι K M) {μ : ι → Dual K L} (hb : ∀ (i : ι) (x : L), ⁅x, b i⁆ = (μ i) x • b i) (hμ : Function.Injective μ) (i : ι) : ↑(LieModule.weightSpace M ⇑(μ i)) = K ∙ b i

With distinct basis weights, the weight space at a basis weight is its basis-vector line.

theorem Module.Basis.linearWeights_of_weight_basis {K : Type u} [Field K] {L : Type v} [LieRing L] [LieAlgebra K L] [LieRing.IsNilpotent L] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {ι : Type t} (b : Basis ι K M) {μ : ι → Dual K L} (hb : ∀ (i : ι) (x : L), ⁅x, b i⁆ = (μ i) x • b i) : LieModule.LinearWeights K L M

A basis of weight vectors gives linear generalized weights vanishing on brackets.

theorem Module.Basis.formalCharacter_eq_sum_single_of_weight_basis {K : Type u} [Field K] {L : Type v} [LieRing L] [LieAlgebra K L] [LieRing.IsNilpotent L] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {ι : Type t} (b : Basis ι K M) {μ : ι → Dual K L} (hb : ∀ (i : ι) (x : L), ⁅x, b i⁆ = (μ i) x • b i) [Fintype ι] : TauCeti.formalCharacter K L M = ∑ i : ι, AddMonoidAlgebra.single (μ i) 1

The formal character of a module with a finite basis of weight vectors is the sum of those weights, counting repeated weights with their multiplicities.