Every finite-dimensional sl₂-module is a direct sum of the V(n)

TauCeti/Algebra/Lie/Sl2/CompleteReducibility.lean proves complete reducibility in its complement form: every Lie submodule of a finite-dimensional module over a Lie algebra generated by an sl₂ triple has a complement. TauCeti/Algebra/Lie/Sl2/Classification.lean proves that the finite-dimensional irreducibles are exactly the standard modules Ado.Sl2Std K n = V(n). This file joins the two into the decomposition itself: such a module is an internal direct sum of finitely many irreducible Lie submodules, and over LieAlgebra.SpecialLinear.sl (Fin 2) K each summand is a V(n).

The passage from complements to a decomposition is lattice-theoretic, and is carried out for an arbitrary Lie module in TauCeti/Algebra/Lie/Submodule/Decomposition.lean (Ado.exists_isInternal_isIrreducible); this file only feeds it the sl₂ complements and identifies the resulting summands.

Main results

• Ado.Sl2Std.exists_isInternal_lieModuleEquiv: every finite-dimensional sl₂-module is ⨁ V(nᵢ). Over LieAlgebra.SpecialLinear.sl (Fin 2) K the summands are the standard modules.
• Ado.Sl2Std.finrank_eq_sum: the dimension of the module is ∑ᵢ (nᵢ + 1).

References

This closes the complete-reducibility item of Layer 0 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md, which asks that every finite-dimensional sl₂-module be exhibited as a direct sum of the V(nᵢ).

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

theorem Ado.Sl2Std.exists_isInternal_lieModuleEquiv (K : Type u_1) [Field K] [CharZero K] [IsAlgClosed K] (M : Type u_2) [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] : ∃ (k : ℕ) (N : Fin k → LieSubmodule K (↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) M) (n : Fin k → ℕ), (DirectSum.IsInternal fun (i : Fin k) => ↑(N i)) ∧ ∀ (i : Fin k), Nonempty (↥(N i) ≃ₗ⁅K,↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)⁆ Sl2Std K (n i))

Every finite-dimensional sl₂-module is ⨁ V(nᵢ). Over an algebraically closed field of characteristic zero, a finite-dimensional LieAlgebra.SpecialLinear.sl (Fin 2) K-module is the internal direct sum of a finite family of Lie submodules, the i-th of which is equivalent to the standard irreducible V(nᵢ). The highest weights nᵢ are returned alongside the summands.

theorem Ado.Sl2Std.finrank_eq_sum {K : Type u_1} [Field K] {M : Type u_2} [AddCommGroup M] [Module K M] [LieRingModule (↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) M] {k : ℕ} {N : Fin k → LieSubmodule K (↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) M} {n : Fin k → ℕ} (hint : DirectSum.IsInternal fun (i : Fin k) => ↑(N i)) (hn : ∀ (i : Fin k), Nonempty (↥(N i) ≃ₗ⁅K,↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)⁆ Sl2Std K (n i))) : Module.finrank K M = ∑ i : Fin k, (n i + 1)

The dimension of an sl₂-module from its decomposition. If the module is the internal direct sum of Lie submodules equivalent to V(n₀), …, V(n_{k-1}), its dimension is ∑ᵢ (nᵢ + 1), each V(nᵢ) having dimension nᵢ + 1.