Relating the categorical product and the normal product

Stream: Is there code for X?

[Joachim Breitner]

I’m looking at reviving an old abondonned PR (Showing that ωCPO forms a complete category), so I am exploring the category theory APIs right now. That PR proves relates X ⨯ Y (the binary product object) and X × Y (the product on types), and in the proofs then goes from one world to the other, together with a bunch of helper lemmas relatings fst and lift of the two worlds etc.
But I’d expect that many concrete categories have the structure that the product object is isomorphic to the (normal) product, so I wonder if there is generic machinery for that somewhere that I can just instantiate?
Or is it a sign that the proofs are not “category theoryish” enough if I have to leave the world of arrows and objects and drop to concrete tuples?

[Scott Morrison]

There are various preserves_limits typeclasses for functors, and you may be looking for one of those for your forgetful functor.

[Scott Morrison]

Then you can use preserves_product.iso : G.obj (∏ f) ≅ ∏ (λ j, G.obj (f j)).

[Scott Morrison]

or preserves_limit_pair.iso : G.obj (X ⨯ Y) ≅ G.obj X ⨯ G.obj Y for the binary product version

[Joachim Breitner]

Thanks! I would still need something that relates the binary categorical product in the category of types with the product type, would I?

[Joachim Breitner]

Probably <https://leanprover-community.github.io/mathlib_docs/category_theory/limits/shapes/types.html> is relevant somehow. Maybe I need to browse through the docs some more.

[Scott Morrison]

Yeah, that file is not as useful as it might be, because it doesn't interact with the has_limits world.

[Scott Morrison]

You want things like docs#Module.kernel_iso_ker

[Scott Morrison]

I'm a bit mystified to not find these for Type...

[Joachim Breitner]

Ok, so I’d instantiate perserves_limits for forget for ωCPO, like <https://leanprover-community.github.io/mathlib_docs/algebra/category/Group/limits.html#Group.forget_preserves_limits> does for Group.
Then I can use <https://leanprover-community.github.io/mathlib_docs/category_theory/limits/preserves/shapes/binary_products.html#category_theory.limits.preserves_limit_pair.iso> to relate the ⨯ on ωCPO to the ⨯ on types.
And then someone has to find the thing relating ⨯ with ×, or I have to add that.
And then I can only hope that enough simp lemmas are around so that the proofs are actually easy :-) (or can I expect all the identifications above to hold definitionally? probably not)

[Scott Morrison]

If you can construct the preserves_limits instance for forget, everything after that should be boilerplate, and we can help you get it right in the PR.

[Scott Morrison]

@Joachim Breitner, I made a PR with the "missing" explicit isomorphisms between the "opaque" (co)limits in Type and the usual ones. #13854

[Scott Morrison]

Be warned, however, that the reason they haven't existed so far, is that usually if you need to use these isomorphisms, you probably should have been using the has_limit API in the first place, but instead use the limit_data API to control the form of your limits.

[Joachim Breitner]

“you should” or “you should not”?

[Joachim Breitner]

I have no ideas if my requests are sensible, and if they are a sign that I am doing something wrong, then maybe I shouldn’t do that, and the missing isomorphisms shouldn’t be added?

[Joachim Breitner]

Also, what is limit_data? It’s mentioned only once:

~/build/lean/mathlib-docs $ git grep limit_data
src/category_theory/limits/shapes/types.lean:we instead construct terms of `limit_data`.

[Scott Morrison]

oops, it got renamed, and the doc wasn't updated, and I was reading that doc just now :-)

[Scott Morrison]

Just limit_cone. It is just a cone, bundled with the fact it is a limit cone.

[Scott Morrison]

More generally I should have said "use the is_limit API rather than the has_limit API"

[Scott Morrison]

basically, if you can work purely formally with universal properties, the has_limit API is great. It picks limits for you!

[Scott Morrison]

But if you need to "get your hands dirty" with a specific construction of a limit, you probably want to be talking about the particular limit_cone and is_limit terms that you care about.

[Scott Morrison]

(I've fixe that stray limit_data mention in my PR now.)

[Scott Morrison]

Unfortunately I've never looked at the ωCPO stuff, so I don't have a specific opinion about what you should be doing. :-)