leanprover-community
A semisimple Lie algebra is a direct sum of simple Lie algebras
In characteristic zero, a semisimple Lie algebra is a direct sum of simple Lie algebras. We should add this result to Mathlib.
I think the most useful statement of this result would not use either the internal or external direct sum API but instead state the result in the lattice theory language (the minimal ideals have iSup equal to top and are independent in the lattice-theoretic sense).
Note that I don't know whether the following method remains true in general char=0 fields. But, do we already have the Killing form and Cartan's criterion? (if so, then if there exists a proper nontrivial ideal then it has trivial intersection with its orthogonal complement).
We do not yet have Cartan's criteria for solvability or semisimplicity. (Possibly @Espio231 might have some work in this direction.)
I tried quite hard to avoid using characteristic-zero techniques when they were not required. Of course eventually such techniques are needed (the classification in positive characteristic is much harder, and more complicated, but also less important) and we have basically reached this point.
Note also that in characteristic zero the following three conditions for a finite-dimensional Lie algebra over a field are equivalent:
- The solvable radical is trivial
- The Lie algebra is a sum of simple Lie algebras (its minimal ideals)
- The Killing form is non-degenerate
In positive characteristic it is still true that 3 implies 2 and that 2 implies 1 (and in fact Mathlib knows that 3 implies 1) but there are counterexamples to the other implications.
For more detail there is Seligman's book Modular Lie Algebras
See also this proof of Lie's theorem: https://github.com/Espio231/LiesTheorem/tree/main
Wikipedia suggests Dieudonné, Jean (1953), "On semi-simple Lie algebras" for a proof of (3) => (2). It seems like a good source to me.
I just created #13217. Which is a first step towards the implications in Oliver's comment https://github.com/leanprover-community/mathlib4/issues/10073#issuecomment-2035689143