English
Let R be a commutative ring and L, L' be Lie algebras over R. If f: L → L' is a surjective Lie algebra homomorphism, then for every k ≥ 0 the image of the k-th term of the lower central series of L equals the k-th term of the lower central series of L'.
Русский
Пусть R — коммутативный кольцо, L и L' — алгебры Ли над R. Если f: L → L' — сюръективное гомоморфизм Ли, то для каждого k ≥ 0 образ k-й члены нижней центральной серии L совпадает с k-й членом нижней центральной серии L'.
LaTeX
$$$\operatorname{LieIdeal.map} f (\operatorname{lowerCentralSeries} R L L k) = \operatorname{lowerCentralSeries} R L' L' k$$$
Lean4
theorem lowerCentralSeries_map_eq (k : ℕ) {f : L →ₗ⁅R⁆ L'} (h : Function.Surjective f) :
LieIdeal.map f (lowerCentralSeries R L L k) = lowerCentralSeries R L' L' k :=
by
have h' : (⊤ : LieIdeal R L).map f = ⊤ := by
rw [← f.idealRange_eq_map]
exact f.idealRange_eq_top_of_surjective h
induction k with
| zero => simp only [LieModule.lowerCentralSeries_zero]; exact h'
| succ k ih => simp only [LieModule.lowerCentralSeries_succ, LieIdeal.map_bracket_eq f h, ih, h']
