map_lowerCentralSeries_eq — Mathlib

English

If the endomorphism f is surjective, then the image of the k-th LCS equals the k-th LCS of the target.

Русский

При сюръективности f выполняется равенство: map(lcs_k(M)) = lcs_k(M₂).

LaTeX

$$lowerCentralSeries_k.map f = lowerCentralSeries_k$$

Lean4

theorem map_lowerCentralSeries_eq {f : M →ₗ⁅R,L⁆ M₂} (hf : Function.Surjective f) :
    (lowerCentralSeries R L M k).map f = lowerCentralSeries R L M₂ k :=
  by
  apply le_antisymm (map_lowerCentralSeries_le k f)
  induction k with
  | zero => rwa [lowerCentralSeries_zero, lowerCentralSeries_zero, top_le_iff, f.map_top, f.range_eq_top]
  | succ =>
    simp only [lowerCentralSeries_succ, LieSubmodule.map_bracket_eq]
    apply LieSubmodule.mono_lie_right
    assumption

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