map_lowerCentralSeries_le — Mathlib

English

For a Lie algebra homomorphism f:L→L' and an inclusion g:M→M', the map of the lower central series of L,M is contained in the lower central series of L',M'.

Русский

При гомоморфизме f и включении g отображение нижней центральной серии сохраняется в нижнюю центральную серию цели.

LaTeX

$$theorem LieIdeal.map_lowerCentralSeries_le (k : ℕ) {f : L →ₗ⁅R⁆ L'} :$$

Lean4

theorem map_lowerCentralSeries_le (k : ℕ) {f : L →ₗ⁅R⁆ L'} :
    LieIdeal.map f (lowerCentralSeries R L L k) ≤ lowerCentralSeries R L' L' k := by
  induction k with
  | zero => simp only [LieModule.lowerCentralSeries_zero, le_top]
  | succ k ih =>
    simp only [LieModule.lowerCentralSeries_succ]
    exact le_trans (LieIdeal.map_bracket_le f) (LieSubmodule.mono_lie le_top ih)

Похожие утверждения