Complements make a finite-dimensional Lie module a direct sum of irreducibles

Complete reducibility is usually proved in its complement form: every Lie submodule of a finite-dimensional module has a complement. This file turns that form into the decomposition form: the module is the internal direct sum of finitely many irreducible Lie submodules.

The passage is lattice-theoretic and runs entirely in LieSubmodule K L M, which Mathlib already knows to be a complete, modular, compactly generated lattice, well-founded for > once M is Noetherian. Complements make it a ComplementedLattice, hence atomistic (isAtomistic_of_complementedLattice), hence the supremum of an independent set of atoms (exists_sSupIndep_of_sSup_atoms_eq_top), which well-foundedness makes finite (WellFoundedGT.finite_of_sSupIndep). Ado.isIrreducible_iff_isAtom reads the atoms as the irreducible submodules, and LieSubmodule.iSupIndep_toSubmodule transports the independence to the underlying submodules, where DirectSum.IsInternal lives.

The decomposition is indexed by Fin k rather than by the set of atoms: a Fin k index carries DecidableEq, which DirectSum.IsInternal needs, and it is what a dimension count sums over.

Main results

• Ado.exists_isInternal_isIrreducible: complete reducibility as a decomposition. A finite-dimensional Lie module whose submodule lattice is complemented is the internal direct sum of finitely many irreducible Lie submodules.

Roadmap

This is the shared tail of the two complete-reducibility theorems of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md: the sl₂ case of Layer 0 (TauCeti/Algebra/Lie/Sl2/Decomposition.lean) and Weyl's theorem of Layer 5 (TauCeti/Algebra/Lie/HighestWeight/CompleteReducibility.lean), both of which ask for the module to be exhibited as a direct sum of irreducibles.

theorem Ado.exists_isInternal_isIrreducible (K : Type u_1) [Field K] (L : Type u_2) [LieRing L] (M : Type u_3) [AddCommGroup M] [Module K M] [LieRingModule L M] [FiniteDimensional K M] [ComplementedLattice (LieSubmodule K L 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)

Complete reducibility as a decomposition. A finite-dimensional Lie module whose lattice of Lie submodules is complemented is the internal direct sum of a finite family of irreducible Lie submodules.