Theorems · Definition · nonassociative algebras

LieSubmodule.lcs

{R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] → [inst_5 : LieRingModule L M] → ℕ → LieSubmodule R L M → LieSubmodule R L M

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.

Defined in

Mathlib.Algebra.Lie.Nilpotent

Cited by

12 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Quot.sound

Assumes

CommRingLieRingLieAlgebraAddCommGroupModuleLieRingModule