English
For an ideal I in L, the derived series along I equals the comap of the derived series in the ambient Lie algebra: derivedSeries R I k = (derivedSeriesOfIdeal R L k I).comap I.incl.
Русский
Производный ряд по I равен обобщённой проекции в L через включение I: derivedSeries R I k = (derivedSeriesOfIdeal R L k I).comap I.incl.
LaTeX
$$$\text{derivedSeries}_R I(k) = \bigl(\text{derivedSeriesOfIdeal}(R, L, k, I)\bigr)^{\mathrm{comap}}$$$
Lean4
theorem derivedSeries_eq_derivedSeriesOfIdeal_comap (k : ℕ) :
derivedSeries R I k = (derivedSeriesOfIdeal R L k I).comap I.incl := by
induction k with
| zero => simp only [derivedSeries_def, comap_incl_self, derivedSeriesOfIdeal_zero]
| succ k ih =>
simp only [derivedSeries_def, derivedSeriesOfIdeal_succ] at ih ⊢; rw [ih]
exact comap_bracket_incl_of_le I (derivedSeriesOfIdeal_le_self I k) (derivedSeriesOfIdeal_le_self I k)
