English
For a LieIdeal I of a Lie algebra L acting on a module M, the k-th term of the lower central series is defined by repeatedly bracketing with I: I.lcs M k = ⎧ bracket with I applied k times to ⊤ ⎫.
Русский
ДляLie-идеала I в Lie-алгебре L, действующего на модуль M, k-й член нижней центральной серии определяется повторными скобками с I: I.lcs M k = ⊤ под действием I скобками, применённое k раз.
LaTeX
$$$I.lcs M k = (\,[I, -]\,)^k \top$$$
Lean4
/-- Given a Lie module `M` over a Lie algebra `L` together with an ideal `I` of `L`, this is the
lower central series of `M` as an `I`-module. The advantage of using this definition instead of
`LieModule.lowerCentralSeries R I M` is that its terms are Lie submodules of `M` as an
`L`-module, rather than just as an `I`-module.
See also `LieIdeal.coe_lcs_eq`. -/
def lcs : LieSubmodule R L M :=
(fun N => ⁅I, N⁆)^[k] ⊤
