ucs_comap_incl — Mathlib

English

Composing upper central series with inclusion preserves the expected equality: the comap of N along inclusion with ⊥.ucs(k) equals ⊥.ucs(k) in the ambient module.

Русский

Образ обратного образа по включению с граничной степенью верхней центральной серии сохраняет равенство с нижним модулем.

LaTeX

$$$( (\perp : LieSubmodule R L M).\\mathrm{ucs}(k)).\\mathrm{comap} N.inlc = (\\perp : LieSubmodule R L N).\\mathrm{ucs}(k)$$

Lean4

theorem ucs_comap_incl (k : ℕ) : ((⊥ : LieSubmodule R L M).ucs k).comap N.incl = (⊥ : LieSubmodule R L N).ucs k := by
  induction k with
  | zero => exact N.ker_incl
  | succ k ih => simp [← ih]

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