mathlib

e41208d8 - feat(category_theory/monoidal): define monoidal structures on cartesian products of monoidal categories, (lax) monoidal functors and monoidal natural transformations (#13033)

feat(category_theory/monoidal): define monoidal structures on cartesian products of monoidal categories, (lax) monoidal functors and monoidal natural transformations (#13033) This PR contains (fairly straightforward) definitions / proofs of the following facts: - Cartesian product of monoidal categories is a monoidal category. - Cartesian product of (lax) monoidal functors is a (lax) monoidal functor. - Cartesian product of monoidal natural transformations is a monoidal natural transformation. These are prerequisites to defining a monoidal category structure on the category of monoids in a braided monoidal category (with the approach that I've chosen). In particular, the first bullet point above is a prerequisite to endowing the tensor product functor, viewed as a functor from `C × C` to `C`, where `C` is a braided monoidal category, with a strength that turns it into a monoidal functor (stacked PR). This fits as follows into the general strategy for defining a monoidal category structure on the category of monoids in a braided monoidal category `C`, at least conceptually: first, define a monoidal category structure on the category of lax monoidal functors into `C`, and then transport this structure to the category `Mon_ C` of monoids along the equivalence between `Mon_ C` and the category `lax_monoid_functor (discrete punit) C`. All, not necessarily lax monoidal functors into `C` form a monoidal category with "pointwise" tensor product. The tensor product of two lax monoidal functors equals the composition of their cartesian product, which is lax monoidal, with the tensor product on`C`, which is monoidal if `C` is braided. This gives a way to define a tensor product of two lax monoidal functors. The details still need to be fleshed out.