Bimon C = Mon C when C is cartesian-monoidal

Stream: mathlib4

[Yaël Dillies]

I am trying to show Bimon_ C ≌ Mon_ C. Since Bimon_ C := Comon_ (Mon_ C), this should be easy from the existing Comon_ C ≌ C (docs#comonEquiv), except:

1. Mon_ C doesn't have HasTerminal, HasBinaryProducts instances (these are true, right?)
2. The existing Comon_ C ≌ C only talks about the cartesian-monoidal structure defined from the finite products using choice (docs#CategoryTheory.monoidalOfHasFiniteProducts), while Mon_ C has its own pre-existing monoidal structure (docs#Mon_.monMonoidal).

[Yaël Dillies]

Here's my idea:
1.Provide ChosenFiniteProducts (Mon_ C) in such a way that the derived MonoidalCategory (Mon_ C) instance will be defeq to the existing one (is this possible?)

2. Refactor this Comon_ C ≌ C thing to take the monoidal structure coming from ChosenFiniteProducts rather than from monoidalOfHasFiniteProducts.

[Yaël Dillies]

Does that sound reasonable?

[Yaël Dillies]

Greater context: In Toric we are trying to derive the non-categorical version of "antipode antidistributes over comultiplication" from the categorical version (docs#Hopf_.antipode_comul)

[Yaël Dillies]

In general, I feel like we're pushing the existing cartesian-monoidal design to its limits here, and it might need to be refactored away, eg by replacing

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

with

class ChosenFiniteProducts (C : Type u) [Category.{v} C] [MonoidalCategory C] where
  -- state that `𝟙_ C` forms a cone for `Functor.empty.{0} C`
  -- state that `X ⊗ Y` forms a cone for `LimitCone (pair X Y)`

[Yaël Dillies]

cc @Kim Morrison who wrote the original file and @Joël Riou whose categorical wisdom is unmatched

[Yaël Dillies]

(Bhavik already didn't disagree to the plan)

[Adam Topaz]

I would refactor Chosen…as you suggest, change the comon equivalence to use Chosen… instead of the Cartesian structure coming from choice, and add a Chosen… instance on Mon_ C when C has chosen finite products. I think everything will work out with these steps.

[Robin Carlier]

In #mathlib4 > Cartesian closed Monoidal categories. , I pitched the idea for such a refactor of cartesian monoidal categories (having it extends monoidal categories, rather than being a structure on its own), but got no big feedback on this.

[Robin Carlier]

My limited experience of refactoring cartesian closed categories to use ChosenFiniteProduct is that this refactor would be a good thing, and matches the idea that being cartesian is essentially a property of a monoidal category, not an actual extra structure (at least, from a pen-and-paper point of view; the limit cones are of course non-Prop structures).

[Bhavik Mehta]

Yaël Dillies said:

(Bhavik already didn't disagree to the plan)

(And now the above discussion has moved me from not disagreeing with the plan to agreeing with the plan )

[Joël Riou]

I think this would go in the right direction (even though we would still need a constructor for MonoidalCategory/ChosenFiniteProducts which would take as an input the current ChosenFiniteProducts structure). For monoidal functors between categories with chosen finite products, I have outlined some changes in the same direction at https://github.com/leanprover-community/mathlib4/pull/23912#issuecomment-2793022708

[Adam Topaz]

I should say that when I originally introduced chosen finite products, I added the monoidal structure primarily as a notational convenience. Of course I’m happy that this class ended up being so useful, and now that we’ve reached genuine interaction between this class and things like Mon_ I think the suggested refactor is absolutely the way to go (given that a constructor is also added as Joël suggests).

[Yaël Dillies]

Yes, great! We've got 4-5 people who reached the same conclusions independently, so they must be somewhat right. I don't know how much potential there is to share work, but at least I will try to get this refactor done by the end of next week.

[Yaël Dillies]

Draft refactor is at #24390. Andrew, Michal and I will work on it in the coming weeks

[Robin Carlier]

A comment on your definition for CartesianMonoidalCategory: the maps fst and snd do not have to be part of the structure. They are fully determined by the fact that the unit is terminal and the monoidal category structure (fst is X ⊗ Y ⟶ (X ⊗ ⊤_) ≅ (X ⊗ 𝟙_) ≅ X for instance; first map is X tensor the unique map to the terminal, last is right unitor.)

[Robin Carlier]

This also makes it redundant to extend BraidedCategory: the braiding isomorphism should be defined using the universal property of products instead.

[Yaël Dillies]

Your suggestions are going against the idea behind CartesianMonoidalCategory: that existing data shouldn't be rewritten over. For example, in the case of CommAlg, we want to set fst to docs#Algebra.TensorProduct.includeLeft

[Robin Carlier]

I don’t understand. For (the opposite of) commutative algebras, I believe the map you linked is equal to the composition I wrote. Are you saying this is bad because it should instead be defeq?

My point is that in terms of extra data compared to a regular monoidal category, the only thing a cartesian monoidal category has as extra is the maps from any object to the unit (which is baked into the fact that said unit is terminal), and that it’s then a property of these maps that this forms a limit cone (at least, that’s how they are usually presented in the literature I know of).

[Andrew Yang]

Yes. The point is to have good defeqs on the projections fst and snd (as well as lift)

[Robin Carlier]

class CartesianMonoidalCategory extends MonoidalCategory C where
  /-- A choice of a limit binary fan for any two objects of the category. -/
  isTerminalTensorUnit : IsTerminal (𝟙_ C)
  tensorProductIsBinaryProduct (X Y : C) :
    IsLimit <| BinaryFan.mk (X ◁ (isTerminalTensorUnit.from Y) ≫ (ρ_ X).hom)
      ((isTerminalTensorUnit.from X) ▷ Y ≫ (λ_ Y).hom)

This is more or less what I was thinking. I understand the point of the defeq properties of the projections.
As long as you can show that your fst and snd are equal to the maps I wrote/provide a constructor with the parameters I gave I guess it’s fine.

[Robin Carlier]

The reason I worry is that while the maps X ◁ (isTerminalTensorUnit.from Y) ≫ (ρ_ X).hom and ((isTerminalTensorUnit.from X) ▷ Y ≫ (λ_ Y).hom) are "clearly" natural with respect to both argument, I am not sure that this is the case if you just pick arbitrary projections and merely ask that they form a limit cone. For instance, is it clear with your definition that f ⊗ g : X ⊗ Y ⟶ X' ⊗ Y' (which you already have from the MonoidalCategory struct) is also lift (fst ≫ f) (snd ≫ g)?

[Andrew Yang]

On the contrary, this is what I am proposing:

class CartesianMonoidalCategory extends MonoidalCategory C, BraidedCategory C where
  /-- A choice of a limit binary fan for any two objects of the category. -/
  isTerminalTensorUnit : IsTerminal (𝟙_ C)
  fst (X Y : C) : X ⊗ Y ⟶ X
  snd (X Y : C) : X ⊗ Y ⟶ Y
  tensorProductIsBinaryProduct (X Y : C) : IsLimit <| BinaryFan.mk (fst X Y) (snd X Y)
  whiskerLeft_fst (X : C) {Y Z : C} (f : Y ⟶ Z) : X ◁ f ≫ fst _ _ = fst _ _ := by aesop_cat
  whiskerLeft_snd (X : C) {Y Z : C} (f : Y ⟶ Z) : X ◁ f ≫ snd _ _ = snd _ _ ≫ f := by aesop_cat
  whiskerRight_fst {X Y : C} (f : X ⟶ Y) (Z : C) : f ▷ Z ≫ fst _ _ = fst _ _ ≫ f := by aesop_cat
  whiskerRight_snd {X Y : C} (f : X ⟶ Y) (Z : C) : f ▷ Z ≫ snd _ _ = snd _ _ := by aesop_cat
  leftUnitor_inv_fst (X : C) : (λ_ X).inv ≫ fst _ _ = isTerminalTensorUnit.from _ := by aesop_cat
  leftUnitor_inv_snd (X : C) : (λ_ X).inv ≫ snd _ _ = 𝟙 _ := by aesop_cat
  rightUnitor_inv_fst (X : C) : (ρ_ X).inv ≫ fst _ _ = 𝟙 _ := by aesop_cat
  rightUnitor_inv_snd (X : C) : (ρ_ X).inv ≫ snd _ _ = isTerminalTensorUnit.from _ := by aesop_cat
  associator_hom_fst (X Y Z : C) : (α_ X Y Z).hom ≫ fst _ _ = fst _ _ ≫ fst _ _ := by aesop_cat
  associator_hom_snd_fst (X Y Z : C) :
    (α_ X Y Z).hom ≫ snd _ _ ≫ fst _ _ = fst _ _ ≫ snd _ _ := by aesop_cat
  associator_hom_snd_snd (X Y Z : C) : (α_ X Y Z).hom ≫ snd _ _ ≫ snd _ _ = snd _ _ := by aesop_cat
  braiding_hom_fst (X Y : C) : (β_ X Y).hom ≫ fst _ _ = snd _ _ := by aesop_cat
  braiding_hom_snd (X Y : C) : (β_ X Y).hom ≫ snd _ _ = fst _ _ := by aesop_cat

[Robin Carlier]

Ok, then you are baking in all the coherences in that constructor, and this should be fine. I was worried because of the current content of #24390.

[Andrew Yang]

I believe for your approach to work, you would need similar compatibility lemmas with the existing structure (I don't think the monoidal structure is uniquely determined given such limit cones)? Or if they are actually not needed, I might be able to cut down the number of fields to my approach as well.

[Andrew Yang]

E.g leftUnitor_inv_fst is not needed because maps to the terminal object is obviously unique…

[Robin Carlier]

The monoidal category is fully determined by what I wrote I think, at least that’s what I can read from chapter 2.4 of Lurie's Higher Algebra. Def 2.4.0.1 is the one I gave, and the chapter shows some universal properties and unicity for such monoidal structures (this is for infinity categories, but it applies in particular to 1-categories).

[Robin Carlier]

So perhaps you could get away with

class CartesianMonoidalCategory extends MonoidalCategory C, BraidedCategory C where
  /-- A choice of a limit binary fan for any two objects of the category. -/
  isTerminalTensorUnit : IsTerminal (𝟙_ C)
  fst (X Y : C) : X ⊗ Y ⟶ X
  snd (X Y : C) : X ⊗ Y ⟶ Y
  tensorProductIsBinaryProduct (X Y : C) : IsLimit <| BinaryFan.mk (fst X Y) (snd X Y)
  fst_eq (X Y : C) : fst X Y = X ◁ (isTerminalTensorUnit.from Y) ≫ (ρ_ X).hom := by aesop_cat
  snd_eq (X Y : C) : snd X Y = (isTerminalTensorUnit.from X) ▷ Y ≫ (λ_ Y).hom := by aesop_cat

[Robin Carlier]

On second though, maybe there is a need for two extra coherence axioms that characterize the braiding as well (I am not entirely sure yet).

[Andrew Yang]

I’ve tried and it works perfectly (with braidings as well)

[Robin Carlier]

Great, I was writing one big diagram to see if it works, but it’s even better that there no need for it.

[Andrew Yang]

#24399 is ready for review now. I've decided it is easier to do the refactor in place, and rename ChosenFiniteProducts to CartesianMonoidalCategory in a follow up PR.