English
If x acts nilpotently on M via a Lie action, and I acts nilpotently on M, with hxI ensuring the span of x and I is the whole space, then L acts nilpotently on M.
Русский
Если элемент x действует нильпотентно на M и I также нильпотентен на M, и span{x} ∪ I охватывает всю структуру, то L действует нильпотентно на M.
LaTeX
$$isNilpotentOfIsNilpotentSpanSupEqTop (hnp : IsNilpotent <| toEnd R L M x) (hIM : IsNilpotent I M) : IsNilpotent L M.$$
Lean4
theorem isNilpotentOfIsNilpotentSpanSupEqTop (hnp : IsNilpotent <| toEnd R L M x) (hIM : IsNilpotent I M) :
IsNilpotent L M := by
obtain ⟨n, hn⟩ := hnp
obtain ⟨k, hk⟩ := IsNilpotent.nilpotent R I M
have hk' : I.lcs M k = ⊥ := by simp only [← toSubmodule_inj, I.coe_lcs_eq, hk, bot_toSubmodule]
suffices ∀ l, lowerCentralSeries R L M (l * n) ≤ I.lcs M l
by
rw [isNilpotent_iff R]
use k * n
simpa [hk'] using this k
intro l
induction l with
| zero => simp
| succ l ih => exact (l.succ_mul n).symm ▸ lcs_le_lcs_of_is_nilpotent_span_sup_eq_top hxI hn ih
