lowerCentralSeries_eq_lcs_comap — Mathlib

English

The lower central series of a submodule N equals the comap under the inclusion map of the lcs of N: lcs_k(R,L,N) = comap N.incl (lcs_k N).

Русский

Нижняя центральная серия подмодуля N равна обратному образу по включению от lcs k самого N.

LaTeX

$$$\\operatorname{lcs}_k(R,L,N) = \\operatorname{comap}(N\\incl)(\\operatorname{lcs}_k N)$$$

Lean4

theorem lowerCentralSeries_eq_lcs_comap : lowerCentralSeries R L N k = (N.lcs k).comap N.incl := by
  induction k with
  | zero => simp
  | succ k ih =>
    simp only [lcs_succ, lowerCentralSeries_succ] at ih ⊢
    have : N.lcs k ≤ N.incl.range := by
      rw [N.range_incl]
      apply lcs_le_self
    rw [ih, LieSubmodule.comap_bracket_eq _ N.incl _ N.ker_incl this]

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