English
Let G be a group and {H_i} a finite family of subgroups of G such that every pair of subgroups commutes elementwise (i.e., any x ∈ H_i and y ∈ H_j commute). Then there exists a canonical homomorphism from the external direct product ∏_{i} H_i into G, which on the i-th factor is the inclusion H_i ↪ G; equivalently, the product map (h_i) ↦ ∏ h_i is a well-defined homomorphism because the factors commute.
Русский
Пусть G — группа и {H_i} — конечное семейство подгрупп под G так, что любые элементы из разных подгрупп коммутируют. Тогда существует каноничный гомоморфизм из внешнего прямого произведения ∏_{i} H_i в G, который на i-м факторе является вложением H_i в G; эквивалентно, отображение (h_i) ↦ ∏_i h_i определено как однородный гомоморфизм, потому что элементы из разных факторов commute.
LaTeX
$$$\text{Let } G \text{ be a group and } \{H_i \}_{i \in \iota} \text{ a finite family of subgroups of } G \text{ with } x \in H_i, y \in H_j \Rightarrow [x,y]=1. \\ \text{Then there exists a canonical homomorphism } \phi: \prod_{i\in \iota} H_i \to G \text{ such that } \phi|_{H_i} = \iota_i. \\ \text{Equivalently } \phi((h_i)_{i}) = \prod_{i\in \iota} h_i \text{ (order irrelevant by commutativity).}$$$
Lean4
/-- The canonical homomorphism from a family of subgroups where elements from different subgroups
commute -/
@[to_additive /-- The canonical homomorphism from a family of additive subgroups where elements from
different subgroups commute -/
]
def noncommPiCoprod (hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i → y ∈ H j → Commute x y) :
(∀ i : ι, H i) →* G :=
MonoidHom.noncommPiCoprod (fun i => (H i).subtype) (commute_subtype_of_commute hcomm)
