English
A central extension of nilpotent Lie algebras is nilpotent; more precisely, if I ≤ center(L) and L/I is nilpotent, then L is nilpotent.
Русский
Центральное расширение нильпотентных Ли-алгебр нильпотентно; если I ⊆ центр(L) и L/I нильпотентна, то L нильпотентна.
LaTeX
$$theorem LieAlgebra.nilpotent_of_nilpotent_quotient {I : LieIdeal R L} (h₁ : I ≤ center R L) (h₂ : IsNilpotent (L ⧸ I)) : IsNilpotent L$$
Lean4
/-- A central extension of nilpotent Lie algebras is nilpotent. -/
theorem nilpotent_of_nilpotent_quotient {I : LieIdeal R L} (h₁ : I ≤ center R L) (h₂ : IsNilpotent (L ⧸ I)) :
IsNilpotent L :=
by
suffices LieModule.IsNilpotent L (L ⧸ I) by exact LieModule.nilpotentOfNilpotentQuotient R L L h₁ this
simp only [LieRing.IsNilpotent, LieModule.isNilpotent_iff R] at h₂ ⊢
peel h₂ with k hk
simp [← LieSubmodule.toSubmodule_inj, coe_lowerCentralSeries_ideal_quot_eq, hk]
