English
If η is finite, the commutator of the direct product over η of H and K equals the direct product of the commutators: [∏ H_i, ∏ K_i] = ∏ [H_i,K_i].
Русский
Пусть η конечна. Коммутатор прямого произведения по η подмножеств H и K равен прямому произведению коммутаторов: [∏ H_i, ∏ K_i] = ∏ [H_i,K_i].
LaTeX
$$$ [\\mathrm{Subgroup.pi} Set.univ H, \\mathrm{Subgroup.pi Set.univ} K] = \\mathrm{Subgroup.pi Set.univ} (\\lambda i, [H i, K i]) $$$
Lean4
/-- The commutator of a finite direct product is contained in the direct product of the commutators.
-/
theorem commutator_pi_pi_of_finite {η : Type*} [Finite η] {Gs : η → Type*} [∀ i, Group (Gs i)]
(H K : ∀ i, Subgroup (Gs i)) :
⁅Subgroup.pi Set.univ H, Subgroup.pi Set.univ K⁆ = Subgroup.pi Set.univ fun i => ⁅H i, K i⁆ := by
classical
apply le_antisymm (commutator_pi_pi_le H K)
rw [pi_le_iff]
intro i hi
rw [map_commutator]
apply commutator_mono <;>
· rw [le_pi_iff]
intro j _hj
rintro _ ⟨x, hx, rfl⟩
by_cases h : j = i
· subst h
simpa using hx
· simp [h, one_mem]
