Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(category_theory/monoidal): define monoidal structures on cartesi…
…an 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.
- Loading branch information
Showing
4 changed files
with
170 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters