Complete reducibility for sl₂

Every finite-dimensional module over a Lie algebra generated by an sl₂ triple, over an algebraically closed field of characteristic zero, is a direct sum of irreducibles: every Lie submodule has a complement (Ado.exists_isCompl_of_toLieSubalgebra_eq_top). With the classification of the irreducibles already in TauCeti/Algebra/Lie/Sl2/Classification.lean, this says that every such module is ⨁ V(nᵢ).

The argument is the classical one, and all of it except the Casimir step is field- and algebra-agnostic; that part lives in TauCeti/Algebra/Lie/CompleteReducibility.lean, whose Ado.HasInvariantOutsideIrreducible is the single input it consumes. This file supplies that input for an sl₂ triple, using the concrete Casimir operator of TauCeti/Algebra/Lie/Sl2/Casimir.lean, which is built from the triple alone and so needs neither the universal enveloping algebra nor the Killing form: this is Layer 0 of the roadmap, and the general Casimir argument for a semisimple Lie algebra is Layer 5.

Concretely, if L carries M into an irreducible proper submodule N and acts nontrivially somewhere on M, then L acts nontrivially on N — otherwise the action would compose to zero, and L, being perfect (Ado.lie_eq_zero_of_lie_lie_eq_zero), would act trivially on M — so the Casimir operator is injective on N while its range lies in N; it is therefore not surjective, hence not injective, and any nonzero kernel vector is invariant and outside N.

Main results

• Ado.hasInvariantOutsideIrreducible_of_toLieSubalgebra_eq_top: the Casimir step, which is everything TauCeti/Algebra/Lie/CompleteReducibility.lean needs.
• Ado.exists_invariant_notMem: an invariant vector outside a proper submodule containing ⁅L, M⁆.
• Ado.exists_isCompl_of_toLieSubalgebra_eq_top: complete reducibility. Every Lie submodule of a finite-dimensional module over a Lie algebra generated by an sl₂ triple has a complement.
• Ado.exists_isCompl_sl_fin_two: the same for the model algebra LieAlgebra.SpecialLinear.sl (Fin 2) K.

References

This is Layer 0 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md, whose sl₂ complete reducibility is Ado.exists_isCompl_of_toLieSubalgebra_eq_top.

• [J. E. Humphreys, Introduction to Lie Algebras and Representation Theory][humphreys1972], §6.2 and §6.3.

The Casimir step, and the complete reducibility it unlocks

theorem Ado.hasInvariantOutsideIrreducible_of_toLieSubalgebra_eq_top {K : Type u_1} [Field K] [CharZero K] [IsAlgClosed K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {h e f : L} {t : IsSl2Triple h e f} (htop : IsSl2Triple.toLieSubalgebra K t = ⊤) : HasInvariantOutsideIrreducible K L

The Casimir operator supplies an invariant vector outside an irreducible submodule. If L carries M into an irreducible proper N and acts nontrivially somewhere on M, then L acts nontrivially on N, so the Casimir operator is injective on N. Its range lies in N, so it is not surjective on M, hence — M being finite-dimensional — not injective, and any nonzero kernel vector is invariant and outside N.

This is the single input of TauCeti/Algebra/Lie/CompleteReducibility.lean; everything else in the proof of complete reducibility is formal.

theorem Ado.exists_invariant_notMem {K : Type u_1} [Field K] [CharZero K] [IsAlgClosed K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {h e f : L} {t : IsSl2Triple h e f} {M : Type v} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] (htop : IsSl2Triple.toLieSubalgebra K t = ⊤) [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 a Lie algebra generated by an sl₂ triple carries a finite-dimensional module M into a proper Lie submodule N, then M has an invariant vector outside N.

theorem Ado.exists_isCompl_of_toLieSubalgebra_eq_top {K : Type u_1} [Field K] [CharZero K] [IsAlgClosed K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {h e f : L} {t : IsSl2Triple h e f} {M : Type v} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] (htop : IsSl2Triple.toLieSubalgebra K t = ⊤) [FiniteDimensional K M] (N : LieSubmodule K L M) : ∃ (N' : LieSubmodule K L M), IsCompl N N'

Complete reducibility for sl₂. Over an algebraically closed field of characteristic zero, every Lie submodule of a finite-dimensional module over a Lie algebra generated by an sl₂ triple has a complement, so the module is a direct sum of irreducibles.

Combined with the classification of the irreducibles (Ado.Sl2Std.existsUnique_nonempty_lieModuleEquiv), every such module is ⨁ V(nᵢ).

theorem Ado.exists_isCompl_sl_fin_two {K : Type u_1} [Field K] [CharZero K] [IsAlgClosed K] {M : Type v} [AddCommGroup M] [Module K M] [LieRingModule (↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) M] [LieModule K (↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) M] [FiniteDimensional K M] (N : LieSubmodule K (↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) M) : ∃ (N' : LieSubmodule K (↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) M), IsCompl N N'

Complete reducibility for the model sl₂. Over an algebraically closed field of characteristic zero, every Lie submodule of a finite-dimensional module over LieAlgebra.SpecialLinear.sl (Fin 2) K has a complement. This is Ado.exists_isCompl_of_toLieSubalgebra_eq_top for the standard triple, which generates sl (Fin 2) K by Ado.toLieSubalgebra_isSl2Triple_single_eq_top.