English
If η is finite, the lower central series of the Pi-product equals the Pi of the lower central series of the components: lowerCentralSeries((i→Gs i)) n = pi i (lowerCentralSeries(Gs i) n).
Русский
Если η конечна, то нижняя центральная последовательность произведения по индексу равна произведению нижних центральных последовательностей факторов.
LaTeX
$$$\\lowerCentralSeries((i \\to Gs_i), n) = \\operatorname{pi}_{i}(\\lowerCentralSeries(Gs_i, n))$$$
Lean4
theorem lowerCentralSeries_pi_of_finite [Finite η] (n : ℕ) :
lowerCentralSeries (∀ i, Gs i) n = Subgroup.pi Set.univ fun i => lowerCentralSeries (Gs i) n :=
by
let pi := fun f : ∀ i, Subgroup (Gs i) => Subgroup.pi Set.univ f
induction n with
| zero => simp [pi_top]
| succ n ih =>
calc
lowerCentralSeries (∀ i, Gs i) n.succ = ⁅lowerCentralSeries (∀ i, Gs i) n, ⊤⁆ := rfl
_ = ⁅pi fun i => lowerCentralSeries (Gs i) n, ⊤⁆ := by rw [ih]
_ = ⁅pi fun i => lowerCentralSeries (Gs i) n, pi fun i => ⊤⁆ := by simp [pi, pi_top]
_ = pi fun i => ⁅lowerCentralSeries (Gs i) n, ⊤⁆ := (commutator_pi_pi_of_finite _ _)
_ = pi fun i => lowerCentralSeries (Gs i) n.succ := rfl
