derivedSeries_le_lowerCentralSeries

English

For the derived series of R,L on M, every term is contained in the corresponding lower central series term on the same module: derived_k ≤ lcs_k.

Русский

Производная серия удовлетворяет: derived_k ≤ lcs_k.

LaTeX

$$$derivedSeries(R,L,M,k) \\le lcs(R,L,M,k)$$$

Lean4

theorem derivedSeries_le_lowerCentralSeries (k : ℕ) : derivedSeries R L k ≤ lowerCentralSeries R L L k := by
  induction k with
  | zero => rw [derivedSeries_def, derivedSeriesOfIdeal_zero, lowerCentralSeries_zero]
  | succ k h =>
    have h' : derivedSeries R L k ≤ ⊤ := by simp only [le_top]
    rw [derivedSeries_def, derivedSeriesOfIdeal_succ, lowerCentralSeries_succ]
    exact LieSubmodule.mono_lie h' h

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