Lie's theorem for Solvable Lie algebras.

Lie's theorem asserts that Lie modules of solvable Lie algebras over fields of characteristic 0 have a common eigenvector for the action of all elements of the Lie algebra. This result is named LieModule.exists_forall_lie_eq_smul_of_isSolvable.

def LieModule.weightSpaceOfIsLieTower (R : Type u_1) {L : Type u_2} {A : Type u_3} (V : Type u_4) [CommRing R] [IsPrincipalIdealRing R] [IsDomain R] [CharZero R] [LieRing L] [LieAlgebra R L] [LieRing A] [LieAlgebra R A] [Bracket L A] [Bracket A L] [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] [LieRingModule L V] [LieModule R L V] [LieRingModule A V] [LieModule R A V] [IsLieTower L A V] [IsLieTower A L V] (χ : A → R) : LieSubmodule R L V

The weight space of V with respect to χ : A → R, a priori a Lie submodule for A, is also a Lie submodule for L.

Equations

• LieModule.weightSpaceOfIsLieTower R V χ = { toSubmodule := ↑(LieModule.weightSpace V χ), lie_mem := ⋯ }

theorem LieModule.exists_nontrivial_weightSpace_of_lieIdeal {k : Type u_1} [Field k] {L : Type u_2} [LieRing L] [LieAlgebra k L] {V : Type u_3} [AddCommGroup V] [Module k V] [LieRingModule L V] [LieModule k L V] [CharZero k] [Module.Finite k V] [IsTriangularizable k L V] (A : LieIdeal k L) (hA : IsCoatom ↑A) (χ₀ : Module.Dual k ↥A) [Nontrivial ↥(weightSpace V ⇑χ₀)] : ∃ (χ : Module.Dual k L), Nontrivial ↥(weightSpace V ⇑χ)

theorem LieModule.exists_nontrivial_weightSpace_of_isSolvable (k : Type u_1) [Field k] (L : Type u_2) [LieRing L] [LieAlgebra k L] (V : Type u_3) [AddCommGroup V] [Module k V] [LieRingModule L V] [LieModule k L V] [CharZero k] [Module.Finite k V] [Nontrivial V] [LieAlgebra.IsSolvable L] [IsTriangularizable k L V] : ∃ (χ : Module.Dual k L), Nontrivial ↥(weightSpace V ⇑χ)

Lie's theorem: Lie modules of solvable Lie algebras over fields of characteristic 0 have a common eigenvector for the action of all elements of the Lie algebra.

See LieModule.exists_nontrivial_weightSpace_of_isNilpotent for the variant that assumes that L is nilpotent and drops the condition that k is of characteristic zero.