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 719

Options

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 \).

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

## Comments

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.

\( (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 \).

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) \).

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.

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