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

- All Categories 2.2K
- Applied Category Theory Course 353
- Applied Category Theory Seminar 4
- Exercises 149
- Discussion Groups 49
- How to Use MathJax 15
- Chat 480
- Azimuth Code Project 108
- News and Information 145
- Azimuth Blog 149
- Azimuth Forum 29
- Azimuth Project 189
- - Strategy 108
- - Conventions and Policies 21
- - Questions 43
- Azimuth Wiki 711
- - Latest Changes 701
- - - Action 14
- - - Biodiversity 8
- - - Books 2
- - - Carbon 9
- - - Computational methods 38
- - - Climate 53
- - - Earth science 23
- - - Ecology 43
- - - Energy 29
- - - Experiments 30
- - - Geoengineering 0
- - - Mathematical methods 69
- - - Meta 9
- - - Methodology 16
- - - Natural resources 7
- - - Oceans 4
- - - Organizations 34
- - - People 6
- - - Publishing 4
- - - Reports 3
- - - Software 21
- - - Statistical methods 2
- - - Sustainability 4
- - - Things to do 2
- - - Visualisation 1
- General 39

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