The Cartan subalgebra acts diagonalizably, and weight spaces are honest

Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over an algebraically closed field of characteristic zero, let H be a Cartan subalgebra, and let M be a finite-dimensional L-module. This file proves that every x : H acts on M by a semisimple endomorphism, so that Mathlib's generalized weight spaces LieModule.genWeightSpace M χ are the honest simultaneous eigenspaces LieModule.weightSpace M χ, and M is their internal direct sum.

The route is the rank-one reduction, not the abstract Jordan decomposition. A nonzero root α carries an sl₂ triple whose Cartan element is the coroot α^∨, and the sl₂ engine already knows that such an element acts diagonalizably (Ado.iSup_eigenspace_toEnd_eq_top); over an algebraically closed field diagonalizable means semisimple (Ado.isSemisimple_of_iSup_eigenspace_eq_top). The coroots span H, and H is abelian, so the operators they give are commuting semisimple endomorphisms, and semisimplicity passes to their span (Module.End.IsSemisimple.add_of_commute, Module.End.IsSemisimple.of_mem_adjoin_singleton).

In particular the proof uses only complete reducibility for sl₂, which is where Ado.iSup_eigenspace_toEnd_eq_top comes from, and not Weyl's complete reducibility for L. That is what keeps the highest-weight theory free of circularity: the honest weight-space decomposition is available before Weyl's theorem, whose usual proof consumes it.

That every finite-dimensional module is triangularizable over H needs no work here: it is Mathlib's LieModule.instIsTriangularizableOfIsAlgClosed, which is what makes the generalized weight spaces exhaust M in the first place. The content below is the refinement from generalized to honest.

Main results

• Ado.nonempty_weight: a nonzero finite-dimensional triangularizable module has a weight.
• Ado.isInternal_genWeightSpace: a finite-dimensional triangularizable module is the internal direct sum of its generalized weight spaces. This needs no diagonalizability and is the form the dimension counts consume; the honest-weight-space refinement is below.
• Ado.eq_zero_of_forall_genWeightSpace: a linear functional vanishing on every generalized weight space is zero.
• Ado.isSemisimple_toEnd_coroot: a coroot acts semisimply on a finite-dimensional module.
• Ado.isSemisimple_toEnd_cartan: every element of the Cartan subalgebra acts semisimply.
• Ado.genWeightSpace_eq_weightSpace: the generalized weight spaces are honest weight spaces, with Ado.mem_genWeightSpace_iff_forall_lie_eq_smul the pointwise form: membership is the eigenvector equation ⁅x, m⁆ = χ x • m for every x : H.
• Ado.iSup_weightSpace_eq_top and Ado.isInternal_weightSpace: the honest weight spaces span M, and M is their internal direct sum, so χ ↦ finrank (weightSpace M χ) counts honest multiplicities.
• Ado.eq_zero_of_genWeightSpace_ne_bot_of_isTrivial: a trivial module has no weight but zero. This needs neither diagonalizability nor the Cartan hypothesis, and is stated for an arbitrary nilpotent Lie algebra acting trivially.

References

This is the "honest weight spaces (the diagonalizability theorem)" item of Layer 2 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md, whose target signature isSemisimple_toEnd_cartan is Ado.isSemisimple_toEnd_cartan.

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §6.4 and §20.1.

Existence of a weight

theorem Ado.nonempty_weight (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] [FiniteDimensional K M] [LieModule.IsTriangularizable K L M] [Nontrivial M] : Nonempty (LieModule.Weight K L M)

A nonzero finite-dimensional triangularizable module has at least one weight: the generalized weight spaces span it (LieModule.iSup_genWeightSpace_eq_top'), and an empty supremum is ⊥. LieModule.Weight is by definition indexed by the linear forms whose generalized weight space is nonzero, so no honest-weight-space hypothesis is available or needed here; nilpotency of L is carried only because LieModule.Weight demands it.

Mathlib performs this step inside the proof of LieModule.exists_nontrivial_weightSpace_of_isNilpotent rather than naming it.

The generalized weight-space decomposition

theorem Ado.isInternal_genWeightSpace (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] [FiniteDimensional K M] [LieModule.IsTriangularizable K L M] [DecidableEq (LieModule.Weight K L M)] : DirectSum.IsInternal fun (χ : LieModule.Weight K L M) => ↑(LieModule.genWeightSpace M ⇑χ)

The generalized weight-space decomposition. A finite-dimensional triangularizable module is the internal direct sum of its generalized weight spaces, indexed by all of its weights. This is Mathlib's LieModule.iSupIndep_genWeightSpace' and LieModule.iSup_genWeightSpace_eq_top' packaged as a DirectSum.IsInternal, which is the form the dimension counts consume.

theorem Ado.eq_zero_of_forall_genWeightSpace {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] [FiniteDimensional K M] [LieModule.IsTriangularizable K L M] {g : Module.Dual K M} (hg : ∀ (χ : L → K), ∀ m ∈ LieModule.genWeightSpace M χ, g m = 0) : g = 0

A functional vanishing on every generalized weight space is zero. The generalized weight spaces of a finite-dimensional triangularizable module span it (LieModule.iSup_genWeightSpace_eq_top), so a linear functional killing each of them kills M.

Trivial modules

theorem Ado.eq_zero_of_genWeightSpace_ne_bot_of_isTrivial {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.IsTrivial L M] {chi : L → K} (hchi : LieModule.genWeightSpace M chi ≠ ⊥) : chi = 0

A trivial module has no weight but zero: the only linear form with a nonzero generalized weight space in a module on which the Lie algebra acts by zero is the zero form.

Semisimplicity of the Cartan action

theorem Ado.isSemisimple_toEnd_coroot {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] (α : LieModule.Weight K (↥H) L) : ((LieModule.toEnd K (↥H) M) (LieAlgebra.IsKilling.coroot α)).IsSemisimple

A coroot acts semisimply. The coroot α^∨ of a weight α of L acts on a finite-dimensional module by a semisimple endomorphism.

For a nonzero α this is the sl₂ engine: α^∨ is the Cartan element of an sl₂ triple, whose eigenspaces span (Ado.iSup_eigenspace_toEnd_eq_top), and a diagonalizable endomorphism is semisimple. The coroot of a zero weight is zero.

theorem Ado.isSemisimple_toEnd_cartan {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] (x : ↥H) : ((LieModule.toEnd K (↥H) M) x).IsSemisimple

The Cartan subalgebra acts semisimply. Every element of a Cartan subalgebra of a Killing-semisimple Lie algebra acts on a finite-dimensional module by a semisimple endomorphism.

The coroots span the Cartan subalgebra (RootPairing.IsRootSystem.span_coroot_eq_top for LieAlgebra.IsKilling.rootSystem H) and act semisimply by Ado.isSemisimple_toEnd_coroot; the Cartan subalgebra is abelian, so the endomorphisms they give commute, and both a sum of commuting semisimple endomorphisms and a scalar multiple of one are again semisimple.

Honest weight spaces

@[simp]

theorem Ado.genWeightSpaceOf_eq_eigenspace {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] (μ : K) (x : ↥H) : ↑(LieModule.genWeightSpaceOf M μ x) = ((LieModule.toEnd K (↥H) M) x).eigenspace μ

The generalized eigenspace of x : H at a scalar is an honest eigenspace.

@[simp]

theorem Ado.genWeightSpace_eq_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] (χ : ↥H → K) : LieModule.genWeightSpace M χ = LieModule.weightSpace M χ

The generalized weight spaces are honest weight spaces. For a finite-dimensional module over a Killing-semisimple Lie algebra, LieModule.genWeightSpace M χ is the simultaneous eigenspace LieModule.weightSpace M χ.

Mathlib's LieModule.weightSpace_le_genWeightSpace is the inclusion that holds always; this is the reverse one, and it is exactly the diagonalizability of the Cartan action.

theorem Ado.mem_genWeightSpace_iff_forall_lie_eq_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] {χ : ↥H → K} {m : M} : m ∈ LieModule.genWeightSpace M χ ↔ ∀ (x : ↥H), ⁅↑x, m⁆ = χ x • m

Membership of a weight space is the eigenvector equation. An element of a finite-dimensional module lies in the χ-weight space exactly when every x : H acts on it by the scalar χ x.

This is deliberately not a simp lemma: Ado.genWeightSpace_eq_weightSpace already rewrites the left-hand side to m ∈ LieModule.weightSpace M χ, so tagging it would leave it in non-simp-normal form.

theorem Ado.iSup_weightSpace_eq_top (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] : ⨆ (χ : LieModule.Weight K (↥H) M), LieModule.weightSpace M ⇑χ = ⊤

The honest weight spaces span. A finite-dimensional module over a Killing-semisimple Lie algebra is spanned by the simultaneous eigenspaces of its Cartan subalgebra.

theorem Ado.isInternal_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] : DirectSum.IsInternal fun (χ : LieModule.Weight K (↥H) M) => ↑(LieModule.weightSpace M ⇑χ)

The honest weight-space decomposition. A finite-dimensional module over a Killing-semisimple Lie algebra is the internal direct sum of the simultaneous eigenspaces of its Cartan subalgebra, so χ ↦ finrank (weightSpace M χ) counts honest multiplicities.