English
Lie's theorem: if L is solvable and acts triangularizably on V over a field k of characteristic zero, there exists a nontrivial weight space for some χ ∈ Dual(k,L).
Русский
Ли‑теорема: если L разрешима и действует треугольно над V над полем k нулевой характеристики, то существует ненулевое весовое пространство для некоторого χ ∈ Dual(k,L).
LaTeX
$$$\\exists \\chi \\in \\operatorname{Dual}(k,L): \\operatorname{Nontrivial}(\\operatorname{weightSpace}(V,\\chi)).$$$
Lean4
/-- **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. -/
theorem exists_nontrivial_weightSpace_of_isSolvable [IsSolvable L] [LieModule.IsTriangularizable k L V] :
∃ χ : Module.Dual k L, Nontrivial (weightSpace V χ) :=
by
let imL := (toEnd k L V).range
let toEndo : L →ₗ[k] imL :=
LinearMap.codRestrict imL.toSubmodule (toEnd k L V)
(fun x ↦ LinearMap.mem_range.mpr ⟨x, rfl⟩ : ∀ x : L, (toEnd k L V) x ∈ imL)
have ⟨χ, h⟩ := exists_forall_lie_eq_smul_of_isSolvable_of_finite k V imL
use χ.comp toEndo
obtain ⟨⟨v, hv⟩, hv0⟩ := exists_ne (0 : weightSpace V χ)
refine nontrivial_of_ne ⟨v, ?_⟩ 0 ?_
· rw [mem_weightSpace] at hv ⊢
intro x
apply hv (toEndo x)
· simpa using hv0
