Premonoidal categories

Stream: mathlib4

[Jad Ghalayini]

Hello everyone!

I'm formalizing some programming language theory in Lean as a continuation of my paper: arXiv:2411.09347. In my work, I make extensive use of (symmetric) premonoidal categories, which generalize monoidal categories by removing the sliding condition.

Unfortunately, this means I can't use Mathlib's MonoidalCategory class directly, so I had to implement a workaround: a somewhat unusual variant in discretion, with typical usage in refined-ssa. This implementation is really just a hack to work around Mathlib’s current design, so I’m not proposing it for merging. However, I’d like to discuss how we might improve Mathlib’s category hierarchy to better support premonoidal categories.

Currently, we have:

• MonoidalCategoryStruct: Defines tensor products and associators/unitors.
• MonoidalCategory: Ensures that MonoidalCategoryStruct forms a valid monoidal category.

I propose adding two intermediate structures:

1. BinoidalCategory: Ensures that left/right whiskering is functorial and defines tensorHom as their composition.
2. PremonoidalCategory: Like MonoidalCategory, but omitting tensorHom composition and requiring associators/unitors to be central.

MonoidalCategory would then remain as before, with the extra structure from PremonoidalCategory handled via default members.

Some of the main things we can do with this are:

• Monoidal coherence extends to premonoidal categories, which I’ve already proved in discretion.
• BraidedCategory can depend on PremonoidalCategory instead of MonoidalCategory, and arguably should just depend on MonoidalCategoryStruct.
• The Kleisli category of a monoidal category is naturally premonoidal, giving a broad class of models for free.

If this is too much, we could drop BinoidalCategory and introduce just PremonoidalCategory, but I find BinoidalCategory useful and aligned with the literature.

Would you be open to a pull request introducing these changes? It seems like a moderate refactor, so I’d likely need guidance from maintainers.

Thanks for your time, and apologies for the long post!

Jad

EDIT: removed distributive categories from the title as I left them out of this proposal since they complicate things

[Johan Commelin]

cc @Yuma Mizuno @Kim Morrison

[Yuma Mizuno]

@Jad Ghalayini I was not familiar with those concepts, but I think it's good to have a premonoidal category in mathlib.

While I cannot accurately estimate the required work, this may not be too much as many definitions and theorems about monoidal categories have already been written in terms of whiskering. You may find it helpful to see the formalization of bicategories (docs#CategoryTheory.Bicategory) where the horizontal composition (analogous to tensorHom) is not yet implemented.

[Joël Riou]

I am not completely sure I understand the exact axioms. Currently, the lemmas that are related to tensor_comp are whiskerLeft_comp, comp_whiskerRight and whisker_exchange. Is it whisker_exchange which does not hold in your context?
In terms of design, my only concern is that when defining a new monoidal category structure, most users should not have to know about the intermediate classes. If MonoidalCategory extends BinoidalCategory, and BinoidalCategory extends MonoidalCategoryStruct, I think it would be ok, but I am not sure that MonoidalCategory should extend PremonoidalCategory.
(In #12728, with @Dagur Asgeirsson , we constructed the monoidal category structure on a localized category. In order to show the pentagon (and triangle) axioms, we need to use some lemmas most of which are consequences of the axioms from BinoidalCategory. If this class was available, the proof would be slightly more direct .)

[Jad Ghalayini]

I already have an idea (hopefully) how to implement this, since I've implemented it along with coherence in discretion. So I should just get along with the PR, then? I'm thinking of doing exactly what @Joël Riou said and making the hierarchy
MonoidalCategory extends PremonoidalCategory extends BinoidalCategory extends MonoidalCategoryStruct;
this is slightly ugly since a binoidal category in the literature does not require associator/unitor isomorphisms to exist, so future refactoring might be to shunt those higher in the hierarchy, but that's just perfectionism imo

[Jad Ghalayini]

Also, that's exactly right, it's whisker_exchange which is invalid, which follows from tensor_comp. The idea is to add whiskerLeft_comp and whiskerRight_comp as members and remove tensor_comp, this follows from the definition of a premonoidal category where ⊗ is individually a functor in the left and right elements but is _not_ (necessarily) a bifunctor. Bifunctoriality is then recovered by adding tensor_comp or whisker_exchange, which in this setting are equivalent; doing the former is probably easier since it should minimize changes to existing MonoidalCategory instances (since whiskerLeft_comp and whiskerLeft_comp can easily be derived from tensor_comp)

[Joël Riou]

I think you may proceed with the PR. (I only have a doubt about whether MonoidalCategory should extend PremonoidalCagegory: if you find a way to make things so that no changes are required in downstream definitions, this would be fine though.)

[Yuma Mizuno]

@Jad Ghalayini If you are interested in generalizing the coherence tactic to PremonoidalCategory setting but stack at some points, feel free to ask me. I found your codes for Central instances around https://github.com/imbrem/discretion/blob/a90ccae04fe1bae94ab38005f71bc1a217526a18/Discretion/Premonoidal/Category.lean#L447 may be enough to implement the tactic, but you will need to write several lines of codes to handle these instances in meta setting.

[Jad Ghalayini]

Hello! I'm working on the PR and am mildly stuck: so I'm trying to get whiskerLeft_comp and comp_whiskerRight to be filled in by default for MonoidalCategory instances as follows:

class MonoidalCategory (C : Type u) [𝒞 : Category.{v} C] extends PremonoidalCategory C where
  /--
  Composition of tensor products is tensor product of compositions:
  `(f₁ ⊗ g₁) ∘ (f₂ ⊗ g₂) = (f₁ ∘ f₂) ⊗ (g₁ ⊗ g₂)`
  -/
  tensor_comp :
    ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
      (f₁ ≫ g₁) ⊗ (f₂ ≫ g₂) = (f₁ ⊗ f₂) ≫ (g₁ ⊗ g₂) := by
    aesop_cat
  whiskerLeft_comp := whiskerLeft_comp_ofTensorHom tensorHom_def id_whiskerRight tensor_comp
  comp_whiskerRight := comp_whiskerRight_ofTensorHom tensorHom_def whiskerLeft_id tensor_comp

Unfortunately... this doesn't work. It's a very minor change to fix all uses by just switching to an alternative constructor for MonoidalCategory, but... there _must_ be a better way? How can we synthesize this nicely?

[Yuma Mizuno]

I'm a bit confused. PremonoidalCategory doesn't have tensorHom, right?

[Jad Ghalayini]

To make my life a (lot) easier I left it in

[Jad Ghalayini]

It makes sense for it to be defined as $f \otimes A ; B \otimes g$

[Jad Ghalayini]

And its useful because for central morphisms it behaves just like it does for monoidal categories

[Jad Ghalayini]

(indeed it is standard notation to write central morphisms with tensors and everything else with ltimes/rtimes)

[Jad Ghalayini]

Let me just show you what I've got:

[Jad Ghalayini]

class BinoidalCategory (C : Type u) [𝒞 : Category.{v} C] extends MonoidalCategoryStruct C where
  -- NOTE: this is easily derivable from the others...
  /-- Tensor product of identity maps is the identity: `(𝟙 X₁ ⊗ 𝟙 X₂) = 𝟙 (X₁ ⊗ X₂)` -/
  tensor_id : ∀ X₁ X₂ : C, 𝟙 X₁ ⊗ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂) := by aesop_cat
  tensorHom_def {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) :
    f ⊗ g = (f ▷ X₂) ≫ (Y₁ ◁ g) := by
      aesop_cat
  /- Left whiskering of the identity is the identity: `X ◁ 𝟙 Y = 𝟙 (X ⊗ Y)` -/
  whiskerLeft_id : ∀ (X Y : C), X ◁ 𝟙 Y = 𝟙 (X ⊗ Y) := by
    aesop_cat
  /- Right whiskering of the identity is the identity `𝟙 X ▷ Y = 𝟙 (X ⊗ Y)` -/
  id_whiskerRight : ∀ (X Y : C), 𝟙 X ▷ Y = 𝟙 (X ⊗ Y) := by
    aesop_cat
  /- Left whiskering respects composition -/
  whiskerLeft_comp (W : C) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
    W ◁ (f ≫ g) = W ◁ f ≫ W ◁ g := by
    aesop_cat
  /- Right whiskering respects composition -/
  comp_whiskerRight {W X Y : C} (f : W ⟶ X) (g : X ⟶ Y) (Z : C) :
    (f ≫ g) ▷ Z = f ▷ Z ≫ g ▷ Z := by
    aesop_cat

class PremonoidalCategory (C : Type u) [𝒞 : Category.{v} C] extends BinoidalCategory C where
  /-- Naturality of the associator isomorphism: `(f₁ ⊗ f₂) ⊗ f₃ ≃ f₁ ⊗ (f₂ ⊗ f₃)` -/
  associator_naturality :
    ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
      ((f₁ ⊗ f₂) ⊗ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ (f₂ ⊗ f₃)) := by
    aesop_cat
  /--
  Naturality of the left unitor, commutativity of `𝟙_ C ⊗ X ⟶ 𝟙_ C ⊗ Y ⟶ Y` and `𝟙_ C ⊗ X ⟶ X ⟶ Y`
  -/
  leftUnitor_naturality :
    ∀ {X Y : C} (f : X ⟶ Y), 𝟙_ _ ◁ f ≫ (λ_ Y).hom = (λ_ X).hom ≫ f := by
    aesop_cat
  /--
  Naturality of the right unitor: commutativity of `X ⊗ 𝟙_ C ⟶ Y ⊗ 𝟙_ C ⟶ Y` and `X ⊗ 𝟙_ C ⟶ X ⟶ Y`
  -/
  rightUnitor_naturality :
    ∀ {X Y : C} (f : X ⟶ Y), f ▷ 𝟙_ _ ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f := by
    aesop_cat
  /--
  The pentagon identity relating the isomorphism between `X ⊗ (Y ⊗ (Z ⊗ W))` and `((X ⊗ Y) ⊗ Z) ⊗ W`
  -/
  pentagon :
    ∀ W X Y Z : C,
      (α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom =
        (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom := by
    aesop_cat
  /--
  The identity relating the isomorphisms between `X ⊗ (𝟙_ C ⊗ Y)`, `(X ⊗ 𝟙_ C) ⊗ Y` and `X ⊗ Y`
  -/
  triangle :
    ∀ X Y : C, (α_ X (𝟙_ _) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y := by
    aesop_cat
...

[Jad Ghalayini]

So we add whiskerLeft_comp and comp_whiskerRight and remove tensor_comp, which implies both of those

[Jad Ghalayini]

What we're basically saying is that - ⊗ A and A ⊗ - are functors, but - ⊗ - is not _necessarily_ a functor

[Jad Ghalayini]

Anyways the issue is it is not filling in the default fields whiskerLeft_comp and comp_whiskerRight so I need to add them in manually in about 5 places; it's not too big a change but it's moderately ugly

[Jad Ghalayini]

Simplest possible method is just to do that and then everything works

[Jad Ghalayini]

Making coherence work shouldn't be _too_ hard after that

[Jad Ghalayini]

Since all you need to do is swap out everything Monoidal for Premonoidal

[Jad Ghalayini]

I've also considered removing tensor_id since its easily derivable from the other members of BinoidalCategory

[Yuma Mizuno]

I see. What I thought was not to include tensorHom in the definition, as in the bicategory definition (docs#CategoryTheory.Bicategory). You can state tensor_comp as the theorem instead of an axiom. This allows you to extract whisker_exchange relation.

[Yuma Mizuno]

One question. Do the f_{1,2,3} in the naturality of associators have to be central?

[Jad Ghalayini]

I think this complicates things a lot; also it now means we need to do even more work fixing usages of MonoidalCategory, whereas now we just need to prove the whiskering lemmas

[Jad Ghalayini]

No, but I just realized that I forgot to make the associators themselves central, d'uh...

[Jad Ghalayini]

Which _also_ follows from tensor_comp, which makes _everything_ central

[Jad Ghalayini]

Now that's a bit more irritating

[Jad Ghalayini]

My current solution is to do something like LawfulMonad.mk', in which I have an alternative constructor for MonoidalCategory which acts exactly like the old constructor and fills in all the defaults

[Jad Ghalayini]

Jad Ghalayini said:

No, but I just realized that I forgot to make the associators themselves central, d'uh...

Note I did this in discretion just forgot to port it over

[Jad Ghalayini]

What I wish is that there was a cleaner way to define default elements in child classes for parents

[Yaël Dillies]

Do you know you can redeclare parent fields when defining a child class? This gives you the opportunity to set a default value

[Jad Ghalayini]

I did redeclare those fields, and it's not working!

[Jad Ghalayini]

See, I wrote this:

class MonoidalCategory (C : Type u) [𝒞 : Category.{v} C] extends PremonoidalCategory C where
  /--
  Composition of tensor products is tensor product of compositions:
  `(f₁ ⊗ g₁) ∘ (f₂ ⊗ g₂) = (f₁ ∘ f₂) ⊗ (g₁ ⊗ g₂)`
  -/
  tensor_comp :
    ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
      (f₁ ≫ g₁) ⊗ (f₂ ≫ g₂) = (f₁ ⊗ f₂) ≫ (g₁ ⊗ g₂) := by
    aesop_cat
  whiskerLeft_comp := whiskerLeft_comp_ofTensorHom tensorHom_def id_whiskerRight tensor_comp
  comp_whiskerRight := comp_whiskerRight_ofTensorHom tensorHom_def whiskerLeft_id tensor_comp

[Jad Ghalayini]

whiskerLeft_comp and comp_whiskerRight being child fields

[Jad Ghalayini]

But for example this code for the Drinfield center fails to synthesize (runs out of heartbeats) without the sorries

instance : MonoidalCategory (Center C) where
  tensorObj X Y := tensorObj X Y
  tensorHom f g := tensorHom f g
  tensorHom_def := by intros; ext; simp [tensorHom_def]
  whiskerLeft X _ _ f := whiskerLeft X f
  whiskerRight f Y := whiskerRight f Y
  tensorUnit := tensorUnit
  associator := associator
  leftUnitor := leftUnitor
  rightUnitor := rightUnitor
  whiskerLeft_comp := sorry
  comp_whiskerRight := sorry

[Jad Ghalayini]

So my current approach is just to replace this with MonoidalCategory.mk', which of course makes the syntax a bit uglier since now all these things become named args with lambdas (thankfully can still use aesop cat as a default tactic)

[Jad Ghalayini]

Thing is only 4 things fail this way so it's not too irritating a change to just get it over with

[Jad Ghalayini]

The alternative is to copy Discretion and have IsPremonoidal and IsMonoidal typeclasses

[Jad Ghalayini]

This would solve the problem since PremonoidalCategory and MonoidalCategory can just inherit from the appropriate typeclasses, and we can have an instance deriving IsPremonoidal from IsMonoidal

[Joël Riou]

Why not keep MonoidalCategory as it is, and only introduce IsBinoidal and IsPremonoidal?

[Jad Ghalayini]

That's what I do in discretion

[Jad Ghalayini]

This is ugly because it makes premonoidal categories into a second-class citizen, imo

[Jad Ghalayini]

Since now you write [Category C] [MonoidalCategoryStruct C] [IsPremonoidal C] everywhere

[Jad Ghalayini]

Of course, we could have a utility class [PremonoidalCategory C] which inherits from MonoidalCategoryStruct C and IsPremonoidal C and use that...

[Jad Ghalayini]

Also when you're actually doing these proofs you often want to do it in stages, e.g. first prove your category is binoidal, then use that to prove your category is premonoidal, etc

[Joël Riou]

Currently, we mostly have only MonoidalCategory, and turning this into [MonoidalCategoryStruct C] and [IsMonoidal C] everywhere would be strictly more ugly...

[Jad Ghalayini]

No I specifically want to avoid this by having PremonoidalCategory C be a subclass of MonoidalCategory C

[Jad Ghalayini]

This also lets you prove a premonoidal category is monoidal by showing everything is central, which is nice

[Jad Ghalayini]

There is one nice alternative I've experimented with in discretion quite a bit, but I have no idea why it doesn't seem to be used a lot in Mathlib which makes me fear there's something horribly wrong with it

[Jad Ghalayini]

That is: have a structure class (so MonoidalCategoryStruct)

[Jad Ghalayini]

A bunch of prop classes on it (IsPremonoidal, IsMonoidal, etc.)

[Jad Ghalayini]

and then define MonoidalCategory to inherit from IsMonoidal and MCS, PremonoidalCategory from IsPremonoidal and MCS, etc

[Jad Ghalayini]

The you can add an instance so that any MCS which is IsMonoidal is automatically a MonoidalCategory

[Jad Ghalayini]

I think I'm overcomplicating it and should just go with the custom constructor for now, I just wish there was nicer syntax/the default fields worked because then I wouldn't need the custom constructor and everything would be fine!

[Jad Ghalayini]

I do wonder why this is not working though:

class MonoidalCategory (C : Type u) [𝒞 : Category.{v} C] extends PremonoidalCategory C where
  /--
  Composition of tensor products is tensor product of compositions:
  `(f₁ ⊗ g₁) ∘ (f₂ ⊗ g₂) = (f₁ ∘ f₂) ⊗ (g₁ ⊗ g₂)`
  -/
  tensor_comp :
    ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
      (f₁ ≫ g₁) ⊗ (f₂ ≫ g₂) = (f₁ ⊗ f₂) ≫ (g₁ ⊗ g₂) := by
    aesop_cat
  whiskerLeft_comp := whiskerLeft_comp_ofTensorHom tensorHom_def id_whiskerRight tensor_comp
  comp_whiskerRight := comp_whiskerRight_ofTensorHom tensorHom_def whiskerLeft_id tensor_comp

abbrev MonoidalCategory.mk' {C : Type u} [𝒞 : Category.{v} C] [MonoidalCategoryStruct C]
  (tensorHom_def :
    ∀{X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
      f ⊗ g = f ▷ X₂ ≫ Y₁ ◁ g := by aesop_cat)
  (tensor_comp :
    ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
      (f₁ ≫ g₁) ⊗ (f₂ ≫ g₂) = (f₁ ⊗ f₂) ≫ (g₁ ⊗ g₂) := by aesop_cat)
  (whiskerLeft_id :
    ∀ (X Y : C), X ◁ 𝟙 Y = 𝟙 (X ⊗ Y) := by aesop_cat)
  (id_whiskerRight :
    ∀ (X Y : C), 𝟙 X ▷ Y = 𝟙 (X ⊗ Y) := by aesop_cat)
  (associator_naturality :
    ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
      ((f₁ ⊗ f₂) ⊗ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ (f₂ ⊗ f₃))
      := by aesop_cat)
  (leftUnitor_naturality :
    ∀ {X Y : C} (f : X ⟶ Y), 𝟙_ _ ◁ f ≫ (λ_ Y).hom = (λ_ X).hom ≫ f := by
    aesop_cat)
  (rightUnitor_naturality :
    ∀ {X Y : C} (f : X ⟶ Y), f ▷ 𝟙_ _ ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f := by
    aesop_cat)
  (pentagon :
    ∀ W X Y Z : C,
      (α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom =
        (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom := by
    aesop_cat)
  (triangle :
    ∀ X Y : C, (α_ X (𝟙_ _) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y := by
    aesop_cat)
      : MonoidalCategory C where
  tensorHom_def := tensorHom_def
  tensor_comp := tensor_comp
  whiskerLeft_id := whiskerLeft_id
  id_whiskerRight := id_whiskerRight
  associator_naturality := associator_naturality
  leftUnitor_naturality := leftUnitor_naturality
  rightUnitor_naturality := rightUnitor_naturality
  pentagon := pentagon
  triangle := triangle

fails with "could not synthesize default value for field 'whiskerLeft_comp' of 'CategoryTheory.BinoidalCategory' using tactics" rather than just using the default value I gave it

[Yuma Mizuno]

Jad Ghalayini said:

No, but I just realized that I forgot to make the associators themselves central, d'uh...

Sorry for going back to my previous question. There is another possible definition of tensorHom (rtimes in discretion). Does the rtimes version associator_naturality_rtimes hold as well? I think that should be the case, but I can't be sure right now.

[Yuma Mizuno]

Also, all possible mix verseions of the two.

[Jad Ghalayini]

Yuma Mizuno said:

Jad Ghalayini said:

No, but I just realized that I forgot to make the associators themselves central, d'uh...

Sorry for going back to my previous question. There is another possible definition of tensorHom (rtimes in discretion). Does the rtimes version associator_naturality_rtimes hold as well? I think that should be the case, but I can't be sure right now.

Yes, I'm using ltimes since that's what you guys currently use

[Jad Ghalayini]

Note that you can prove the rtimes version from the ltimes version of naturality and vice versa

[Jad Ghalayini]

In discretion we only assume the ltimes version and prove the rtimes version as a theorem

[Yuma Mizuno]

Can I see the proofs?

[Jad Ghalayini]

So in discretion we define premonoidal categories as follows:

class IsBinoidal (C: Type u) [Category C] [MonoidalCategoryStruct C] : Prop where
  tensorHom_def {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) :
    f ⊗ g = (f ▷ X₂) ≫ (Y₁ ◁ g) := by
      aesop_cat
  whiskerLeft_id : ∀ (X Y : C), X ◁ 𝟙 Y = 𝟙 (X ⊗ Y) := by
    aesop_cat
  id_whiskerRight : ∀ (X Y : C), 𝟙 X ▷ Y = 𝟙 (X ⊗ Y) := by
    aesop_cat
  whiskerLeft_comp : ∀ {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z), W ◁ (f ≫ g) = (W ◁ f) ≫ (W ◁ g)
    := by aesop_cat
  whiskerRight_comp : ∀ {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z), (f ≫ g) ▷ W = (f ▷ W) ≫ (g ▷ W)
    := by aesop_cat

class IsPremonoidal (C: Type u) [Category C] [MonoidalCategoryStruct C]
  extends IsBinoidal C : Prop where
  associator_central : ∀ {X Y Z : C}, Monoidal.Central (α_ X Y Z).hom := by aesop_cat
  leftUnitor_central : ∀ {X : C}, Monoidal.Central (λ_ X).hom := by aesop_cat
  rightUnitor_central : ∀ {X : C}, Monoidal.Central (ρ_ X).hom := by aesop_cat
  /-- Naturality of the associator isomorphism: `(f₁ ⊗ f₂) ⊗ f₃ ≃ f₁ ⊗ (f₂ ⊗ f₃)` -/
  associator_naturality :
    ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
      ((f₁ ⊗ f₂) ⊗ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ (f₂ ⊗ f₃)) := by
    aesop_cat
  /--
  Naturality of the left unitor, commutativity of `𝟙_ C ⊗ X ⟶ 𝟙_ C ⊗ Y ⟶ Y` and `𝟙_ C ⊗ X ⟶ X ⟶ Y`
  -/
  leftUnitor_naturality :
    ∀ {X Y : C} (f : X ⟶ Y), 𝟙_ _ ◁ f ≫ (λ_ Y).hom = (λ_ X).hom ≫ f := by
    aesop_cat
  /--
  Naturality of the right unitor: commutativity of `X ⊗ 𝟙_ C ⟶ Y ⊗ 𝟙_ C ⟶ Y` and `X ⊗ 𝟙_ C ⟶ X ⟶ Y`
  -/
  rightUnitor_naturality :
    ∀ {X Y : C} (f : X ⟶ Y), f ▷ 𝟙_ _ ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f := by
    aesop_cat
  /--
  The pentagon identity relating the isomorphism between `X ⊗ (Y ⊗ (Z ⊗ W))` and `((X ⊗ Y) ⊗ Z) ⊗ W`
  -/
  pentagon :
    ∀ W X Y Z : C,
      (α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom =
        (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom := by
    aesop_cat
  /--
  The identity relating the isomorphisms between `X ⊗ (𝟙_ C ⊗ Y)`, `(X ⊗ 𝟙_ C) ⊗ Y` and `X ⊗ Y`
  -/
  triangle :
    ∀ X Y : C, (α_ X (𝟙_ _) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y := by
    aesop_cat

Note we assume that ⊗ = ⋉ by tensorHom_def

[Jad Ghalayini]

It's trivial to prove left/middle/right versions from this as follows:

theorem associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) :
  ((f₁ ⊗ f₂) ⊗ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ (f₂ ⊗ f₃))
  := IsPremonoidal.associator_naturality f₁ f₂ f₃

@[reassoc]
theorem associator_naturality_right {X Y Z : C} (f : X ⟶ X') :
  (f ▷ Y) ▷ Z ≫ (α_ X' Y Z).hom = (α_ X Y Z).hom ≫ f ▷ (Y ⊗ Z) := by
  convert associator_naturality f (𝟙 Y) (𝟙 Z) using 1 <;> simp [tensorHom_def]

@[reassoc]
theorem associator_naturality_middle {X Y Z : C} (f : Y ⟶ Y') :
  (X ◁ f) ▷ Z ≫ (α_ X Y' Z).hom = (α_ X Y Z).hom ≫ X ◁ (f ▷ Z) := by
  convert associator_naturality (𝟙 _) f (𝟙 _) using 1 <;> simp [tensorHom_def]

@[reassoc]
theorem associator_naturality_left {X Y Z : C} (f : Z ⟶ Z') :
  (X ⊗ Y) ◁ f ≫ (α_ X Y Z').hom = (α_ X Y Z).hom ≫ X ◁ (Y ◁ f) := by
  convert associator_naturality (𝟙 _) (𝟙 _) f using 1 <;> simp [tensorHom_def]

@[reassoc]
theorem associator_inv_naturality
  {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) :
  (f₁ ⊗ (f₂ ⊗ f₃)) ≫ (α_ Y₁ Y₂ Y₃).inv = (α_ X₁ X₂ X₃).inv ≫ ((f₁ ⊗ f₂) ⊗ f₃)
  := (cancel_mono (α_ Y₁ Y₂ Y₃).hom).mp (by simp [associator_naturality])

@[reassoc]
theorem associator_inv_naturality_right {X Y Z : C} (f : X ⟶ X') :
  f ▷ (Y ⊗ Z) ≫ (α_ X' Y Z).inv = (α_ X Y Z).inv ≫ f ▷ Y ▷ Z := by
  convert associator_inv_naturality f (𝟙 _) (𝟙 _) using 1 <;> simp [tensorHom_def]

@[reassoc]
theorem associator_inv_naturality_middle {X Y Z : C} (f : Y ⟶ Y') :
  X ◁ (f ▷ Z) ≫ (α_ X Y' Z).inv = (α_ X Y Z).inv ≫ (X ◁ f) ▷ Z := by
  convert associator_inv_naturality (𝟙 _) f (𝟙 _) using 1 <;> simp [tensorHom_def]

@[reassoc]
theorem associator_inv_naturality_left {X Y Z : C} (f : Z ⟶ Z') :
  X ◁ (Y ◁ f) ≫ (α_ X Y Z').inv = (α_ X Y Z).inv ≫ (X ⊗ Y) ◁ f := by
  convert associator_inv_naturality (𝟙 _) (𝟙 _) f using 1 <;> simp [tensorHom_def]

@[reassoc]
theorem leftUnitor_naturality {X Y : C} (f : X ⟶ Y) :
  𝟙_ C ◁ f ≫ (λ_ Y).hom = (λ_ X).hom ≫ f := IsPremonoidal.leftUnitor_naturality f

@[reassoc]
theorem leftUnitor_inv_naturality {X Y : C} (f : X ⟶ Y) :
  f ≫ (λ_ Y).inv = (λ_ X).inv ≫ 𝟙_C ◁ f := by
  apply (cancel_mono (λ_ Y).hom).mp
  simp [leftUnitor_naturality]

@[reassoc]
theorem rightUnitor_naturality {X Y : C} (f : X ⟶ Y) :
  f ▷ 𝟙_ C ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f := IsPremonoidal.rightUnitor_naturality f

@[reassoc]
theorem rightUnitor_inv_naturality {X Y : C} (f : X ⟶ Y) :
  f ≫ (ρ_ Y).inv = (ρ_ X).inv ≫ f ▷ 𝟙_ C := by
  apply (cancel_mono (ρ_ Y).hom).mp
  simp [rightUnitor_naturality]

[Jad Ghalayini]

I didn't bother writing versions for rtimes, but you can see that e.g. for associators if I wanted to do naturality for

$$f \rtimes (g \rtimes h)$$

I'd rewrite it to

$$- \lhd (- \lhd h) ; - \lhd (g \rhd -) ; f \rhd -$$

and apply right, middle, left naturality lemmas to get

$$- \lhd h ; (- \rhd g) \lhd - ; (f \rhd -) \rhd -$$

I can do the same for any permutation of f, g, h

[Jad Ghalayini]

In fact, premonoidal categories are usually defined with separate naturality squares for the left, right, and middle; I'm just being lazy and noting that you can instead equivalently just write a single square with ltimes and derive these, and you just happen to get the same thing originally in MonoidalCategory

[Yuma Mizuno]

I see, thanks!

[Yuma Mizuno]

Jad Ghalayini said:

(indeed it is standard notation to write central morphisms with tensors and everything else with ltimes/rtimes)

I actually prefer this convension, which is less confusing for me.

[Jad Ghalayini]

Yuma Mizuno said:

Jad Ghalayini said:

(indeed it is standard notation to write central morphisms with tensors and everything else with ltimes/rtimes)

I actually prefer this convension, which is less confusing for me.

As in, writing central morphisms with tensors? I agree; all other use of tensors in discretion is for backwards compatibility purposes with mathlib's monoidal stuff

[Jad Ghalayini]

Also, I'm currently experimenting with a design like this to deal with the default member problem. Would such dirty hacks be acceptable as a pure implementation detail, assuming the rest of mathlib can use MonoidalCategory with exactly the same API as before?

variable (C : Type u) [𝒞 : Category.{v} C] [MonoidalCategoryStruct C]

class TensorHomDef : Prop where
  tensorHom_def {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) :
    f ⊗ g = (f ▷ X₂) ≫ (Y₁ ◁ g) := by aesop_cat

class WhiskeringId : Prop where
  /- Left whiskering of the identity is the identity: `X ◁ 𝟙 Y = 𝟙 (X ⊗ Y)` -/
  whiskerLeft_id : ∀ (X Y : C), X ◁ 𝟙 Y = 𝟙 (X ⊗ Y) := by
    aesop_cat
  /- Right whiskering of the identity is the identity `𝟙 X ▷ Y = 𝟙 (X ⊗ Y)` -/
  id_whiskerRight : ∀ (X Y : C), 𝟙 X ▷ Y = 𝟙 (X ⊗ Y) := by
    aesop_cat

class WhiskeringComp : Prop where
  /- Left whiskering respects composition -/
  whiskerLeft_comp (W : C) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
    W ◁ (f ≫ g) = W ◁ f ≫ W ◁ g := by
    aesop_cat
  /- Right whiskering respects composition -/
  comp_whiskerRight {W X Y : C} (f : W ⟶ X) (g : X ⟶ Y) (Z : C) :
    (f ≫ g) ▷ Z = f ▷ Z ≫ g ▷ Z := by
    aesop_cat

class TensorFunctorial : Prop where
  /-- Tensor product of identity maps is the identity: `(𝟙 X₁ ⊗ 𝟙 X₂) = 𝟙 (X₁ ⊗ X₂)` -/
  tensor_id : ∀ X₁ X₂ : C, 𝟙 X₁ ⊗ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂) := by
    aesop_cat
  /--
  Composition of tensor products is tensor product of compositions:
  `(f₁ ⊗ g₁) ∘ (f₂ ⊗ g₂) = (f₁ ∘ f₂) ⊗ (g₁ ⊗ g₂)`
  -/
  tensor_comp :
    ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
      (f₁ ≫ g₁) ⊗ (f₂ ≫ g₂) = (f₁ ⊗ f₂) ≫ (g₁ ⊗ g₂) := by
    aesop_cat

theorem WhiskeringId.id_tensorHom [TensorHomDef C] [WhiskeringId C]
  (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂) :
    𝟙 X ⊗ f = X ◁ f := by simp [TensorHomDef.tensorHom_def, id_whiskerRight]

theorem WhiskeringId.tensorHom_id [TensorHomDef C] [WhiskeringId C]
  {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) :
    f ⊗ 𝟙 Y = f ▷ Y := by simp [TensorHomDef.tensorHom_def, whiskerLeft_id]

instance TensorFunctorial.instWhiskeringComp
  [TensorHomDef C] [TensorFunctorial C] [WhiskeringId C] : WhiskeringComp C where
  whiskerLeft_comp := by intros; simp [<-WhiskeringId.id_tensorHom, <-tensor_comp]
  comp_whiskerRight := by intros; simp [<-WhiskeringId.tensorHom_id, <-tensor_comp]

[Jad Ghalayini]

Note that now the WhiskeringComp fields are automatically generated by typeclass inference

[Jad Ghalayini]

I'm taking inspiration from how Lattice and friends work; the idea would be to have BinoidalCategory extend WhiskeringId, WhiskeringComp, and TensorHomDef while MonoidalCategory would extend TensorFunctorial

[Jad Ghalayini]

TensorFunctorial would also by typeclass inference render everything central, and hence it would be easy to infer the associators are central by e.g. just infer_instance

[Jad Ghalayini]

In general I'd like to separate out the tensor structure (whiskering, homs, etc) from the monoidal structure (associators) but that can be a separate PR, again, most users would see no difference except that you can theoretically structure your proofs a bit more cleanly by using the fact that your category is binoidal before even constructing associators

[Jad Ghalayini]

This is however only really useful for my use-case where (in the repo https://github.com/imbrem/debruijn-ssa) I construct a premonoidal category by quotienting syntax and defining associators/unitors/etc is Very Hard (TM), with the binoidal structure maybe useful to prove e.g. the associator is an isomorphism

[Jad Ghalayini]

I've been facing some issues with default members, which have been moved to #lean4 > Issues with default parameters . My current best-effort solution is just to fill in the default parameters for all uses of MonoidalCategory now, since when/if that issue is fixed we can remove them. Other options include:

• Leaving them in
• Weird typeclass hack I've been experimenting with to avoid this problem, but it messes with the monoidal tactic

[Yuma Mizuno]

I would like to suggest using whisker_exchange rather than tensor_comp as an axiom for MonoidalCategory minus PremonoidalCategory. Adding a redundant condition is aesthetically unappealing (in my personal view) and may increase the work when proving the condition in practice.

We can define an additional constructor for MonoidalCategory that includes tensor_comp as an axiom, written solely in terms of tensorHom rather than whiskerings. Several monoidal category instances in the current downstream files could likely be given by this constructor.

[Jad Ghalayini]

@Yuma Mizuno I could do that, but that would require changing all existing instances of MonoidalCategory to use the new constructor. On the other hand, it would unblock us from #lean4 > Issues with default parameters , and the other solution I was considering is kind of ugly. Would doing this be acceptable, that is, changing every

instance : MonoidalCategory C where
  tensor_comp f g := ...

to

instance: MonoidalCategory C := MonoidalCategory.mk' (tensor_comp := fun f g => ...)

[Jad Ghalayini]

If so I can probably get a PR ready Soon (TM) (I was really gunning for yesterday but I used the whole day on it and I have to give a presentation tomorrow rip)

[Jad Ghalayini]

Also w.r.t. your note about work it turns out the automation is much better at proving things like tensor_comp than it is at proving things like whiskerLeft_comp, let alone whisker_exchange. This actually makes sense when you consider the current simp-normal forms favored, and I don't plan to change that since most math people will be using monoidal categories, and PL users such as myself will need weird simplifications anyways

[Jad Ghalayini]

(At least, so my intuition tells me from work on discretion)

[Joël Riou]

If the lean4 issue has a chance to be solved in a near future, I would prefer we wait for the fix, unless there are other particular reasons to proceed very fast.

[Yuma Mizuno]

Jad Ghalayini said:

Would doing this be acceptable, that is, changing every

instance : MonoidalCategory C where
  tensor_comp f g := ...

to

instance: MonoidalCategory C := MonoidalCategory.mk' (tensor_comp := fun f g => ...)

In my opinion, this kind of change is acceptable. The default constructor has some syntactic privileges, but other than that I think the change is not large.

[Yuma Mizuno]

Perhaps the syntax could be improved by defining a structure that contains the arguments of the additional constructor?

[Jad Ghalayini]

@Joël Riou if we go with the whisker_exchange design then things look the same whether or not we have the fix, hence my suggestion to just go ahead. On the other hand, with tensor_comp, things are indeed a _lot_ cleaner with the fix.

[Yuma Mizuno]

Jad Ghalayini said:

Also w.r.t. your note about work it turns out the automation is much better at proving things like tensor_comp than it is at proving things like whiskerLeft_comp, let alone whisker_exchange.

I find this observation interesting since it contradicts my intuition. I would like to know more about this.

One note: It is "intentional" that the simp automation does not handle whisker_exchange. Currently, simp does not determine whether right or left morphisms should come first. On the other hand, I believe the automation works well for whiskerLeft_comp. It just expands the expression distributively, which is a typical simp lemma in algebraic theories.

[Jad Ghalayini]

@Yuma Mizuno so I finally found some time to work on this again, and I'm nearly finished what will hopefully be a decent PR

[Jad Ghalayini]

I've got a question though: for stuff that's true for PremonoidalCategory, should we move it from the MonoidalCategory namespace to the PremonoidalCategory namespace and re-export it or just leave it in the MonoidalCategory namespace with a PremonoidalCategory bound?

[Jad Ghalayini]

Going with the former so far

[Jad Ghalayini]

One issue I'm worried about however is the notation is in MonoidalCategory, so we'd want to open that anyways...

[Jad Ghalayini]

OK, I'm done a draft PR:
https://github.com/leanprover-community/mathlib4/pull/21488

[Jad Ghalayini]

I'm stuck because this change seems to break the string diagram tool...

[Jad Ghalayini]

@Yuma Mizuno this seems to be related to the coherence tactic; mind helping me out?

[Jad Ghalayini]

I have no idea how CoherenceM works

[Jad Ghalayini]

I fixed the failing tests with type hints, should have thought of that first!

[Jad Ghalayini]

Well, at least I hope I did, waiting for CI!

[Yuma Mizuno]

Thanks! I can't look it in detail today, but I will sometime soon.

[Jad Ghalayini]

Thanks a lot! I've now got the monoidal_coherence tactic working, and the monoidal tactic working _sometimes_, since premonoidal categories can't interconvert between f \rtimes g and f \otimes g. We'd probably want a premonoidal tactic that doesn't attempt such normalization, but for now we just error out if its required with a can't find monoidal instance and that works just fine

[Jad Ghalayini]

Hello! I realize this PR is very big; do you think it would be worthwhile to split it into some smaller PRs which:

1. Introduce the premonoidal category API
2. Port the coherence tactic to use the premonoidal category API (depends on 1)
3. Port braided + symmetric monoidal categories to use premonoidal categories (depends on 2)
4. Add some extra lemmas unique to premonoidal categories (depends on 1)

[Jad Ghalayini]

@Yuma Mizuno ?

[Kim Morrison]

Sorry I'm coming to this very late. I admit I am a little skeptical, and would like to see some more explanation of why premonoidal categories are a natural concept (despite working in low-dimensional category theory for many years, I had not met them).

In particular, consider the following question: what if someone later wants to add the (in my mind, better justified) definition of a skew monoidal category (this is one in which the associator is not necessarily invertible). How will the development of monoidal categories look then, if it has to accomodate both? Would it still be viable?

[Kim Morrison]

(I can't promise to engage at length with an answer here --- but I hope whoever is reviewing these PRs considers the question/answer!)

[Jad Ghalayini]

Kim Morrison said:

Sorry I'm coming to this very late. I admit I am a little skeptical, and would like to see some more explanation of why premonoidal categories are a natural concept (despite working in low-dimensional category theory for many years, I had not met them).

In particular, consider the following question: what if someone later wants to add the (in my mind, better justified) definition of a skew monoidal category (this is one in which the associator is not necessarily invertible). How will the development of monoidal categories look then, if it has to accomodate both? Would it still be viable?

So premonoidal categories are an extremely natural concept in theoretical computer science, since they (very slightly) generalize the Kleisli category of a strong monad over a symmetric monoidal category

[Jad Ghalayini]

I specifically need them to formalize my PhD thesis, which is about using premonoidal categories to model refinement of imperative programs in a variety of complex memory models

[Jad Ghalayini]

I can't think of _too many_ uses in pure mathematics off the top of my head

[Jad Ghalayini]

Skew monoidal categories would be imo no more difficult to implement than they are now, since you'd need to change MonoidalCategoryStruct to not make the associator an isomorphism either way

[Jad Ghalayini]

One particularly important CS-flavored application is https://ncatlab.org/nlab/show/Freyd+category, and in particular a lot of axiomatic domain theory, as well as modeling Lawvere theories

[Jad Ghalayini]

Right now in my library discretion I've got a dirty hack where I essentially copy over the monoidal category implementation as PremonoidalCategory, and it's... not very pretty; I'd much rather just use it from Mathlib and not have to duplicate all that + the tactics

[Jad Ghalayini]

Jad Ghalayini said:

Kim Morrison said:

Sorry I'm coming to this very late. I admit I am a little skeptical, and would like to see some more explanation of why premonoidal categories are a natural concept (despite working in low-dimensional category theory for many years, I had not met them).

In particular, consider the following question: what if someone later wants to add the (in my mind, better justified) definition of a skew monoidal category (this is one in which the associator is not necessarily invertible). How will the development of monoidal categories look then, if it has to accomodate both? Would it still be viable?

So premonoidal categories are an extremely natural concept in theoretical computer science, since they (very slightly) generalize the Kleisli category of a strong monad over a symmetric monoidal category

My longer-term hopes would be to have a large amount of rewriting for monads over arbitrary SMCs (and in particular, for my thesis, the category of partial orders) done in terms of premonoidal categories, and then separately theorems about commutative monads and how, if a monad is commutative, its Kleisli category is in fact monoidal

[Jad Ghalayini]

Lots of interesting things can be written as strong monads over the appropriate category, so hopefully that should open some math applications too other than the extensive theoretical CS applications (in particular, for example, the fact that the free vector space monad is commutative derives a lot of linear algebra in a slick way; on the other hand, the free module monad is not necessarily commutative, and hence induces a premonoidal rather than monoidal category)

[Yuma Mizuno]

Based on Kim's comments, I'd like to review these changes more carefully.

Jad Ghalayini said:

Hello! I realize this PR is very big; do you think it would be worthwhile to split it into some smaller PRs which:

In any case, I think the split of the PR would be better in this PR process. As step zero, would it be possible to first separate the following?: Before introducing Premonoidal, rewrite the definition of monoidal in terms of whiskering and introduce the constructor ofTensorHom.

Regarding introducing of Premonoidal category, my perspective might be based on the following my experience: I previously attempted the above "step zero" as a part of a refactoring of the monoidal category library (though I didn't complete it as it wasn't really necessary at the time). I believe the split of whisker_exchange by introducing Premonoidal category could be done without much effort during that process. While this itself doesn't demonstrate necessity of Premonoidal category definition, it might explain why I am less skepitical to it.

Also, for the split of PRs, would it be possible to postpone the introduction of ltimes and rtimes operators to a later step? To be honest, I'm not yet clear about their need at this point.

(I can't see mathlib this week as I'm traveling without my main PC, sorry about that.)

[Jad Ghalayini]

Yuma Mizuno said:

Based on Kim's comments, I'd like to review these changes more carefully.

Jad Ghalayini said:

Hello! I realize this PR is very big; do you think it would be worthwhile to split it into some smaller PRs which:

In any case, I think the split of the PR would be better in this PR process. As step zero, would it be possible to first separate the following?: Before introducing Premonoidal, rewrite the definition of monoidal in terms of whiskering and introduce the constructor ofTensorHom.

Regarding introducing of Premonoidal category, my perspective might be based on the following my experience: I previously attempted the above "step zero" as a part of a refactoring of the monoidal category library (though I didn't complete it as it wasn't really necessary at the time). I believe the split of whisker_exchange by introducing Premonoidal category could be done without much effort during that process. While this itself doesn't demonstrate necessity of Premonoidal category definition, it might explain why I am less skepitical to it.

Also, for the split of PRs, would it be possible to postpone the introduction of ltimes and rtimes operators to a later step? To be honest, I'm not yet clear about their need at this point.

(I can't see mathlib this week as I'm traveling without my main PC, sorry about that.)

OK, that works, though I might need a bit of time as I have a paper deadline coming up

[Jad Ghalayini]

I can leave ltimes and rtimes out, but really I just view them as syntax sugar for writing down centrality more cleanly, rather than anything fundamental (they're just an abbrev in my PR). Would it be a big add to have them as scoped notation inside PremonoidalCategory?

[Jad Ghalayini]

Since https://github.com/leanprover/lean4/issues/6769 was just merged, do we still want to refactor the MonoidalCategory instances to use the ofTensorHom constructor or should we use default parameters?

[Jad Ghalayini]

I've fixed the merge conflicts, just making sure everything builds (I'm away from home on a tiny laptop, so slow!) before pushing

[Jad Ghalayini]

But if I'll need to split up the PR anyways was wondering whether I should try the default parameter approach or whether using the ofTensorHom constructor is strictly better

[Jad Ghalayini]

Sorry for the inactivity, Thesis Is Hard (TM)

[Yuma Mizuno]

My preference is to use ofTensorHom, not to use tensorHom in PremonoidalCategory. My mental model of tensorHom is horizontally aligned morphisms in a string diagram, which I think is meaningful interpretation only in MonoidalCategory. So what I really expect is like

PremonoidalCategoryStruct
  • left whiskering
  • right whiskering

PremonoidalCategory extends PremonoidalCategoryStruct
  • axioms

MonoidalCategoryStruct extends PremonoidalCategoryStruct
  • tensorHom

MonoidalCategory extends PremonoidalCategory, MonoidalCategoryStruct
  • whiskering_exchange
  • tensorHom_def

[Yuma Mizuno]

Also, I don't think it's a good idea to have a long list of exports, as it hard to maintain. How about basically having the MonoidalCategory namespace even if theorems hold in Premonoidal categories?

[Kevin Buzzard]

We have the RingHom namespace even though stuff applies to semirings