isNilpotent_quotient_iff — Mathlib

English

The quotient M/N is nilpotent if and only if there exists a natural number k such that the k-th term of the lower central series of M lies inside N.

Русский

Фактор-модуль M/N нильпотентен тогда и только тогда, когда существует число k, для которого k-й элемент нижней центральной серии M лежит внутри N.

LaTeX

$$$\\operatorname{IsNilpotent}_L\\bigl(M/N\\bigr) \\iff \\exists k \\; (\\lowerCentralSeries_R L M k \\le N).$$$

Lean4

theorem isNilpotent_quotient_iff : IsNilpotent L (M ⧸ N) ↔ ∃ k, lowerCentralSeries R L M k ≤ N :=
  by
  rw [isNilpotent_iff R L]
  refine exists_congr fun k ↦ ?_
  rw [← LieSubmodule.Quotient.map_mk'_eq_bot_le, map_lowerCentralSeries_eq k (LieSubmodule.Quotient.surjective_mk' N)]

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