map_lowerCentralSeries_le — Mathlib

English

For a LieModule homomorphism f, the image of the k-th lower central series is contained in the k-th lower central series of the target.

Русский

Гомоморфизм f сохраняет нижнюю центральную серию на каждом уровне: map(lcs_k(M)) ≤ lcs_k(M₂).

LaTeX

$$(lowerCentralSeries(R,L,M,k)).map f ≤ lowerCentralSeries(R,L,M₂,k)$$

Lean4

theorem map_lowerCentralSeries_le (f : M →ₗ⁅R,L⁆ M₂) :
    (lowerCentralSeries R L M k).map f ≤ lowerCentralSeries R L M₂ k := by
  induction k with
  | zero => simp only [lowerCentralSeries_zero, le_top]
  | succ k ih =>
    simp only [LieModule.lowerCentralSeries_succ, LieSubmodule.map_bracket_eq]
    exact LieSubmodule.mono_lie_right ⊤ ih

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