Commit 2024-11-10 22:57 5b47f116

refactor(CategoryTheory/Monoidal): typeclasses Functor.LaxMonoidal, Functor.OplaxMonoidal and Functor.Monoidal (#17904) Monoidal functors are refactored. Given a functor F : C ⥤ D between monoidal categories, we introduce typeclasses F.LaxMonoidal and F.OplaxMonoidal which carry the data of morphisms like μ : F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y) (or δ : F.obj (X ⊗ Y) ⟶ F.obj X ⊗ F.obj Y). Then, the functor is monoidal if both F.LaxMonoidal and F.OplaxMonoidal and that both data provide inverse isomorphisms. With this design, there is more symmetry between lax and oplax functors (in the bundled setting, this was also experimented upon in #10845 ). (Roughly speaking, what was previously in CategoryTheory.Monoidal.Functorial was generalized.) This is also a change from the previous designs where (lax) monoidal functors were bundled, which would be quite problematic or at least very unpractical in future applications: sooner or later, we shall have functors between derived categories, which are lax/oplax/monoidal, but are also triangulated, and some of these functors shall be adjoints, etc. The bundled aspect was not very much in use before this refactor: it was relevant only when constructing functors from a category of lax monoidal functors; in such case, the corresponding case of bundled lax monoidal functors, etc, have been kept in the code.