7
$\begingroup$

The strictification theorem for monoidal categories states that every monoidal categorically is monoidally equivalent to a strict monoidal category. Is there a strictification theorem for closed monoidal categories? I expect this to take a form similar to the following.

Call a closed monoidal category strict if the monoidal structure is strict and the following canonical isomorphisms are identities: $$[I, X] \cong X$$ $$[X, [Y, Z]] \cong [X \otimes Y, Z]$$

I believe that the first identity should follow from a strictification theorem for closed categories, so that the strictification theorem for closed monoidal categories is the union of the strictification theorems for monoidal categories, closed categories, along with the additional axiom governing the interaction between the monoidal and closed structures given by currying.

This seems like a natural question to ask, and so I would not be surprised to find it in the literature already, but I have not been able to do so.

$\endgroup$
8
  • $\begingroup$ I find this unlikely $\endgroup$ Commented Sep 19, 2021 at 15:07
  • 1
    $\begingroup$ I'm reasonably sure it is true, and think I can prove it using a syntactic argument, but there are quite a number of conditions to check, and I would hope there was either a more elegant argument, or a proof already in the literature. $\endgroup$
    – varkor
    Commented Sep 19, 2021 at 17:17
  • 2
    $\begingroup$ So, how would you do it for the category of sets? I'm really curious. $\endgroup$ Commented Sep 19, 2021 at 17:49
  • $\begingroup$ The first thing that comes to mind for me is a theorem of Mike Shulman's: every closed monoidal category embeds fully faithfully into a star-autonomous monoidal category. For a star-autonomous category, I'm tempted to say that some sort of strictification theorem will follow from the usual strictification of monoidal categories... It seems relevant that the star-autonomous structure is almost definable in terms of the monoidal structure. $\endgroup$ Commented Sep 21, 2021 at 12:17
  • 6
    $\begingroup$ One possible abstract approach would be to express closed monoidal categories as pseudoalgebras for a 2-monad (on the 2-category of categories, functors, and natural isomorphisms, because there is contravariance) and try to apply a general strictification theorem for pseudoalgebras for 2-monads. $\endgroup$ Commented Sep 21, 2021 at 16:02

1 Answer 1

3
$\begingroup$

I have not been able to find an explicit reference for this in the literature, so I will sketch a proof here. Steve Lack suggested that one could make use of Mac Lane's proof of strictification for monoidal categories, by showing that it may be refined in the case that the monoidal category is furthermore closed.

Let $(\mathcal C, \otimes, I, [{-}, {-}])$ be a closed monoidal category. Following Theorem XI.3.1 of Categories for the Working Mathematician, there is a strict monoidal category $\mathcal C'$ that is monoidally equivalent to $\mathcal C$, whose set of objects is the free monoid on $|\mathcal C|$ and whose category structure is induced by the full image of the canonical functor $|\mathcal C|^* \to \mathcal C$ (using that $\mathcal C$ is monoidal).

We will show that $\mathcal C'$ may also be equipped with closed structure such that the unit and transposition laws hold strictly. We define a function $\multimap : \mathcal C'^{\text{op}} \times \mathcal C' \to \mathcal C'$ as follows, which inherits functoriality from $[{-}, {-}]$.

$$(x_1, \ldots, x_n) \multimap \vec y := [x_1, [x_2, \ldots, [x_n, \vec y] \ldots ]]$$

This indeed forms a closed structure, since:

$$\mathcal C'((\vec w, \vec x), \vec y) \\ = \mathcal C(w_1 \otimes \cdots \otimes x_n, y_1 \otimes \cdots y_m) \\ \cong \mathcal C(w_1 \otimes \ldots \otimes w_o, [x_1, [x_2, \ldots, [x_n, y_1 \otimes \cdots \otimes y_m] \ldots ]]) \\ = \mathcal C'(\vec w, \vec x \multimap \vec y)$$

and will be preserved by the monoidal equivalence between $\mathcal C$ and $\mathcal C'$, since it is equivalent to the closed structure on $\mathcal C'$ induced by the equivalence. It remains to check that this new closed structure is in fact strict.

For strict unitality, we have that the canonical isomorphism is given by instantiating the following at the identity:

$$\mathcal C'(\vec x, () \multimap \vec x) = \mathcal C(x_1 \otimes \cdots x_n, x_1 \otimes \cdots x_n) = \mathcal C'(\vec x, \vec x)$$

For strict transposition, we have that the canonical isomorphism is given by instantiating the following at the identity:

$$\mathcal C'((\vec w, \vec x) \multimap \vec y, \vec w \multimap \vec x \multimap \vec y) = \mathcal C([w_1, \ldots, [y_1, \ldots, [y_m, x_1 \otimes \cdots \otimes x_n] \ldots ]]], [w_1, \ldots, [y_1, \ldots, [y_m, x_1 \otimes \cdots \otimes x_n] \ldots ]]]) = \mathcal C'(\vec w \multimap \vec x \multimap \vec y, \vec w \multimap \vec x \multimap \vec y)$$

More abstractly, this establishes that, while it may not be possible, given an arbitrary closed monoidal category, to find a new strict closed structure equivalent to the original, it is possible when the closed monoidal category in question is the strictification of a monoidal category.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .