English
Let N be a Lie submodule on which the Lie algebra acts trivially. If the quotient M/N is nilpotent (as an L-module), then M is nilpotent (as an L-module).
Русский
Пусть N — подмодуль Ли-алгебры, по которому действие алгебры тривиально; если фактор-модуль M/N нильпотентен относительно L, то и M нильпотентен относительно L.
LaTeX
$$$\\bigl(N \\le \\maxTrivSubmodule(R,L,M)\\bigr) \\land \\operatorname{IsNilpotent}_L\\bigl(M/N\\bigr) \\Rightarrow \\operatorname{IsNilpotent}_L(M).$$$
Lean4
/-- If the quotient of a Lie module `M` by a Lie submodule on which the Lie algebra acts trivially
is nilpotent then `M` is nilpotent.
This is essentially the Lie module equivalent of the fact that a central
extension of nilpotent Lie algebras is nilpotent. See `LieAlgebra.nilpotent_of_nilpotent_quotient`
below for the corresponding result for Lie algebras. -/
theorem nilpotentOfNilpotentQuotient {N : LieSubmodule R L M} (h₁ : N ≤ maxTrivSubmodule R L M)
(h₂ : IsNilpotent L (M ⧸ N)) : IsNilpotent L M :=
by
rw [isNilpotent_iff R L] at h₂ ⊢
obtain ⟨k, hk⟩ := h₂
use k + 1
simp only [lowerCentralSeries_succ]
suffices lowerCentralSeries R L M k ≤ N
by
replace this := LieSubmodule.mono_lie_right ⊤ (le_trans this h₁)
rwa [ideal_oper_maxTrivSubmodule_eq_bot, le_bot_iff] at this
rw [← LieSubmodule.Quotient.map_mk'_eq_bot_le, ← le_bot_iff, ← hk]
exact map_lowerCentralSeries_le k (LieSubmodule.Quotient.mk' N)
