isNilpotent_iff_exists_ucs_eq_top

English

For a Lie module L over a Noetherian ring, nilpotence of the module is equivalent to the existence of a level k such that the k-th upper central submodule equals the whole module.

Русский

Для модуля Ли над кольцом Ноетерова равносильность: нильпотентность эквивалентна существованию уровня k с верхней центральной серией, равной всей модуле.

LaTeX

$$$\text{LieModule.IsNilpotent } L M \iff \exists k, (\perp) .ucs_k(\text{LieSubmodule.instBot.bot}) = \top$$$

Lean4

theorem _root_.LieModule.isNilpotent_iff_exists_ucs_eq_top :
    LieModule.IsNilpotent L M ↔ ∃ k, (⊥ : LieSubmodule R L M).ucs k = ⊤ := by rw [LieModule.isNilpotent_iff R];
  exact exists_congr fun k => by simp [ucs_eq_top_iff]

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