Howdy, Stranger!

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

Options

Exercise 79 - Chapter 2

edited June 2018

Condition Eq. (2.77) says precisely that we have a Galois connection in the sense of Definition 1.78. Let’s prove this fact. In particular, we’ll prove that a monoidal preorder is monoidal closed if, given any $$v \in V$$, the map $$− \otimes v : V \rightarrow V$$ given by multiplying with $$v$$ has a right adjoint. We write this right adjoint $$v \multimap : V \rightarrow V$$.

1. Using Definition 2.2, show that $$− \otimes v$$ is monotone.
2. Supposing that $$V$$ is closed, show that for all $$a, v \in V$$ we have $$(v \multimap a) \otimes v \le a$$.
3. Using 2., show that $$v \multimap −$$ is monotone.
4. Conclude that a symmetric monoidal preorder is closed if and only if the monotone map $$− \otimes v$$ has a right adjoint.

• Options
1.
edited June 2018
1. Using property a of Definition 2.2, taking $$v := x_2 = y_2$$ and substituting $$x$$ for $$x_1$$, $$y$$ for $$y_1$$, we get "if $$x \leq y$$ then $$x \otimes v \leq y \otimes v$$, which precisely means that $$− \otimes v$$ is monotone.

2. $$(v \multimap a) \leq (v \multimap a)$$ so by going from right to left in the definition of closedness we have $$(v \multimap a) \otimes v \leq a$$.

3. We need to show that if $$a \leq b$$, that $$(v \multimap a) \leq (v \multimap b)$$. Combining the result from part 2 with $$a \leq b$$ we have $$(v \multimap a) \otimes v \leq b$$. Now going from left to right in the definition of closedness, we have $$(v \multimap a) \leq (v \multimap b)$$.

4. We just showed that if $$\mathcal{V}$$ is closed then the two functions $$− \otimes v$$ and $$v \multimap -$$ are monotone; Equation 2.77 gives all that is then needed for a Galois connection. In the reverse, if we have right adjoints $$g_v$$ for each $$− \otimes v$$, Equation 1.81 of Definition 1.80 gives us Equation 2.77.

Comment Source:1. Using property a of Definition 2.2, taking \$$v := x_2 = y_2\$$ and substituting \$$x\$$ for \$$x_1\$$, \$$y\$$ for \$$y_1\$$, we get "if \$$x \leq y\$$ then \$$x \otimes v \leq y \otimes v\$$, which precisely means that \$$− \otimes v \$$ is monotone. 2. \$$(v \multimap a) \leq (v \multimap a) \$$ so by going from right to left in the definition of closedness we have \$$(v \multimap a) \otimes v \leq a \$$. 3. We need to show that if \$$a \leq b\$$, that \$$(v \multimap a) \leq (v \multimap b) \$$. Combining the result from part 2 with \$$a \leq b\$$ we have \$$(v \multimap a) \otimes v \leq b \$$. Now going from left to right in the definition of closedness, we have \$$(v \multimap a) \leq (v \multimap b) \$$. 4. We just showed that if \$$\mathcal{V}\$$ is closed then the two functions \$$− \otimes v \$$ and \$$v \multimap - \$$ are monotone; Equation 2.77 gives all that is then needed for a Galois connection. In the reverse, if we have right adjoints \$$g_v\$$ for each \$$− \otimes v \$$, Equation 1.81 of Definition 1.80 gives us Equation 2.77.