exists_genWeightSpace_zero_le_ker_of_isNoetherian

English

By Engel’s theorem, the zero weight space of a Noetherian Lie module is nilpotent as a Lie algebra module.

Русский

По теореме Энгеля нулевое весовое пространство является нильпотентным как модуль над Ли-алгеброй.

LaTeX

$$[IsNoetherian R M] ⇒ IsNilpotent L (genWeightSpace M (0 : L → R))$$

Lean4

theorem exists_genWeightSpace_zero_le_ker_of_isNoetherian [IsNoetherian R M] (x : L) :
    ∃ k : ℕ, genWeightSpace M (0 : L → R) ≤ LinearMap.ker (toEnd R L M x ^ k) := by
  simpa using exists_genWeightSpace_le_ker_of_isNoetherian M (0 : L → R) x

Похожие утверждения