The term closed in the context of symmetric monoidal closed preorders refers to the fact that a hom-element can be constructed from any two elements (the preorder is closed under the operation of "taking homs").
Consider the hom-element \(v \multimap w\) as a kind of "single use v to w converter"
a and v are enough to get to w iff a is enough to get to a single-use v-to-w converter.
One may read
A symmetric monoidal preorder \(\mathcal{V}:=(V,\leq,I,\otimes)\) is symmetric monoidal closed (or just closed)
For every \(v,w \in V\), there is an element \(v \multimap w \in V\) called the hom-element with the property:
\(\forall a,v,w \in V: (a \otimes v) \leq w\) iff \(a \leq (v \multimap w)\)
A category \(\mathcal{V}\) that is enriched in itself.
For every \(v,w \in Ob(\mathcal{V})\) we can define \(\mathcal{V}(v,w)\) as \((v \multimap w) \in \mathcal{V}\)
For this to be an enrichment, we need to check the two conditions.
The first condition \(I \leq \mathcal{X}(x,x) = x \multimap x\) is satsified because \(I \otimes x \leq x\)
The second condition is satisfied by P2.87e
The symmetric monoidal preorder \(\mathbf{Cost}:=([0,\infty],\geq,0,+)\) is monoidal closed.
For any \(x,y \in [0,\infty]\), define \(x \multimap y := max(0,y-x)\)
Then, for any \(a,x,y\), we have \(a+x\geq y\) iff \(a \geq y-x\) iff \(max(0,a)\geq max(0,y-x)\) iff \(a \geq (x \multimap y)\)
We can use this to define a notion of subtraction in Cost.
What would a monoidal closed structure mean for the resource theory of chemistry?
For any two material collections, one can form a material collection \(c \multimap d\) with the property that, for any a one has \(a + c \rightarrow d\) iff \(a \rightarrow (c \multimap d)\)
Concretely, say we have \(2 H_2O + 2 Na \rightarrow 2 NaOH + H_2\), we must also have \(2H_2O \rightarrow (2Na \multimap (2NaOH+H_2))\)
From two molecules of water, you can form a certain substance. This doesn’t make sense, so maybe this symmetric monoidal preorder is not closed.
Alternatively, think of the substance \(2Na \multimap (2NaOH+H_2)\) as a potential reaction, that of converting sodium to sodium-hyroxide+hydrogen. Two molecules of water unlock that potential. NOCARD
The meaning of \((- \otimes v) \dashv (v \multimap -)\) is exactly the condition of \(\multimap\) in a closed symmetric monoidal preorder.
This follows from (1), using the fact that left adjoints preserve joins.
This follows from (1) using the alternative characterization of Galois connections.
Alternatively, start from definition of closed symmetric monoidal preorder and substitute \(v \multimap w\) for \(a\), and note by reflexivity that \((v \multimap w) \leq (v \multimap w)\)
Then we obtain \((v \multimap w) \otimes v \leq w\) (by symmetry of \(\otimes\) we are done)
Since \(v \otimes I = v \leq v\), then the closed condition means that \(v \leq I \multimap v\)
For the other direction, we have \(I \multimap v = I \otimes (I \multimap v) \leq v\) by (3)
We need \(u \otimes (u \multimap v) \otimes (v \multimap w) \leq w\)
This follows from two applications of the third part of this proposition.
Suppose \(\mathcal{V}:=(V,\leq,I,\otimes,\multimap)\) is a closed symmetric monoidal preorder.
For every \(v \in V\) the monotone map \((V, \leq) \xrightarrow{-\otimes v}(V,\leq)\) is left adjoint to \((V, \leq)\ \xrightarrow{v \multimap -} (V,\leq)\)
For any element \(v \in V\) and a subset of elements \(A \subseteq V\), if the join \(\bigvee A\) exists, then so does \(\bigvee_{a \in A} v \otimes a\) and we have \((v \otimes \bigvee A)\cong \bigvee_{a \in A} v \otimes a\)
\(\forall v,w \in V: v \otimes (v \multimap w) \leq w\)
\(\forall v \in V: v \cong (I \multimap v)\)
\(\forall u,v,w \in V: (u \multimap v) \otimes (v \multimap w) \leq (u \multimap w)\)
Prove that a symmetric monoidal preorder is closed iff, given any \(v \in V\), the map \(V \xrightarrow{(-\otimes v)}V\) given by multiply with v has a right adjoint. We write this adjoint \(V \xrightarrow{(v \multimap -)}V\):
Show that \(V \xrightarrow{(-\otimes v)}V\) is monotone.
Supposing that \(\mathcal{V}\) is closed, show that \(\forall v,w \in V: ((v \multimap w)\otimes v) \leq w\)
Show that \((v \multimap -)\) is monotone.
Conclude that a symmetric monoidal preorder is closed iff the monotone map \((- \otimes v)\) has a right adjoint.
Given the monotonicity constraint of \(\otimes\)
And reflexivity: \(v \leq v\), we have:
\(x_1 \leq y_1\) implies that \((x_1 \otimes v) \leq (y_1 \otimes v)\)
Substitute \(v \multimap w\) for \(a\) into the closed property equation, to get \(((v \multimap w)\otimes v) \leq w \iff v \multimap w \leq v \multimap w\) (the RHS is true by reflexivity, so the LHS must be true).
Need to show: if we assume \(x \leq y\) then we can conclude \((v \multimap x) \leq (v \multimap y)\)
From the previous part, we have \((v \multimap x) \otimes v \leq x\) and \((v \multimap y) \otimes v \leq y\)
Assuming the antecedant \(x \leq y\), and given transitivity, we have \((v \multimap x) \otimes v \leq (v \multimap y) \otimes v\)
Because the \(\otimes\) operation must be monotonic, the consequent follows.
A Galois connection requires that both maps be monotone and that they satisfy \(f(p)\leq q\) iff \(p \leq g(q)\). This is the relation captured by the closed property equation, and both maps were shown to be monotone.
Show that \(\mathbf{Bool}=(\mathbb{B},\leq, true, \land)\) is monoidal closed.
Our translation is: \(\otimes \mapsto \land,\ \leq \mapsto \implies\)
Condition for being closed is then:
\(\forall a,v,w:\) \((a \land v) \implies w\) iff \(a \implies (v \multimap w)\)
On the LHS, we have the truth table:
| a | v | w | \((a \land v) \implies w\) |
|---|---|---|---|
| F | F | F | T |
| F | F | T | T |
| F | T | F | T |
| F | T | T | T |
| T | F | F | T |
| T | F | T | T |
| T | T | F | F |
| T | T | T | T |
In order to define \(v \multimap w\) in a way consistent with this, we need it to only be false when \(v=true, w=false\), which is the truth condition for \(v \implies w\).
This is consistent with a ‘single use v-to-w converter’ analogy.