English
There is an inequality comparing the lower central series when passing to a quotient by an ideal I; the image under the natural map is contained in the LCS of the ambient Lie algebra.
Русский
Существует неравенство нижней центральной серии после quotient по идеалу I; образ под естественного отображения содержится в LCS над окружной алгеброй.
LaTeX
$$theorem coe_lowerCentralSeries_ideal_le {I : LieIdeal R L} (k : ℕ) :$$
Lean4
/-- Note that the below inequality can be strict. For example the ideal of strictly-upper-triangular
2x2 matrices inside the Lie algebra of upper-triangular 2x2 matrices with `k = 1`. -/
-- Porting note: added `LieSubmodule.toSubmodule` in the statement
theorem coe_lowerCentralSeries_ideal_le {I : LieIdeal R L} (k : ℕ) :
LieSubmodule.toSubmodule (lowerCentralSeries R I I k) ≤ lowerCentralSeries R L I k := by
induction k with
| zero => simp
| succ k ih =>
simp only [LieModule.lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span]
apply Submodule.span_mono
rintro x ⟨⟨y, -⟩, ⟨z, hz⟩, rfl : ⁅y, z⁆ = x⟩
exact ⟨⟨y.val, LieSubmodule.mem_top _⟩, ⟨z, ih hz⟩, rfl⟩
