English
In a solvable/polynomially vanishing context, there exists a nontrivial weight space for a finite-dimensional module.
Русский
В разрешимом контексте существует ненулевое весовое пространство для конечномерного модуля.
LaTeX
$$$\\exists χ: Weight\\;k\\;L\\;M,\\; weightSpace(M,χ) \\neq 0.$$$
Lean4
/-- See `LieModule.exists_nontrivial_weightSpace_of_isSolvable` for the variant that
only assumes that `L` is solvable but additionally requires `k` to be of characteristic zero. -/
theorem exists_nontrivial_weightSpace_of_isNilpotent [Field k] [LieAlgebra k L] [Module k M] [Module.Finite k M]
[LieModule k L M] [LinearWeights k L M] [IsTriangularizable k L M] [Nontrivial M] :
∃ χ : Module.Dual k L, Nontrivial (weightSpace M χ) :=
by
obtain ⟨χ⟩ : Nonempty (Weight k L M) := by
by_contra! contra
simpa only [iSup_of_empty, bot_ne_top] using LieModule.iSup_genWeightSpace_eq_top' k L M
obtain ⟨m, hm₀, hm⟩ := exists_forall_lie_eq_smul k L M χ
simp only [LieSubmodule.nontrivial_iff_ne_bot, LieSubmodule.eq_bot_iff, ne_eq, not_forall]
exact ⟨χ.toLinear, m, by simpa [mem_weightSpace], hm₀⟩
