Name for map from pi group

Stream: general

[Joachim Breitner]

/poll https://github.com/leanprover-community/mathlib/pull/11744 defines the map (Π (i : I), N i) →* M given maps N i →* M with commuting ranges. What should be the name of this construction, and where should it live?
monoid_hom.copi, analogous to monoid_hom.coprod
monoid_hom.comm_coprod, to avoid the odd copi and hint at the commutativity assumption (but possibly confusing pi with × here)

[Joachim Breitner]

The kind of yak shaving needed to get stuff in… :-)
Sorry for the messed up syntax.

[Joachim Breitner]

See this Github thread for the discussion so far

[Yaël Dillies]

You can always edit the poll name! #11744 for the lazy

[Eric Wieser]

I think it should be noncomm not comm to match docs#finset.noncomm_prod`

[Eric Wieser]

Just to check - you do actually care about the case where the destination monoid is not itself commutative, right?

[Reid Barton]

It's the "commutative coproduct" in the sense that the factors commute, which they would not do in the actual coproduct. BTW I has to be finite, right?

[Eric Wieser]

Right, but docs#finset.noncomm_prod is also the "commutative product", so I think the names should match one way or the other

[Eric Wieser]

Doing the rename the other way around also seems fine to me

[Junyan Xu]

In analogy to free_product.lift it could also be called comm_free_product.lift.

[Eric Wieser]

I don't think monoid_hom.comm_coprod is a good choice, because that seems like the name we'd use for a version of docs#monoid_hom.coprod that takes commute assumptions instead of comm_monoid P

[Eric Wieser]

Perhaps *_pi_coprod or *_coprod_pi, which sort of matches how we named docs#pi_tensor_prod?

[Reid Barton]

Yeah there is a minor but annoying mismatch where in ordinary math, we don't make such a fuss about the difference between binary products and arbitrary products, while in category theory, the term "pi" has a distinct (but related) meaning.

[Joachim Breitner]

The poll was inconclusive. I updated the PR to call the main definition monoid_hom.nonocomm_pi_coprod, hoping we can make progress here.