isNilpotent_toEnd_genWeightSpace_zero

English

There is a correspondence between weight spaces and their generating eigenvalues in the nilpotent setting.

Русский

Существует соответствие между весовыми пространствами и их порождающими собственными значениямии в нильпотентной обстановке.

LaTeX

$$Weight space connections: genWeightSpace$$

Lean4

/-- A (nilpotent) Lie algebra acts nilpotently on the zero weight space of a Noetherian Lie
module. -/
theorem isNilpotent_toEnd_genWeightSpace_zero [IsNoetherian R M] (x : L) :
    _root_.IsNilpotent <| toEnd R L (genWeightSpace M (0 : L → R)) x := by
  simpa using isNilpotent_toEnd_sub_algebraMap M (0 : L → R) x

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