lowerCentralSeries_tensor_eq_baseChange

English

Base change commutes with lower central series: lowerCentralSeries_A (A⊗R L) (A⊗R M) k = (lowerCentralSeries_R L M k).baseChange A.

Русский

Базовое изменение совместимо с нижней центральной серией: lowerCentralSeries_A ... = baseChange A (lowerCentralSeries_R L M k).

LaTeX

$$$\operatorname{lowerCentralSeries} A (A \otimes_R L) (A \otimes_R M) k = (\operatorname{lowerCentralSeries} R L M k).\text{baseChange } A$$$

Lean4

@[simp]
theorem lowerCentralSeries_tensor_eq_baseChange (k : ℕ) :
    lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) k = (lowerCentralSeries R L M k).baseChange A := by
  induction k with
  | zero => simp
  | succ k ih => simp only [lowerCentralSeries_succ, ih, ← baseChange_top, lie_baseChange]

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