Naming mess

Stream: maths

[Patrick Massot]

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 $f$ and $g$, one going from $X$ to $Y \times Z$ and the other one from $X \times X$ to $Y \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]

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]

/poll What should we normalize to?

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

[Anne Baanen]

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]

This is awkward in ordinary math too

[Reid Barton]

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]

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

[Patrick Massot]

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]

Maybe putting a _diag somewhere would help disambiguate too?

[Yaël Dillies]

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]

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]

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]

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]

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]

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

[Vincent Beffara]

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

[Yaël Dillies]

but not docs#finset.card_doubleton

[Eric Wieser]

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