Weyl's complete reducibility theorem

Let L be a finite-dimensional Lie algebra with nondegenerate Killing form over a field of characteristic zero. Every Lie submodule of a finite-dimensional L-module is a direct summand (Ado.exists_isCompl_of_isKilling), so the lattice of Lie submodules is complemented and a finite-dimensional module is a direct sum of irreducibles.

All the formal content of the proof is already in TauCeti/Algebra/Lie/CompleteReducibility.lean, which derives complete reducibility from the single representation-theoretic input Ado.HasInvariantOutsideIrreducible: whenever L carries a finite-dimensional module M into a proper irreducible submodule N and acts nontrivially somewhere on M, the module M has a nonzero invariant vector outside N. Over an algebraically closed field this file supplies that input from the Casimir element of U(L), which is what makes the argument work for a general semisimple L rather than only for sl₂ (TauCeti/Algebra/Lie/Sl2/CompleteReducibility.lean, the rank-one instance of the same reduction). Over an arbitrary field of characteristic zero it is then obtained by descent from an algebraic closure.

The Casimir step

Two facts about the Casimir element Ω ∈ U(L) do the work.

• Ω acts on M by a sum of double brackets ∑ᵢ ⁅xᵢ, ⁅yᵢ, -⁆⁆, so ⁅L, M⁆ ⊆ N already forces its image to lie in N.
• Ω is injective on a nontrivial finite-dimensional irreducible module (Ado.representation_casimirElement_injective_of_isIrreducible_of_not_isTrivial): such a module is generated by a highest weight vector of a dominant integral weight λ (Ado.exists_isHighestWeightVector_and_lieSpan_eq_top), and λ ≠ 0 because a highest weight vector of weight zero generates a trivial module (Ado.isTrivial_of_isHighestWeightVector_weight_zero_of_isIrreducible); the Casimir then acts by the nonzero scalar ⟨λ + ρ, λ + ρ⟩ - ⟨ρ, ρ⟩ (Ado.casimir_apply_ne_zero_of_isHighestWeightVector_of_lieSpan_eq_top).

Being injective on N and having its image inside the proper submodule N, the Casimir operator of M is not surjective, hence — M being finite-dimensional — not injective; a nonzero kernel vector lies outside N, and its brackets lie in N ∩ ker Ω = 0, so it is invariant.

The remaining case is the one where L acts trivially on N. Then the action of L on M composes to zero, and a Lie algebra with nondegenerate Killing form is perfect (Ado.derivedSeries_one_eq_top_of_isKilling), so the action is already zero, contradicting the hypothesis that L acts nontrivially somewhere on M.

Descent from an algebraic closure

Over a field K of characteristic zero, let A = AlgebraicClosure K. The Killing form of A ⊗[K] L is the extension of that of L, so it is again nondegenerate (Ado.isKilling_baseChange_iff). If L carries M into a proper Lie submodule N, then A ⊗[K] L carries A ⊗[K] M into the proper Lie submodule N.baseChange A, and the algebraically closed case gives an invariant vector of A ⊗[K] M outside N.baseChange A. The invariants of A ⊗[K] M are the extension of the invariants of M (LieModule.maxTrivSubmodule_baseChange), so the invariants of M are not all contained in N.

Main results

• Ado.representation_casimirElement_injective_of_isIrreducible_of_not_isTrivial: the Casimir element acts injectively on a finite-dimensional irreducible module with a nontrivial action.
• Ado.exists_invariant_notMem_of_isKilling: a module carried into a proper Lie submodule has an invariant vector outside it.
• Ado.hasInvariantOutsideIrreducible_of_isKilling: hence the input of the formal complete-reducibility argument holds over every field of characteristic zero.
• Ado.exists_isCompl_of_isKilling: Weyl's complete reducibility theorem. Every Lie submodule of a finite-dimensional module is a direct summand.
• Ado.complementedLattice_lieSubmodule_of_isKilling: the lattice restatement.
• Ado.exists_isInternal_isIrreducible_of_isKilling: the decomposition restatement, a finite-dimensional module as an internal direct sum of irreducibles.
• LieSubmodule.exists_isCompl_of_le_ker: Weyl's theorem for a module on which an ideal I acts trivially, when only the quotient L ⧸ I has nondegenerate Killing form.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §6.3, for the Casimir proof of Weyl's theorem; the reduction to the case of a codimension-one submodule is the formal part carried out in TauCeti/Algebra/Lie/CompleteReducibility.lean.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 1--3, Ch. I, §6, no. 2, for Weyl's theorem over an arbitrary field of characteristic zero.

The Casimir element is injective on a nontrivial irreducible

theorem Ado.representation_casimirElement_injective_of_isIrreducible_of_not_isTrivial {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] [IsAlgClosed K] (M : Type w) [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [LieModule.IsIrreducible K L M] (hact : ¬LieModule.IsTrivial L M) : Function.Injective ⇑((UniversalEnvelopingAlgebra.representation K L M) (casimirElement K L))

The Casimir element is injective on a nontrivial finite-dimensional irreducible module. The module is generated by a highest weight vector, whose weight is dominant integral and, the action being nontrivial, nonzero; the Casimir element then acts by a nonzero scalar.

The Casimir step over an algebraically closed field

Complete reducibility over a field of characteristic zero

theorem Ado.exists_invariant_notMem_of_isKilling {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] (N : LieSubmodule K L M) (hN : N ≠ ⊤) (htriv : ∀ (x : L) (m : M), ⁅x, m⁆ ∈ N) : ∃ v ∉ N, ∀ (x : L), ⁅x, v⁆ = 0

An invariant vector outside a proper submodule. If L carries a finite-dimensional module M into a proper Lie submodule N, then M has a nonzero invariant vector outside N.

theorem Ado.hasInvariantOutsideIrreducible_of_isKilling (K : Type u) (L : Type v) [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] : HasInvariantOutsideIrreducible K L

The input of the formal complete-reducibility argument holds in characteristic zero: if L carries a finite-dimensional module into a proper irreducible Lie submodule N and acts nontrivially somewhere, the module has an invariant vector outside N.

theorem Ado.exists_isCompl_of_isKilling {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] (N : LieSubmodule K L M) : ∃ (N' : LieSubmodule K L M), IsCompl N N'

Weyl's complete reducibility theorem. Over a field of characteristic zero, every Lie submodule of a finite-dimensional module over a Lie algebra with nondegenerate Killing form has a complement, so the module is a direct sum of irreducibles.

The sl₂ case, Ado.exists_isCompl_of_toLieSubalgebra_eq_top, is the rank-one instance of the same argument, run with the concrete Casimir operator of an sl₂ triple.

theorem Ado.complementedLattice_lieSubmodule_of_isKilling (K : Type u) (L : Type v) [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] (M : Type w) [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] : ComplementedLattice (LieSubmodule K L M)

The lattice form of Weyl's theorem: the Lie submodules of a finite-dimensional module over a Lie algebra with nondegenerate Killing form form a complemented lattice.

theorem Ado.exists_isInternal_isIrreducible_of_isKilling (K : Type u) (L : Type v) [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] (M : Type w) [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] : ∃ (k : ℕ) (N : Fin k → LieSubmodule K L M), (DirectSum.IsInternal fun (i : Fin k) => ↑(N i)) ∧ ∀ (i : Fin k), LieModule.IsIrreducible K L ↥(N i)

Weyl's theorem as a decomposition. A finite-dimensional module over a Lie algebra with nondegenerate Killing form, over a field of characteristic zero, is the internal direct sum of a finite family of irreducible Lie submodules.

theorem LieSubmodule.exists_isCompl_of_le_ker {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] (N : LieSubmodule K L M) {I : LieIdeal K L} [LieAlgebra.IsKilling K (L ⧸ I)] (hI : I ≤ LieModule.ker K L M) : ∃ (N' : LieSubmodule K L M), IsCompl N N'

Weyl's theorem for an action through a quotient. If an ideal I of L acts trivially on a finite-dimensional module M and the quotient L ⧸ I has nondegenerate Killing form, then every Lie submodule of M has a complement. This applies when L itself is not semisimple, for instance to a module of L on which its solvable radical acts trivially.