derivedSeriesOfIdeal_baseChange — Mathlib

English

Under a base change A of R with a Lie algebra L, the k-th derived series commutes with base change: derivedSeriesOfIdeal A (A ⊗ L) k (I.baseChange A) = (derivedSeriesOfIdeal R L k I).baseChange A.

Русский

При смене основания A над R тройка сохраняет структуру: D_k(I.baseChange A) = (D_k I).baseChange A.

LaTeX

$$$\text{derivedSeriesOfIdeal}(A, A \otimes_R L, k, I^{\text{baseChange} A}) = (\text{derivedSeriesOfIdeal}(R, L, k, I)).baseChange A$$$

Lean4

@[simp]
theorem derivedSeriesOfIdeal_baseChange {A : Type*} [CommRing A] [Algebra R A] (k : ℕ) :
    derivedSeriesOfIdeal A (A ⊗[R] L) k (I.baseChange A) = (derivedSeriesOfIdeal R L k I).baseChange A := by
  induction k with
  | zero => simp
  | succ k ih => simp only [derivedSeriesOfIdeal_succ, ih, LieSubmodule.lie_baseChange]

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