Zulip Chat Archive

Stream: maths

Topic: Naming mess


Patrick Massot (Apr 04 2022 at 13:29):

We really need to work on naming consistency with products. Given $$f \co X \to Y$$ and $$g \co X \to Z$$ there are two maps that could be called the product of ff and gg, one going from XX to Y×ZY \times Z and the other one from X×XX \times X to Y×ZY \times Z. I already pointed out the inconsistency between docs#continuous_linear_map.prod_map and docs#continuous_linear_equiv.prod. I just discovered (or rediscovered) that we have docs#continuous.prod_mk and docs#continuous_on.prod.

Patrick Massot (Apr 04 2022 at 13:30):

I think that prod_mk and prod_map are unambiguous, and prod can mean one or the other, switching even for very very closely related notions.

Patrick Massot (Apr 04 2022 at 13:32):

/poll What should we normalize to?

  • prod and prod_map
  • prod_mk and prod_map
  • prod_mk and prod

Anne Baanen (Apr 04 2022 at 13:36):

I have a slight preference for prod f g : X → Y × Z to match docs#monoid_hom.prod and docs#linear_map.prod.

Reid Barton (Apr 04 2022 at 13:38):

This is awkward in ordinary math too

Reid Barton (Apr 04 2022 at 13:49):

I always feel a bit guilty about calling the map X -> Y x Z the "product", while I obviously don't feel guilty about talking about the product X x X -> Y x Z (or W x X -> Y x Z).

Patrick Massot (Apr 04 2022 at 13:55):

Clearly the one that feels fonctorial is (x,y)(f  x,g  y)(x, y) \mapsto (f\; x, g\; y), and the other one is obtained by precomposing with the diagonal embedding.

Patrick Massot (Apr 04 2022 at 13:56):

The issue is that the map itself cannot be called prod because this is already used. And indeed it is called docs#prod.map

Yaël Dillies (Apr 04 2022 at 14:01):

Maybe putting a _diag somewhere would help disambiguate too?

Yaël Dillies (Apr 04 2022 at 14:04):

Does it happen that some bundled maps X → Y × Z can't be composed from diag : X → X × X (with the correct decoration) and some map X × X → Y × Z?

Reid Barton (Apr 04 2022 at 14:06):

X → Y × Z is also the thing that comes from the universal property of the product, which is exactly the role of prod.mk.

Eric Wieser (Apr 04 2022 at 19:24):

Anne Baanen said:

I have a slight preference for prod f g : X → Y × Z to match docs#monoid_hom.prod and docs#linear_map.prod.

I'd be happy to have those renamed to whatever we decide

Vincent Beffara (Apr 07 2022 at 07:42):

I have another candidate: docs#measure_theory.ae_eq_fun.pair exists so that could have

pair : (X  Y) × (X  Z)  (X  Y × Z)

(or alternatively, rename measure_theory.ae_eq_fun.pair to something involving prod in the name). At least pair is not ambiguous, as it would feel to make no sense to use the name for the X × X → Y × Z version.

Eric Wieser (Apr 07 2022 at 08:06):

Pair seems weird to me, if we were going to use that word at all I'd argue we should have just called the type prod that (like C++)

Eric Wieser (Apr 07 2022 at 08:07):

Does docs#pair reveal many other declarations using that naming?

Vincent Beffara (Apr 07 2022 at 08:12):

Essentially none except for docs#Set.pair and a few things involving {a,b}

Yaël Dillies (Apr 07 2022 at 08:14):

but not docs#finset.card_doubleton

Eric Wieser (Apr 07 2022 at 09:09):

I think pair as a canonical spelling for insert a (singleton b) (aka {a, b}) is a nicer choice than doubleton


Last updated: Dec 20 2023 at 11:08 UTC