English
For a Lie submodule N ⊆ M, the lcs operation defines a generalized lower central series by iterating the map N ↦ [⊤, N], with k steps.
Русский
Для подмодуля Ли N ⊆ M операция lcs задаёт обобщённую нижнюю централную серию путём повторения отображения N ↦ [⊤, N] k раз.
LaTeX
$$$\\text{lcs}_k(N) = (\\,N \\mapsto [\\,\\top, N\\]\,)^{[k]}(N).$$$
Lean4
/-- A generalisation of the lower central series. The zeroth term is a specified Lie submodule of
a Lie module. In the case when we specify the top ideal `⊤` of the Lie algebra, regarded as a Lie
module over itself, we get the usual lower central series of a Lie algebra.
It can be more convenient to work with this generalisation when considering the lower central series
of a Lie submodule, regarded as a Lie module in its own right, since it provides a type-theoretic
expression of the fact that the terms of the Lie submodule's lower central series are also Lie
submodules of the enclosing Lie module.
See also `LieSubmodule.lowerCentralSeries_eq_lcs_comap` and
`LieSubmodule.lowerCentralSeries_map_eq_lcs` below, as well as `LieSubmodule.ucs`. -/
def lcs : LieSubmodule R L M → LieSubmodule R L M :=
(fun N => ⁅(⊤ : LieIdeal R L), N⁆)^[k]
