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

- All Categories 2.4K
- Chat 505
- Study Groups 21
- Petri Nets 9
- Epidemiology 4
- Leaf Modeling 2
- Review Sections 9
- MIT 2020: Programming with Categories 51
- MIT 2020: Lectures 20
- MIT 2020: Exercises 25
- Baez ACT 2019: Online Course 339
- Baez ACT 2019: Lectures 79
- Baez ACT 2019: Exercises 149
- Baez ACT 2019: Chat 50
- UCR ACT Seminar 4
- General 75
- Azimuth Code Project 111
- Statistical methods 4
- Drafts 10
- Math Syntax Demos 15
- Wiki - Latest Changes 3
- Strategy 113
- Azimuth Project 1.1K
- - Spam 1
- News and Information 148
- Azimuth Blog 149
- - Conventions and Policies 21
- - Questions 43
- Azimuth Wiki 718

Options

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

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!

`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!`

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'). $$

`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'). \]`