Theorems · Theorem · nonassociative algebras

coe_lowerCentralSeries_ideal_quot_eq

∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {I : LieIdeal R L}
  (k : ℕ), ↑(LieModule.lowerCentralSeries R L (L ⧸ I) k) = ↑(LieModule.lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)

Given an ideal I of a Lie algebra L, the lower central series of L ⧸ I is the same whether we regard L ⧸ I as an L module or an L ⧸ I module. TODO: This result obviously generalises but the generalisation requires the missing definition of morphisms between Lie modules over different Lie algebras.

Defined in

Mathlib.Algebra.Lie.Nilpotent

Cited by

1 results in Mathlib

Foundations

Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingLieRingLieAlgebra