Options

Exercise 9 - Chapter 4

edited June 2018 in Exercises

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} $$

Comments

  • 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!
  • 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'). \]
Sign In or Register to comment.