MonCat is monoidal

Stream: Is there code for X?

[Andrew Yang]

Do we really not have this or do I need to open something

import Mathlib

open CategoryTheory MonoidalCategory

#synth MonoidalCategory MonCat

[Markus Himmel]

Seems like no one has given a docs#CategoryTheory.ChosenFiniteProducts instance for MonCat, but you can do

attribute [local instance] ChosenFiniteProducts.ofFiniteProducts

[Andrew Yang]

Is that the one we want? Or is the ChosenFiniteProducts given by actual PUnit and Prod better?

[Markus Himmel]

Yes, it would be better to have something like docs#CategoryTheory.typesChosenFiniteProducts in mathlib for the various other concrete categories.

[Andrew Yang]

Do we also want good defeqs for IsLimit.lift of the chosen limit cones? Or is it fine to get an arbitrary lift from ReflectsLimits?

[Joël Riou]

If we can have good defeq, I think it is better.

[Andrew Yang]

How does mathlib talk about cartesian monoidal categories? It seems like we use ChosenFiniteProducts, but what if the monoidal category instance is not constructed that way? e.g. CommMonCatᵒᵖ.

[Adam Topaz]

What’s the monoidal structure on CommMonCat^op?

[Andrew Yang]

The one coming from ChosenFiniteProducts CommMonCat (which is not yet in mathlib)

[Andrew Yang]

(and then docs#CategoryTheory.monoidalCategoryOp)

[Adam Topaz]

I guess you could introduce a ChosenFiniteCoproducts class, and show that C^op has such an instance provided that C has chosen finite products, then consider the cocartesian monoidal structure. Of course one has to be careful as we would very quickly hit some bad diamonds. Maybe we should also not make the ChosenFiniteProducts -> MonoidalCategory an instance?

[Andrew Yang]

Yeah that is one problem but the other problem I'm facing (or was; I don't need it anymore) is that the cartesian monoidal structure on CommMonCat is also co-cartesian because biproducts exists in CommMonCat.

[Joël Riou]

Andrew Yang said:

How does mathlib talk about cartesian monoidal categories? It seems like we use ChosenFiniteProducts, but what if the monoidal category instance is not constructed that way? e.g. CommMonCatᵒᵖ.

The general definition is MonoidalClosed!

[Andrew Yang]

I'm confused. Cartesian-monoidal and monoidal closed are different things?

[Joël Riou]

CartesianClosed is an abbrev.

[Andrew Yang]

Yes but I'm talking about not-necessarily-closed cartesian monoidal categories.