English
Let H = (H i) and K = (K i) be subgroups of the groups G i in a direct product indexed by η. Then the commutator of the two subgroups ∏ i H i and ∏ i K i is contained in the direct product of the componentwise commutators, i.e. [∏ i H i, ∏ i K i] ≤ ∏ i [H i, K i].
Русский
Пусть H = (H_i) и K = (K_i) — подгруппы групп G_i в прямом произведении индексируемым множеством η. Тогда коммутатор подгрупп ∏ i H_i и ∏ i K_i содержится в прямом произведении компонентных коммутаторов: [∏ i H_i, ∏ i K_i] ≤ ∏ i [H_i, K_i].
LaTeX
$$$ [\\mathrm{Subgroup.pi} \\ Set.univ H, \\mathrm{Subgroup.pi} \\ Set.univ K] \\le \\mathrm{Subgroup.pi} Set.univ (\\lambda i, [H i, K i]) $$$
Lean4
/-- The commutator of direct product is contained in the direct product of the commutators.
See `commutator_pi_pi_of_finite` for equality given `Fintype η`.
-/
theorem commutator_pi_pi_le {η : Type*} {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⁆ :=
commutator_le.mpr fun _p hp _q hq i hi => commutator_mem_commutator (hp i hi) (hq i hi)
