English
There is an equivalence between the type of pairwise-commuting families of monoid homomorphisms and the monoid homomorphisms from the product, via noncommPiCoprod.
Русский
Существует эквивалентность между семейством гомоморфизмов с попарно коммутируемыми образами и гомоморфизмами из произведения, через noncommPiCoprod.
LaTeX
$$$\\text{noncommPiCoprodEquiv} : (\\{\\varphi : \\prod_i N_i \\to M \\\\;|\\; \\text{Pairwise commuting}) \\simeq ((\\prod_i N_i) \\to M).$$$
Lean4
@[to_additive]
theorem noncommPiCoprod_apply (h : (i : ι) → N i) :
MonoidHom.noncommPiCoprod ϕ hcomm h =
Finset.noncommProd Finset.univ (fun i ↦ ϕ i (h i))
(Pairwise.set_pairwise (fun ⦃i j⦄ a ↦ hcomm a (h i) (h j)) _) :=
by dsimp only [MonoidHom.noncommPiCoprod, MonoidHom.coe_mk, OneHom.coe_mk]
