instIsNilpotentSubtypeMemLieSubmoduleOfIsNoetherian

English

Under Engel's theorem in Noetherian setting, the shifted action on a nilpotent Lie algebra yields a nilpotent Lie module.

Русский

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

LaTeX

$$$\\text{IsNilpotent } L (\\mathrm{shiftedGenWeightSpace}(R,L,M,χ)).$$$

Lean4

/-- By Engel's theorem, if `M` is Noetherian, the shifted action `⁅x, m⁆ - χ x • m` makes the
`χ`-weight space into a nilpotent Lie module. -/
instance [IsNoetherian R M] : IsNilpotent L (shiftedGenWeightSpace R L M χ) :=
  LieModule.isNilpotent_iff_forall'.mpr fun x ↦ isNilpotent_toEnd_sub_algebraMap M χ x

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