English
Under Noetherian and linear weights, there exists a weight χ in the dual such that the weight space is nontrivial.
Русский
При отсутствии ненулевых граничений и линейных весов существует вес χ в двойственном, для которого весовое пространство ненулево.
LaTeX
$$$\\exists χ: \\mathrm{Module.Dual}(k,L) \\text{ s.t. weightSpace}(M, χ) \\neq 0.$$$
Lean4
/-- Given a Lie module `M` of a nilpotent Lie algebra `L` with coefficients in `R`,
if a function `χ : L → R` has a simultaneous generalized eigenvector for the action of `L`
then it has a simultaneous true eigenvector, provided `M` is Noetherian and has linear weights. -/
theorem exists_forall_lie_eq_smul [LinearWeights R L M] [IsNoetherian R M] (χ : Weight R L M) :
∃ m : M, m ≠ 0 ∧ ∀ x : L, ⁅x, m⁆ = χ x • m :=
by
replace hχ : Nontrivial (shiftedGenWeightSpace R L M χ) :=
(LieSubmodule.nontrivial_iff_ne_bot R L M).mpr χ.genWeightSpace_ne_bot
obtain ⟨⟨⟨m, _⟩, hm₁⟩, hm₂⟩ := @exists_ne _ (nontrivial_max_triv_of_isNilpotent R L (shiftedGenWeightSpace R L M χ)) 0
simp_rw [mem_maxTrivSubmodule, Subtype.ext_iff, ZeroMemClass.coe_zero] at hm₁
refine ⟨m, by simpa [LieSubmodule.mk_eq_zero] using hm₂, ?_⟩
intro x
have := hm₁ x
rwa [coe_lie_shiftedGenWeightSpace_apply, sub_eq_zero] at this
