(f, g) vs (f ×ₘ g)

Stream: new members

[Klaus Gy]

I'm a bit confused about the use of ×ₘ for the pair (f, g). The docstring says

Construct a morphism in a product category by giving its constituent components.
This constructor should be preferred over Prod.mk, because lean infers better the
source and target of the resulting morphism.

but why is it then not used in e.g. Mathlib/CategoryTheory/Functor/Currying.lean? Also, why does the simp lemma prod_comp simplify to (f.1 ≫ g.1, f.2 ≫ g.2) and not to (f.1 ≫ g.1 ×ₘ f.2 ≫ g.2), would it make any difference?

I'm not 100% sure but I think it makes a difference and the reason why stuff like rw[← curryObj] does't work in my current project is that curryObj doesn't use ×ₘ but I am.

Ah, nvm, I think the last line is not true. So it's probably just cosmetics, but still curious what difference it makes and when we should use ×ₘ, because some of my terms only type check when using ×ₘ, so I assume there is something deeper going on?

[Robert Maxton]

The fact that some of your terms only type check when using ×ₘ is precisely what the docstring means when it says that "lean infers better the source and target of the resulting morphism". Using a type synonym like ×ₘ makes your code 'line up' more directly with the definitions and lemmas defined for product categories, so Lean is more likely to find the 'right' types/implicit arguments on its own.

[Klaus Gy]

@Robert Maxton Yes, that's also how I understood it, but then sometimes simp drops the ×ₘ e.g. in prod_comb, or the currying definition doesn't use them. So I feel when sticking to f ×ₘ g, one needs to constantly be aware to not use lemmas which change it to (f, g) instead.

Is there a good reason why (f, g) is still used in so many places in mathlib?

[Robert Maxton]

Unfortunately, there is some tension around simp-normal forms. Ideally, you would like simp to stay "within the specific library's notation" exactly until there are no more specific lemmas to simplify with, then to unfold the notation into some simpler/more general form, and then repeat the process. But it's often quite difficult to even pinpoint that line at all, never mind get simp to cooperate. (I am currently running into exactly this problem in TopCat, where many expressions are best simplified as categorical compositions and only reduced to compositions of ContinuousMaps as a last resort.)

[Robert Maxton]

In this case, I would imagine that whoever wrote the library thought that once you pass the initial point of 'making Lean infer the types of theorem statements', it's more useful to reduce ×ₘ to Prod which has a ton of API for it

[Robert Maxton]

But this may in fact be untrue

[Robert Maxton]

At any rate, you may consider just using attribute [-simp] <unhelpful simp lemmas> within your own code at first, and then if you consistently find yourself -simping the same lemmas put forth a PR or suggestion to that effect later

[Klaus Gy]

Thanks a lot for the good explanation! I didn't know attribute [-simp], that sounds really helpful :)