Zulip Chat Archive

Stream: general

Topic: Name for map from pi group


Joachim Breitner (Feb 13 2022 at 17:49):

/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 (Feb 13 2022 at 17:50):

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

Joachim Breitner (Feb 13 2022 at 17:50):

See this Github thread for the discussion so far

Yaël Dillies (Feb 13 2022 at 18:00):

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

Eric Wieser (Feb 13 2022 at 23:14):

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

Eric Wieser (Feb 13 2022 at 23:16):

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

Reid Barton (Feb 13 2022 at 23:31):

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 (Feb 13 2022 at 23:39):

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 (Feb 13 2022 at 23:40):

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

Junyan Xu (Feb 14 2022 at 01:34):

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

Eric Wieser (Feb 14 2022 at 08:49):

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 (Feb 14 2022 at 08:49):

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

Reid Barton (Feb 14 2022 at 10:52):

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 (Feb 15 2022 at 12:28):

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


Last updated: Dec 20 2023 at 11:08 UTC