Lemmas about semisimple Lie algebras

This file is a home for lemmas about semisimple and reductive Lie algebras.

Main definitions / results:

• LieAlgebra.hasCentralRadical_and_of_isIrreducible_of_isFaithful: a finite-dimensional Lie algebra with a irreducible faithful finite-dimensional representation is reductive.
• LieAlgebra.hasTrivialRadical_and_of_isIrreducible_of_isFaithful: a finite-dimensional Lie algebra with a irreducible faithful finite-dimensional trace-free representation is semisimple.

## TODO

• It appears that the lemmas in this file may hold for any principal ideal domain (of characteristic zero) instead of a field. The plan would be to define the nilradical of a Lie algebra (currently missing) and use it with LieModule.exists_nontrivial_weightSpace_of_isNilpotent instead of using the solvable radical with LieModule.exists_nontrivial_weightSpace_of_isSolvable, as below. The conclusion of LieAlgebra.hasCentralRadical_and_of_isIrreducible_of_isFaithful would then make a statement that the nilradical vanishes and one would prove elsewhere that vanishing nilradical is equivalent to HasCentralRadical.

theorem LieAlgebra.hasCentralRadical_and_of_isIrreducible_of_isFaithful (k : Type u_1) (L : Type u_2) (M : Type u_3) [Field k] [CharZero k] [LieRing L] [LieAlgebra k L] [Module.Finite k L] [AddCommGroup M] [Module k M] [LieRingModule L M] [LieModule k L M] [Module.Finite k M] [LieModule.IsIrreducible k L M] [LieModule.IsFaithful k L M] [LieModule.IsTriangularizable k L M] : HasCentralRadical k L ∧ ∀ (x : L), x ∈ center k L ↔ (LieModule.toEnd k L M) x ∈ Submodule.span k {LinearMap.id}

theorem LieAlgebra.hasTrivialRadical_and_of_isIrreducible_of_isFaithful (k : Type u_1) (L : Type u_2) (M : Type u_3) [Field k] [CharZero k] [LieRing L] [LieAlgebra k L] [Module.Finite k L] [AddCommGroup M] [Module k M] [LieRingModule L M] [LieModule k L M] [Module.Finite k M] [LieModule.IsIrreducible k L M] [LieModule.IsFaithful k L M] [LieModule.IsTriangularizable k L M] (h : ∀ (x : L), (LinearMap.trace k M) ((LieModule.toEnd k L M) x) = 0) : HasTrivialRadical k L