Cartesian closed Monoidal categories.

Stream: mathlib4

[Robin Carlier]

After submitting #17424, I realized that it would potentially introduce two competing ways for instanciating a monoidal category structure on Type u: either through the chosen finite products I introduced, or through docs#CategoryTheory.monoidalOfChosenFiniteProducts. The code for cartesian closed categories impose that the monoidal category structure comes from the latter, and so a category whose monoidal structure comes from docs#CategoryTheory.ChosenFiniteProducts.instMonoidalCategory can’t be promoted to a Cartesian closed category, which feels pretty wrong as one should be able to freely choose wether or not their structure comes from provided finite products, or from abstract ones.

I think a solution would be to introduce a class

class CartesianMonoidalCategory (C : Type u) [Category.{v} C] extends MonoidalCategory C where
  unitTerminal : IsTerminal tensorUnit
  tensorProductIsBinaryProduct :
    ∀ X Y : C, IsLimit <| BinaryFan.mk
      ((whiskerLeft X (unitTerminal.from Y)) ≫ (rightUnitor X).hom)
      ((whiskerRight (unitTerminal.from X) Y) ≫ (leftUnitor Y).hom)

which asserts that the underlying monoidal structure is in fact a cartesian one, and then change the code of ChosenFiniteProducts, OfHasFiniteProduct and the things about cartesian closed categories to use this class instead. But this would be a rather big refactor and it would also probably deprecate the code in CategoryTheory/ChosenFiniteProducts/Symmetric.lean (because its content would rather need to be generalized for arbitrarty cartesian monoidal categories).

Since it’s a rather big refactor, I’m asking for opinions on this before I try working on implementing it.

[Adam Topaz]

I’m not sure why that PR is needed, since Type already has a chosen finite products instance in mathlib.

[Adam Topaz]

The monoidal structure on Type in mathlib should indeed be the one coming from this instance.

[Adam Topaz]

I don’t see why ChosenFiniteProducts can’t just be the class for Cartesian monoidal categories

[Robin Carlier]

Adam Topaz said:

I’m not sure why that PR is needed, since Type already has a chosen finite products instance in mathlib.

Damn, you’re right, I did not see that it was in Monoidal/Types/Basic.lean
Then I’ll just close the PR, sorry for the noise for this one.
But then it still looks like the code in CategoryTheory/Closed/Types.lean expects a different monoidal structure, or am I just completely not understanding how instances inferences work?

[Adam Topaz]

Sorry, I’m not by a computer right now, so I can’t check explicitly myself.

[Robin Carlier]

Looks like I was worried about nothing and that instances find their way correctly, despite the code for monoidal closed categories relying on OfHasFiniteProduct

[Robin Carlier]

Actually, it looks like I spoke too soon:

import Mathlib.CategoryTheory.Closed.Types
import Mathlib.CategoryTheory.Monoidal.Types.Basic

universe u
namespace CategoryTheory

attribute [local instance] monoidalOfHasFiniteProducts
noncomputable instance test : MonoidalClosed (Type u) := by infer_instance

end CategoryTheory

The test instance can’t be synthesized if I remove the local instance attribute, which tends to indicate that this is not using the "right" monoidal structure.

[Robin Carlier]

Still on the subject of ChosenFiniteProducts and monoidal structures on Type,

import Mathlib.CategoryTheory.Monoidal.Types.Basic
import Mathlib.CategoryTheory.ChosenFiniteProducts

universe u
namespace CategoryTheory

open CategoryTheory.MonoidalCategory

variable (E F : Type u)

set_option trace.Meta.synthInstance true in
def test : (E ⊗ F) ≅ E ⨯ F := Iso.refl _ -- fails

end CategoryTheory

Shows that despite the ChosenFiniteProduct instance, lean is not using it to synthesize HasBinaryProduct E F (and seems to be using that Type u has limits for all small discrete categories instead), and I don’t know if that should count as a bug or a feature.

[Markus Himmel]

The ⨯ notation always uses a choice principle to pick an arbitrary binary product (and HasBinaryProduct E F is a Prop-valued class that only asserts that a product exists, it does not contain a specific choice of product), so this is not supposed to work. If you want to talk about the chosen binary product, E ⊗ F is the correct way to do so.

[Robin Carlier]

Feature it is then, thanks for the clarification.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

After the change to use ChosenFiniteProducts for CCCs, some lemmas that refer to prod no longer work when the ChosenFiniteProducts are chosen in the AC sense. Should the below be simp lemmas or not?

@[simp]
theorem ChosenFiniteProducts.ofFiniteProducts_fst
    {C : Type*} [Category C] [HasFiniteProducts C] (X Y : C) :
    @ChosenFiniteProducts.fst _ _ (ChosenFiniteProducts.ofFiniteProducts _) X Y = prod.fst := by
  rfl

@[simp]
theorem ChosenFiniteProducts.ofFiniteProducts_snd
    {C : Type*} [Category C] [HasFiniteProducts C] (X Y : C) :
    @ChosenFiniteProducts.snd _ _ (ChosenFiniteProducts.ofFiniteProducts _) X Y = prod.snd := by
  rfl

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

And is it a problem that the following fails to hold definitionally?

import Mathlib.CategoryTheory.ChosenFiniteProducts
import Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts

open CategoryTheory Limits

variable {C : Type} [Category C] [HasFiniteProducts C]

example :
    monoidalOfHasFiniteProducts C =
    @ChosenFiniteProducts.instMonoidalCategory C _ (ChosenFiniteProducts.ofFiniteProducts C) := by
  rfl -- fails