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 an irreducible faithful finite-dimensional representation is reductive.LieAlgebra.hasTrivialRadical_of_isIrreducible_of_isFaithful: a finite-dimensional Lie algebra with an irreducible faithful finite-dimensional trace-free representation is semisimple.
TODO #
- Introduce a
Prop-valued typeclassLieModule.IsTracefreestating(toEnd R L M).range ≤ LieAlgebra.derivedSeries R (Module.End R M) 1, provef ∈ LieAlgebra.derivedSeries k (Module.End k V) 1 ↔ LinearMap.trace k _ f = 0, and restateLieAlgebra.hasTrivialRadical_of_isIrreducible_of_isFaithfulusingLieModule.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] :
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) :
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) :