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_of_isIrreducible_of_isFaithful: a finite-dimensional Lie algebra with a irreducible faithful finite-dimensional trace-free representation is semisimple.

## TODO

• Introduce a Prop-valued typeclass LieModule.IsTracefree stating (toEnd R L M).range ≤ LieAlgebra.derivedSeries R (Module.End R M) 1, prove f ∈ LieAlgebra.derivedSeries k (Module.End k V) 1 ↔ LinearMap.trace k _ f = 0, and restate LieAlgebra.hasTrivialRadical_of_isIrreducible_of_isFaithful using LieModule.IsTracefree.

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_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

theorem LieAlgebra.trace_toEnd_eq_zero {L : Type u_2} {M : Type u_3} [LieRing L] [AddCommGroup M] [LieRingModule L M] {R : Type u_4} [CommRing R] [LieAlgebra R L] [Module R M] [LieModule R L M] {s : Set L} (hs : ∀ x ∈ s, (LinearMap.trace R M) ((LieModule.toEnd R L M) x) = 0) {x : L} (hx : x ∈ LieSubalgebra.lieSpan R L s) : (LinearMap.trace R M) ((LieModule.toEnd R L M) x) = 0