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 := ⋯ }
Instances For
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]
[LieModule.IsTriangularizable k L V]
(A : LieIdeal k L)
(hA : IsCoatom ↑A)
(χ₀ : Module.Dual k ↥A)
[Nontrivial ↥(LieModule.weightSpace V ⇑χ₀)]
:
∃ (χ : Module.Dual k L), Nontrivial ↥(LieModule.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]
[LieModule.IsTriangularizable k L V]
:
∃ (χ : Module.Dual k L), Nontrivial ↥(LieModule.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.