Howdy, Stranger!

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

Options

Exercise 9 - Chapter 4

edited June 2018

Show that a $$\mathcal{V}$$-profunctor (Definition 4.8) is the same as a function $$\Phi : Ob(\mathcal{X}) \times Ob(\mathcal{Y}) \rightarrow \mathcal{V}$$ such that for any $$x, x' \in \mathcal{X} \text{ and } y, y' \in \mathcal{Y}$$ the following inequality holds in $$\mathcal{V}$$: $$\mathcal{X}(x' , x) \otimes \Phi(x, y) \otimes \mathcal{Y}(y, y' ) \le \Phi(x' , y' )$$ Previous Next

Definition 4.8

Let $$\mathcal{V} = (V, \le, I, \otimes)$$ be a (unital commutative) quantale, and let $$\mathcal{X}$$ and $$\mathcal{Y}$$ be $$\mathcal{V}$$-categories. A $$\mathcal{V}$$-profunctor from $$\mathcal{X}$$ to $$\mathcal{Y}$$, denoted $$\Phi : \mathcal{X} \nrightarrow \mathcal{Y}$$, is a $$\mathcal{V}$$-functor $$\Phi : \mathcal{X}^{op} \times \mathcal{Y} \rightarrow \mathcal{V}$$

• Options
1.
edited June 2018

If we take $$\mathcal{V}$$ to be $$\textbf{Bool} := (\mathbb{B}, \le_{Bool}, \text{true}, \wedge)$$ and $$\mathcal{X}(m, n) := m \le_X n$$, $$\mathcal{Y}(m, n) := m \le_Y n$$, $$\Phi(m, n) := m \le_{\Phi} n$$ , then

$$\mathcal{X}(x' , x) \otimes \Phi(x, y) \otimes \mathcal{Y}(y, y' ) \le_{Bool} \Phi(x' , y' )$$ becomes

$$( x' \le_X x ) \wedge \Phi(x, y) \wedge ( y \le_Y y' ) \le_{Bool} \Phi(x' , y' )$$ Which is (almost) the feasibility relation mentioned in the introduction.

$$\text{ if } x' \le_X x \text{ and } y \le_Y y' \text{ then } \Phi(x, y) \le_{Bool} \Phi(x' , y' )$$ Does the difference in $$\le$$ and "then" matter? Is one of them wrong?

I suppose it is the fact that $$\textbf{Bool}$$ is quantale that makes them equivalent.

Help!

Comment Source:If we take \$$\mathcal{V} \$$ to be \$$\textbf{Bool} := (\mathbb{B}, \le_{Bool}, \text{true}, \wedge) \$$ and \$$\mathcal{X}(m, n) := m \le_X n \$$, \$$\mathcal{Y}(m, n) := m \le_Y n \$$, \$$\Phi(m, n) := m \le_{\Phi} n \$$ , then $\mathcal{X}(x' , x) \otimes \Phi(x, y) \otimes \mathcal{Y}(y, y' ) \le_{Bool} \Phi(x' , y' )$ becomes $( x' \le_X x ) \wedge \Phi(x, y) \wedge ( y \le_Y y' ) \le_{Bool} \Phi(x' , y' )$ Which is (almost) the feasibility relation mentioned in the introduction. $\text{ if } x' \le_X x \text{ and } y \le_Y y' \text{ then } \Phi(x, y) \le_{Bool} \Phi(x' , y' )$ Does the difference in \$$\le \$$ and "then" matter? Is one of them wrong? I suppose it is the fact that \$$\textbf{Bool} \$$ is quantale that makes them equivalent. Help!
• Options
2.
edited July 2018

I think we can show that inequality holds for any commutative quantale, and not just for $$\mathbf{Bool}$$. We start from the definition of enriched functor, since the mapping $$\Phi$$ is a $$\mathcal{V}$$-functor between the $$\mathcal{V}$$-categories $$\mathcal{X}^{\text{op}} \times \mathcal{Y}$$ and $$\mathcal{V}$$:

$$(\mathcal{X}^{\text{op}} \times \mathcal{Y})((x, y), (x', y')) \le \mathcal{V}(\Phi(x, y), \Phi(x', y')).$$ We use the definition of the product of $$\mathcal{V}$$-categories to get

$$\mathcal{X}^{\text{op}}(x, x') \otimes \mathcal{Y}(y, y') \le \mathcal{V}(\Phi(x, y), \Phi(x', y'))$$ and the definition of the opposite of $$\mathcal{V}$$-category to get

$$\mathcal{X}(x', x) \otimes \mathcal{Y}(y, y') \le \mathcal{V}(\Phi(x, y), \Phi(x', y')).$$ By remark 2.86 in the book, we know that we can enrich $$\mathcal{V}$$ in itself using the closed property

$$\mathcal{V}(v, w) = v \multimap w$$ which gives

$$\mathcal{X}(x', x) \otimes \mathcal{Y}(y, y') \le \Phi(x, y) \multimap \Phi(x', y')$$ By applying the definition of the closed element (or hom-object)

$$\mathcal{X}(x', x) \otimes \mathcal{Y}(y, y') \otimes \Phi(x, y) \le \Phi(x', y')$$ and using commutativity of the quantale $$\mathcal{V}$$, we finally show that

$$\mathcal{X}(x', x) \otimes \Phi(x, y) \otimes \mathcal{Y}(y, y') \le \Phi(x', y').$$

Comment Source:I think we can show that inequality holds for any commutative quantale, and not just for \$$\mathbf{Bool}\$$. We start from the definition of enriched functor, since the mapping \$$\Phi\$$ is a \$$\mathcal{V}\$$-functor between the \$$\mathcal{V}\$$-categories \$$\mathcal{X}^{\text{op}} \times \mathcal{Y}\$$ and \$$\mathcal{V}\$$: $(\mathcal{X}^{\text{op}} \times \mathcal{Y})((x, y), (x', y')) \le \mathcal{V}(\Phi(x, y), \Phi(x', y')).$ We use the definition of the product of \$$\mathcal{V}\$$-categories to get $\mathcal{X}^{\text{op}}(x, x') \otimes \mathcal{Y}(y, y') \le \mathcal{V}(\Phi(x, y), \Phi(x', y'))$ and the definition of the opposite of \$$\mathcal{V}\$$-category to get $\mathcal{X}(x', x) \otimes \mathcal{Y}(y, y') \le \mathcal{V}(\Phi(x, y), \Phi(x', y')).$ By remark 2.86 in the book, we know that we can enrich \$$\mathcal{V}\$$ in itself using the closed property $\mathcal{V}(v, w) = v \multimap w$ which gives $\mathcal{X}(x', x) \otimes \mathcal{Y}(y, y') \le \Phi(x, y) \multimap \Phi(x', y')$ By applying the definition of the closed element (or hom-object) $\mathcal{X}(x', x) \otimes \mathcal{Y}(y, y') \otimes \Phi(x, y) \le \Phi(x', y')$ and using commutativity of the quantale \$$\mathcal{V}\$$, we finally show that $\mathcal{X}(x', x) \otimes \Phi(x, y) \otimes \mathcal{Y}(y, y') \le \Phi(x', y').$