Algebras in monoidal categories, bundled or semi-bundled?

Stream: mathlib4

[Yuma Mizuno]

Is there a reason why algebras internal to monoidal categories (Mon_, Mod_, etc.) are designed to be bundled structures?

Would it be reasonable to have a semi-bundled type class approach like [MonoidalCategory C] (X : C) [Mon_ C], just like usual algebra type classes in mathlib?

cc @Kim Morrison

[Joël Riou]

I assume you mean [Mon_ X]? Personally, I would not mind if we had these.

On a similar note, I would think that given a functor F between monoidal categories, we should define a typeclass Functor.Monoidal expressing that a functor F is a monoidal functor (resp. lax/oplax). Similarly, if we have a natural transformation between functors which happen to be monoidal, there should be a typeclass saying that the transformation is compatible with the monoidal structure. (I believe that there is also a use for the category MonoidalFunctor, but sooner or later, we shall construct functors which are both monoidal and triangulated. Then, I think that having only the bundled versions would be suboptimal.)

If we combine the two aspects, we would have instances like:

instance [MonoidalCategory C] [MonoidalCategory D] (X : C)
    [Mon_ X] (F : C ⥤ D) [F.Monoidal] :
    Mon_ (F.obj X) := sorry

[Kim Morrison]

@Joël Riou, unbundled monoidal functors exist already (2019!), but are barely developed.

See file#CategoryTheory/Monoidal/Functorial.

[Joël Riou]

Kim Morrison said:

Joël Riou, unbundled monoidal functors exist already (2019!), but are barely developed.

See file#CategoryTheory/Monoidal/Functorial.

Good. Then, we should consider deduplicating the API. I think that the prime API show be the unbundled API, and we should redefine the bundled version using the unbundled API.

[Yuma Mizuno]

The branch branch#ymizuno-Mon_Cat is trying out the unbundled version of Mon_.

[Yuma Mizuno]

The experience so far was good and I have opened PRs to add the type classes:

1. feat(CategoryTheory/Monoidal): add Mon_Class type class #17185
2. feat(CategoryTheory/Monoidal): add IsMon_Hom type class #17186

These PRs only add definitions and do not modify existing code yet. That will be addressed in subsequent PRs.

[Joël Riou]

In PR #17904, I am refactoring lax/oplax/monoidal functors using typeclasses instead of bundled structures. Given a functor F, one may add instances F.LaxMonoidal, F.OplaxMonoidal or F.Monoidal, instead of defining bundled objects LaxMonoidalFunctor, etc.

[Johan Commelin]

I merged the dependency PR.