English
Let R be a commutative ring, L and L' be Lie algebras over R, and f: L' → L a Lie algebra homomorphism. Then for every k ≥ 0, f maps the k-th derived series of L' into the k-th derived series of L, i.e., f(derivedSeries_R(L', k)) ⊆ derivedSeries_R(L, k).
Русский
Пусть R — коммутативное кольцо, L и L' — Ли-алгебры над R, и f: L' → L — гомоморфизм Ли. Тогда для каждого k ≥ 0 отображение f отправляет k-ю производящую серию L' в k-ю производящую серию L: f(derivedSeries_R(L', k)) ⊆ derivedSeries_R(L, k).
LaTeX
$$$f\bigl( \mathrm{derivedSeries}_{R} L' k \bigr) \subseteq \mathrm{derivedSeries}_{R} L k$$$
Lean4
theorem derivedSeries_map_le (k : ℕ) : (derivedSeries R L' k).map f ≤ derivedSeries R L k := by
induction k with
| zero => simp only [derivedSeries_def, derivedSeriesOfIdeal_zero, le_top]
| succ k ih =>
simp only [derivedSeries_def, derivedSeriesOfIdeal_succ] at ih ⊢
exact le_trans (map_bracket_le f) (LieSubmodule.mono_lie ih ih)
