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

  • 1.

    \(\newcommand{\cat}[1]{\mathcal{#1}}\def\op{{^\mathrm{op}}}\newcommand{\Ob}[1]{\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}[1]{\mathcal{#1}}\def\op{{^\mathrm{op}}}\newcommand{\Ob}[1]{\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)\\)).
  • 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.