English
The lower central series computed in the quotient by an ideal I coincides with the lower central series computed in the quotient object L ⧸ I when viewed appropriately.
Русский
Нижняя центральная серия, вычисленная в фактор-пространстве по идеалу I, совпадает с той, что вычисляется в фактор-алгебре L ⧸ I.
LaTeX
$$LieSubmodule.toSubmodule (lowerCentralSeries R L (L ⧸ I) k) = LieSubmodule.toSubmodule (lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)$$
Lean4
/-- 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. -/
-- Porting note: added `LieSubmodule.toSubmodule` in the statement
theorem coe_lowerCentralSeries_ideal_quot_eq {I : LieIdeal R L} (k : ℕ) :
LieSubmodule.toSubmodule (lowerCentralSeries R L (L ⧸ I) k) =
LieSubmodule.toSubmodule (lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) :=
by
induction k with
| zero => simp only [LieModule.lowerCentralSeries_zero, LieSubmodule.top_toSubmodule]
| succ k ih =>
simp only [LieModule.lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span]
congr
ext x
constructor
· rintro ⟨⟨y, -⟩, ⟨z, hz⟩, rfl : ⁅y, z⁆ = x⟩
rw [← LieSubmodule.mem_toSubmodule, ih, LieSubmodule.mem_toSubmodule] at hz
exact ⟨⟨LieSubmodule.Quotient.mk y, LieSubmodule.mem_top _⟩, ⟨z, hz⟩, rfl⟩
· rintro ⟨⟨⟨y⟩, -⟩, ⟨z, hz⟩, rfl : ⁅y, z⁆ = x⟩
rw [← LieSubmodule.mem_toSubmodule, ← ih, LieSubmodule.mem_toSubmodule] at hz
exact ⟨⟨y, LieSubmodule.mem_top _⟩, ⟨z, hz⟩, rfl⟩
