Skip to main content
MathOverflow

Return to Answer

edited body
Source Link
varkor
varkor
  • 10.6k
  • 29
  • 72

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 isomorphicequivalent 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 isomorphicequivalent to the original, it is possible when the closed monoidal category in question is the strictification of a monoidal category.

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 isomorphic 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 isomorphic to the original, it is possible when the closed monoidal category in question is the strictification of a monoidal category.

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.

Source Link
varkor
varkor
  • 10.6k
  • 29
  • 72

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 isomorphic 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 isomorphic to the original, it is possible when the closed monoidal category in question is the strictification of a monoidal category.