Commit 2022-04-03 00:36 e41208d8

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 onC, 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.