Weight spaces for finitely semisimple actions

Generalized and honest weight spaces of a nilpotent Lie algebra agree whenever every acting endomorphism is finitely semisimple: its restriction to every finitely generated invariant submodule is semisimple. This uses Mathlib's equality for generalized eigenspaces over a commutative ring and needs neither a splitting field nor finite-dimensionality.

theorem TauCeti.genWeightSpace_eq_weightSpace_of_isFinitelySemisimple {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (h : ∀ (x : L), ((LieModule.toEnd R L M) x).IsFinitelySemisimple) (χ : L → R) : LieModule.genWeightSpace M χ = LieModule.weightSpace M χ

Generalized and honest weight spaces of a nilpotent Lie algebra agree when every acting endomorphism is finitely semisimple. The scalars may form any commutative ring.