Chosen finite products and internal homs

Stream: Is there code for X?

[Adam Topaz]

We have docs#CategoryTheory.CartesianClosed which uses the (noncomputable) categorical products as an assumption. On the other hand, we have docs#CategoryTheory.monoidalOfChosenFiniteProducts which lets us construct a (cartesian) monoidal structure by explicitly specifying a terminal object and binary products. However, we don't have any real API for cartesian monoidal categories. E.g. there is no lift which takes $f : X \to Y$ and $g : X \to Z$ and gives $X \to Y \otimes Z$.

For a personal project I'm working on, I would like to be able to talk about explicit cartesian (closed) structures on categories, where there is an explicitly chosen product and terminal object (and internal hom for the closed case). The approach I'm currently taking is this:

class ChosenFiniteProducts (C : Type u) [Category.{v} C] where
  product : (X Y : C) → Limits.LimitCone (Limits.pair X Y)
  terminal : Limits.LimitCone (Functor.empty C)

and providing a monoidal instance based on that. I then use the notation from the monoidal categories API to work with the chosen product and terminal object.

Does anyone see a more convenient approach to accomplishing the same thing, using what's currently in mathlib?

[Adam Topaz]

I have opened a PR here: #11248

[Adam Topaz]

One potential issue I see with this is that there are categories which have a natural monoidal structure and a natural Cartesian structure which don’t agree (e.g. modules). In such cases introducing an instance of this new class will cause diamond issues. A potential fix is to introduce custom notation for the explicit product and terminal object that doesn’t go through the monoidal instance, and to make that instance a def. Anyone have any thought about this?

[Adam Topaz]

@Kevin Buzzard Jujian Zhang @Amelia Livingston

[Kevin Buzzard]

@Edison Xie might also be interested in this

[Edison Xie]

Kevin Buzzard said:

Edison Xie might also be interested in this

yes jujian has sent me a paragraph of codes written by Adam to bypass the proof of category over a monoid object being monoidal

[Jujian Zhang]

Am I missing something here. My understanding is that this is a solution to put a monoidal structure where we have good definition equality on a category whose natural monoidal structure is Cartesian product. So can we just manually avoid using ChosenFiniteProducts on category of modules etc whose monoidal structure and Cartesian product diverges. For example, we don’t mark monoidalOfChosenFiniteProducts and monoidalOfFiniteProducts as instance so that monoidal instance from ChosenFiniteProducts and FiniteProducts should be written manually and maybe with help of type alias, could diamonds be eliminated?

[Jujian Zhang]

If we worry that our version of carefully chosen Cartesian product might get confused with the product object by axiom of choice, we can use the tensorObj notation.

[Adam Topaz]

Yeah you don’t have to introduce an instance of this class. But then using the explicit product of modules (whose underlying type is the type theoretic product) is not so convenient when doing category theory