#### 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?

## Comments

• Options
1.

$$\newcommand{\cat}{\mathcal{#1}}\def\op{{^\mathrm{op}}}\newcommand{\Ob}{\mathrm{Ob}(#1)}\cat{X}$$ and 1 are $$\cat{V}$$-categories. A morphism in the profunctor category over $$\cat{V}$$, i.e., $$\textbf{Prof}_\cat{V}$$, is a $$\cat{V}$$-profunctor. Therefore, one must produce a $$\cat{V}$$-functor $$\lambda:(\cat{X}\times\textbf{1})\op\times\cat{X}\to\cat{V}$$. By the exercise following the definition $$\cat{V}$$-profunctor, it is sufficient to specify a function $$\lambda:\Ob{\cat{X}\times\textbf{1}}\times\Ob{\cat{X}}\to\cat{V}$$ such that $(\cat{X}\times\textbf{1})(x',x)\otimes\lambda(x,y)\otimes\cat{X}(y,y')\leq_\cat{V}\lambda(x',y')\quad\forall x,x'\in\cat{X}\times\textbf{1}\,\text{and}\,\forall y,y'\in\cat{X}$. Define $\lambda(\tilde{x},x')=\lambda((x,1),x'):=\begin{cases}I\,\,\text{if}\,\,x=x'\\0\,\,\text{otherwise}\end{cases}$ (note that $$0$$ exists since $$\cat{V}$$ is a quantale). It follows that \begin{align}\forall \tilde{x},\tilde{x}'\in\cat{X}\times\textbf{1}\,\text{and}\,\forall y,y'\in\cat{X}\quad(\cat{X}\times\textbf{1})(\tilde{x}',\tilde{x})\otimes\lambda(x,y)\otimes\cat{X}(y,y')=&(\cat{X}\times\textbf{1})((x',1),(x,1))\otimes\lambda(x,y)\otimes\cat{X}(y,y')\\=&\begin{cases}(\cat{X}\times\textbf{1})((x',1),(x,1))\otimes I\otimes\cat{X}(x,y')\,\,\text{if}\,\,x=y\\0\,\,\text{otherwise}\end{cases}\\=&\begin{cases}(\cat{X}\times\textbf{1})((x',1),(x,1))\otimes\cat{X}(x,y')\,\,\text{if}\,\,x=y\\0\,\,\text{otherwise}\end{cases}\\=&\begin{cases}I\,\,\text{if}\,\,x'=y'\\0\,\,\text{otherwise}\end{cases}\\=&\lambda(\tilde{x}',y')\end{align}. So, $$\lambda:\cat{X}\times\textbf{1}\nrightarrow\cat{X}$$ is a profunctor. Its inverse is its opposite (i.e., $$\lambda^{-1}(y,\tilde{x})=\lambda(\tilde{x},y)$$. The profunctor $$\rho:\textbf{1}\times\cat{X}\nrightarrow\cat{X}$$ can be defined similarly (i.e., $$\rho(\hat{x},y)=\rho((1,x),y)=\begin{cases}I\,\,\text{if}\,\,x=y\\0\,\,\text{otherwise}\end{cases}$$, with proof that it is a profunctor the same as that for $$\lambda$$ above except replacing $$\cat{X}\times\textbf{1}$$ by $$\textbf{1}\times\cat{X}$$ and associated necessary changes), and is also an isomorphism (again, with inverse given by its opposite $$\rho^{-1}(y,\hat{x})=\rho(\hat{x},y)$$).

Comment Source:\$$\newcommand{\cat}{\mathcal{#1}}\def\op{{^\mathrm{op}}}\newcommand{\Ob}{\mathrm{Ob}(#1)}\cat{X}\$$ and **1** are \$$\cat{V}\$$-categories. A morphism in the profunctor category over \$$\cat{V}\$$, i.e., \$$\textbf{Prof}\_\cat{V}\$$, is a \$$\cat{V}\$$-profunctor. Therefore, one must produce a \$$\cat{V}\$$-functor \$$\lambda:(\cat{X}\times\textbf{1})\op\times\cat{X}\to\cat{V}\$$. By the exercise following the definition \$$\cat{V}\$$-profunctor, it is sufficient to specify a function \$$\lambda:\Ob{\cat{X}\times\textbf{1}}\times\Ob{\cat{X}}\to\cat{V}\$$ such that \$(\cat{X}\times\textbf{1})(x',x)\otimes\lambda(x,y)\otimes\cat{X}(y,y')\leq\_\cat{V}\lambda(x',y')\quad\forall x,x'\in\cat{X}\times\textbf{1}\,\text{and}\,\forall y,y'\in\cat{X}\$. Define \$\lambda(\tilde{x},x')=\lambda((x,1),x'):=\begin{cases}I\,\,\text{if}\,\,x=x'\\\\0\,\,\text{otherwise}\end{cases}\$ (note that \$$0\$$ exists since \$$\cat{V}\$$ is a quantale). It follows that \begin{align}\forall \tilde{x},\tilde{x}'\in\cat{X}\times\textbf{1}\,\text{and}\,\forall y,y'\in\cat{X}\quad(\cat{X}\times\textbf{1})(\tilde{x}',\tilde{x})\otimes\lambda(x,y)\otimes\cat{X}(y,y')=&(\cat{X}\times\textbf{1})((x',1),(x,1))\otimes\lambda(x,y)\otimes\cat{X}(y,y')\\\\=&\begin{cases}(\cat{X}\times\textbf{1})((x',1),(x,1))\otimes I\otimes\cat{X}(x,y')\,\,\text{if}\,\,x=y\\\\0\,\,\text{otherwise}\end{cases}\\\\=&\begin{cases}(\cat{X}\times\textbf{1})((x',1),(x,1))\otimes\cat{X}(x,y')\,\,\text{if}\,\,x=y\\\\0\,\,\text{otherwise}\end{cases}\\\\=&\begin{cases}I\,\,\text{if}\,\,x'=y'\\\\0\,\,\text{otherwise}\end{cases}\\\\=&\lambda(\tilde{x}',y')\end{align}. So, \$$\lambda:\cat{X}\times\textbf{1}\nrightarrow\cat{X}\$$ is a profunctor. Its inverse is its opposite (i.e., \$$\lambda^{-1}(y,\tilde{x})=\lambda(\tilde{x},y)\$$. The profunctor \$$\rho:\textbf{1}\times\cat{X}\nrightarrow\cat{X}\$$ can be defined similarly (i.e., \$$\rho(\hat{x},y)=\rho((1,x),y)=\begin{cases}I\,\,\text{if}\,\,x=y\\\\0\,\,\text{otherwise}\end{cases}\$$, with proof that it is a profunctor the same as that for \$$\lambda\$$ above except replacing \$$\cat{X}\times\textbf{1}\$$ by \$$\textbf{1}\times\cat{X}\$$ and associated necessary changes), and is also an isomorphism (again, with inverse given by its opposite \$$\rho^{-1}(y,\hat{x})=\rho(\hat{x},y)\$$).
• 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.
Sign In or Register to comment.