English
Let f: L' → L be a surjective Lie algebra homomorphism. Then for every k ≥ 0, the k-th derived series commutes with f, i.e., the image of the k-th derived series of L' under f equals the k-th derived series of L.
Русский
Пусть f: L' → L — сюръективный гомоморфизм Ли. Тогда для каждого k ≥ 0 выполняется равенство: образ(k-th derived series(L')) = k-th derived series(L).
LaTeX
$$$\mathrm{derivedSeries}_R L' k \mathrm{map} f = \mathrm{derivedSeries}_R L k$$$
Lean4
theorem derivedSeries_map_eq (k : ℕ) (h : Function.Surjective f) : (derivedSeries R L' k).map f = derivedSeries R L k :=
by
induction k with
| zero =>
change (⊤ : LieIdeal R L').map f = ⊤
rw [← f.idealRange_eq_map]
exact f.idealRange_eq_top_of_surjective h
| succ k ih => simp only [derivedSeries_def, map_bracket_eq f h, ih, derivedSeriesOfIdeal_succ]
