English
There exists a bound k such that the weight space is contained in a certain kernel described by the k-th power of a shifted endomorphism.
Русский
Существует предел k, для которого весовое пространство подмодуль заключено в ядро, описываемое через k-ю степень эндоморфа.
LaTeX
$$∃ k, genWeightSpace M χ ≤ ker ((toEnd R L M x − algebraMap R _ (χ x))^k)$$
Lean4
/-- See also `LieModule.iInf_lowerCentralSeries_eq_posFittingComp`. -/
theorem iSup_ucs_eq_genWeightSpace_zero [IsNoetherian R M] :
⨆ k, (⊥ : LieSubmodule R L M).ucs k = genWeightSpace M (0 : L → R) :=
by
obtain ⟨k, hk⟩ := (LieSubmodule.isNilpotent_iff_exists_self_le_ucs <| genWeightSpace M (0 : L → R)).mp inferInstance
refine le_antisymm (iSup_ucs_le_genWeightSpace_zero R L M) (le_trans hk ?_)
exact le_iSup (fun k ↦ (⊥ : LieSubmodule R L M).ucs k) k
