#### Howdy, Stranger!

It looks like you're new here. If you want to get involved, click one of these buttons!

Options

# Exercise 61 - Chapter 4

$$\def\cat#1{{\mathcal{#1}}}$$ $$\def\Cat#1{{\textbf{#1}}}$$ In order for $$\Cat{1}$$ to be a monoidal unit, there are supposed to be isomorphisms $$\cat{X}\times\Cat{1}\to\cat{X}$$ and $$\Cat{1}\times\cat{X}\to\cat{X}$$, for any $$\cat{V}$$-category $$\cat{X}$$. What are they?

• Options
1.


• Options
2.

Working on the next problem, I realized that my solution above is wrong. In particular, $$\lambda_\cat{X}\circ\lambda^{-1}_\cat{X}=U_{\cat{X}\times\textbf{1}}$$ and $$\lambda^{-1}_\cat{X}\circ\lambda_\cat{X}=U_\cat{X}$$ should hold (by definition of isomorphism), but don't for the above definition of $$\lambda$$.

The correct definition of $$\lambda_\cat{X}$$ is $$\lambda_\cat{X}((x,1),x')=\cat{X}(x,x')$$ and that for $$\lambda^{-1}_\cat{X}$$ is $$\lambda^{-1}_\cat{X}(x,(x',1))=(\cat{X}\times\textbf{1})((x,1),(x',1))$$. It is sufficient to check that $$\lambda_\cat{X}$$ is a profunctor (in the same way as above) and that its composition with its proposed inverse is the identity (in each direction).

\begin{align}(\cat{X}\times\textbf{1})((x',1),(x,1))\otimes\lambda_\cat{X}(x,y)\otimes\cat{X}(y,y')=&(\cat{X}\times\textbf{1})((x',1),(x,1))\otimes\cat{X}(x,y)\otimes\cat{X}(y,y')\\=&(\cat{X}\times\textbf{1})((x',1),(x,1))\otimes\cat{X}(x,y')\\=&\cat{X}(x',x)\otimes\textbf{1}(1,1)\otimes\cat{X}(x,y')\\=&\cat{X}(x',x)\otimes I\otimes\cat{X}(x,y')\\=&\cat{X}(x',x)\otimes\cat{X}(x,y')\\=&\cat{X}(x',y')\\=&\lambda_\cat{X}(x',y')\end{align}. So, $$\lambda_\cat{X}$$ is a profunctor (the proof that $$\lambda_\cat{X}^{-1}$$ is a profunctor is almost exactly the same, exchanging $$\cat{X}\times\textbf{1}$$ and $$\cat{X}$$). This calculation also makes it clear that $$(\cat{X}\times\textbf{1})((x',1),(x,1))\otimes\cat{X}(x,y')=\cat{X}(x',y')\geq I$$, so the defintion in the previous post fails to even be a profunctor.

\begin{align}\lambda^{-1}_\cat{X}\circ\lambda_\cat{X}((x,1),(y,1))&=\bigvee_{z\in\cat{X}}(\cat{X}\times\textbf{1})((x,1),(z,1))\otimes\cat{X}(z,y)\\&=\bigvee_{z\in\cat{X}}(\cat{X}\times\textbf{1})((x,1),(z,1))\otimes(\cat{X}\times\textbf{1})((z,1),(y,1))\\&=(\cat{X}\times\textbf{1})((x,1),(y,1))\\&=U_{\cat{X}\times\textbf{1}}((x,1),(y,1))\end{align}.

\begin{align}\lambda_\cat{X}\circ\lambda^{-1}_\cat{X}(x,y)&=\bigvee_{(z,1)\in\cat{X}\times\textbf{1}}\cat{X}(x,z)\otimes(\cat{X}\times\textbf{1})((z,1),(y,1))\\&=\bigvee_{(z,1)\in\cat{X}\times\textbf{1}}\cat{X}(x,z)\otimes\cat{X}(z,y)\\&=\cat{X}(x,y)\\&=U_\cat{X}(x,y)\end{align}. So, $$\lambda^{-1}_\cat{X}$$ is the inverse of $$\lambda_\cat{X}$$, and they are isomorphisms.

Comment Source:Working on the [next problem](https://forum.azimuthproject.org/discussion/2325/exercise-62-chapter-4), I realized that my solution above is wrong. In particular, \$$\lambda\_\cat{X}\circ\lambda^{-1}\_\cat{X}=U\_{\cat{X}\times\textbf{1}}\$$ and \$$\lambda^{-1}\_\cat{X}\circ\lambda\_\cat{X}=U\_\cat{X}\$$ should hold (by definition of isomorphism), but don't for the above definition of \$$\lambda\$$. The correct definition of \$$\lambda\_\cat{X}\$$ is \$$\lambda\_\cat{X}((x,1),x')=\cat{X}(x,x')\$$ and that for \$$\lambda^{-1}\_\cat{X}\$$ is \$$\lambda^{-1}\_\cat{X}(x,(x',1))=(\cat{X}\times\textbf{1})((x,1),(x',1))\$$. It is sufficient to check that \$$\lambda\_\cat{X}\$$ is a profunctor (in the same way as above) and that its composition with its proposed inverse is the identity (in each direction). \begin{align}(\cat{X}\times\textbf{1})((x',1),(x,1))\otimes\lambda\_\cat{X}(x,y)\otimes\cat{X}(y,y')=&(\cat{X}\times\textbf{1})((x',1),(x,1))\otimes\cat{X}(x,y)\otimes\cat{X}(y,y')\\\\=&(\cat{X}\times\textbf{1})((x',1),(x,1))\otimes\cat{X}(x,y')\\\\=&\cat{X}(x',x)\otimes\textbf{1}(1,1)\otimes\cat{X}(x,y')\\\\=&\cat{X}(x',x)\otimes I\otimes\cat{X}(x,y')\\\\=&\cat{X}(x',x)\otimes\cat{X}(x,y')\\\\=&\cat{X}(x',y')\\\\=&\lambda\_\cat{X}(x',y')\end{align}. So, \$$\lambda\_\cat{X}\$$ is a profunctor (the proof that \$$\lambda\_\cat{X}^{-1}\$$ is a profunctor is almost exactly the same, exchanging \$$\cat{X}\times\textbf{1}\$$ and \$$\cat{X}\$$). This calculation also makes it clear that \$$(\cat{X}\times\textbf{1})((x',1),(x,1))\otimes\cat{X}(x,y')=\cat{X}(x',y')\geq I\$$, so the defintion in the previous post fails to even be a profunctor. \begin{align}\lambda^{-1}\_\cat{X}\circ\lambda\_\cat{X}((x,1),(y,1))&=\bigvee\_{z\in\cat{X}}(\cat{X}\times\textbf{1})((x,1),(z,1))\otimes\cat{X}(z,y)\\\\&=\bigvee\_{z\in\cat{X}}(\cat{X}\times\textbf{1})((x,1),(z,1))\otimes(\cat{X}\times\textbf{1})((z,1),(y,1))\\\\&=(\cat{X}\times\textbf{1})((x,1),(y,1))\\\\&=U\_{\cat{X}\times\textbf{1}}((x,1),(y,1))\end{align}. \begin{align}\lambda\_\cat{X}\circ\lambda^{-1}\_\cat{X}(x,y)&=\bigvee\_{(z,1)\in\cat{X}\times\textbf{1}}\cat{X}(x,z)\otimes(\cat{X}\times\textbf{1})((z,1),(y,1))\\\\&=\bigvee\_{(z,1)\in\cat{X}\times\textbf{1}}\cat{X}(x,z)\otimes\cat{X}(z,y)\\\\&=\cat{X}(x,y)\\\\&=U\_\cat{X}(x,y)\end{align}. So, \$$\lambda^{-1}\_\cat{X}\$$ is the inverse of \$$\lambda\_\cat{X}\$$, and they are isomorphisms.