Hey Simon,
Sure, I can try your proofs. I will try to prove the stronger statement.
A lot of this is just reproving the adjoint functor theorem for posets, but I am trying to internalize this stuff so I am reviewing it.
> Suppose \\(\mathcal{V}\\) is a monoidal partial order which has all joins, then \\(\mathcal{V}\\) is closed if and only if the monoidal product distributes over joins.
**Proof.**
Let \\(\mathcal{V} = (V, \leq, \otimes, I, \bigvee)\\) be a monoidal partial order with arbitrary joins \\(\bigvee\\).
**Closed** \\(\implies\\) **Distributivity**: Assume \\(\mathcal{V}\\) is closed. Then \\(\mathcal{V}\\) has a [residual](https://en.wikipedia.org/wiki/Residuated_lattice) \\(\multimap : V \to V \to V\\) such that \\(a \otimes - \dashv a \multimap -\\). Using this Galois connection we have
\[
\begin{align}
\bigvee (a \otimes x) \leq y
& \iff \forall x. a \otimes x \leq y \\\\
& \iff \forall x. x \leq a \multimap y \\\\
& \iff \bigvee x \leq a \multimap y \\\\
& \iff a \otimes \bigvee x \leq y
\end{align}
\]
Hence \\(\bigvee (a \otimes x) \leq y \iff a \otimes \bigvee x \leq y\\).
Since \\(\bigvee (a \otimes x) \leq \bigvee (a \otimes x) \\) we have \\(a \otimes \bigvee x \leq \bigvee (a \otimes x). \\)
Moreover, because \\(a \otimes \bigvee x \leq a \otimes \bigvee x \\) we have \\(\bigvee (a \otimes x) \leq a \otimes \bigvee x. \\)
Hence \\(\bigvee (a \otimes x) = a \otimes \bigvee x \\) since \\(\mathcal{V}\\) is a partial order.
**Distributivity** \\(\implies\\) **Closed**: Assume that \\(\mathcal{V}\\) distributes \\(\otimes\\) over \\(\bigvee\\). To show that \\(\mathcal{V}\\) is closed, we need a right adjoint to \\(a \otimes -\\). Using the old result from [Lecture 6](https://forum.azimuthproject.org/discussion/1901/lecture-6-chapter-1-computing-adjoints/), if the right adjoint \\(a \multimap -\\) does exist it is defined by:
\[ a \multimap y := \bigvee\lbrace x\mid a\otimes x \leq y\rbrace \]
In order to establish \\(a \otimes - \dashv a \multimap -\\), we need to show:
\[
a \otimes x \leq y \iff x \leq a \multimap y
\]
The forward direction is simple and does not rely on distributivity. Assume \\(a \otimes x \leq y\\). Then we know that \\(x \in \lbrace x \mid a \otimes x \leq y \rbrace\\) hence \\( x \leq \bigvee \lbrace x \mid a \otimes x \leq y \rbrace \\), which is the same as \\(x \le a \multimap y\\).
The converse requires distributivity. Assume \\(x \leq \bigvee \lbrace x \mid a \otimes x \leq y \rbrace\\). Since \\(a \otimes -\\) is monotonic we have
\[
a \otimes x \leq a \otimes \bigvee \lbrace x \mid a \otimes x \leq y \rbrace
\]
So it suffices to show \\(a \otimes \bigvee \lbrace x \mid a \otimes x \leq y \rbrace \leq y\\).
Since \\(\mathcal{V}\\) is distributive by hypothesis, we have:
\[
a \otimes \bigvee \lbrace x \mid a \otimes x \leq y \rbrace = \bigvee \lbrace a \otimes x \mid a \otimes x \leq y \rbrace
\]
However we can see that \\(y\\) is an upper bound of \\(\lbrace a \otimes x \mid a \otimes x \leq y \rbrace\\), hence \\( \bigvee \lbrace a \otimes x \mid a \otimes x \leq y \rbrace \leq y\\), and thus the theorem by distributivity. \\( \qquad \blacksquare \\)
-----------------------------
I have been thinking about the assumption that \\(\mathcal{V}\\) has arbitrary joins.
Is there a closed monoidal partial order which does not have arbitrary joins?
Sure, I can try your proofs. I will try to prove the stronger statement.
A lot of this is just reproving the adjoint functor theorem for posets, but I am trying to internalize this stuff so I am reviewing it.
> Suppose \\(\mathcal{V}\\) is a monoidal partial order which has all joins, then \\(\mathcal{V}\\) is closed if and only if the monoidal product distributes over joins.
**Proof.**
Let \\(\mathcal{V} = (V, \leq, \otimes, I, \bigvee)\\) be a monoidal partial order with arbitrary joins \\(\bigvee\\).
**Closed** \\(\implies\\) **Distributivity**: Assume \\(\mathcal{V}\\) is closed. Then \\(\mathcal{V}\\) has a [residual](https://en.wikipedia.org/wiki/Residuated_lattice) \\(\multimap : V \to V \to V\\) such that \\(a \otimes - \dashv a \multimap -\\). Using this Galois connection we have
\[
\begin{align}
\bigvee (a \otimes x) \leq y
& \iff \forall x. a \otimes x \leq y \\\\
& \iff \forall x. x \leq a \multimap y \\\\
& \iff \bigvee x \leq a \multimap y \\\\
& \iff a \otimes \bigvee x \leq y
\end{align}
\]
Hence \\(\bigvee (a \otimes x) \leq y \iff a \otimes \bigvee x \leq y\\).
Since \\(\bigvee (a \otimes x) \leq \bigvee (a \otimes x) \\) we have \\(a \otimes \bigvee x \leq \bigvee (a \otimes x). \\)
Moreover, because \\(a \otimes \bigvee x \leq a \otimes \bigvee x \\) we have \\(\bigvee (a \otimes x) \leq a \otimes \bigvee x. \\)
Hence \\(\bigvee (a \otimes x) = a \otimes \bigvee x \\) since \\(\mathcal{V}\\) is a partial order.
**Distributivity** \\(\implies\\) **Closed**: Assume that \\(\mathcal{V}\\) distributes \\(\otimes\\) over \\(\bigvee\\). To show that \\(\mathcal{V}\\) is closed, we need a right adjoint to \\(a \otimes -\\). Using the old result from [Lecture 6](https://forum.azimuthproject.org/discussion/1901/lecture-6-chapter-1-computing-adjoints/), if the right adjoint \\(a \multimap -\\) does exist it is defined by:
\[ a \multimap y := \bigvee\lbrace x\mid a\otimes x \leq y\rbrace \]
In order to establish \\(a \otimes - \dashv a \multimap -\\), we need to show:
\[
a \otimes x \leq y \iff x \leq a \multimap y
\]
The forward direction is simple and does not rely on distributivity. Assume \\(a \otimes x \leq y\\). Then we know that \\(x \in \lbrace x \mid a \otimes x \leq y \rbrace\\) hence \\( x \leq \bigvee \lbrace x \mid a \otimes x \leq y \rbrace \\), which is the same as \\(x \le a \multimap y\\).
The converse requires distributivity. Assume \\(x \leq \bigvee \lbrace x \mid a \otimes x \leq y \rbrace\\). Since \\(a \otimes -\\) is monotonic we have
\[
a \otimes x \leq a \otimes \bigvee \lbrace x \mid a \otimes x \leq y \rbrace
\]
So it suffices to show \\(a \otimes \bigvee \lbrace x \mid a \otimes x \leq y \rbrace \leq y\\).
Since \\(\mathcal{V}\\) is distributive by hypothesis, we have:
\[
a \otimes \bigvee \lbrace x \mid a \otimes x \leq y \rbrace = \bigvee \lbrace a \otimes x \mid a \otimes x \leq y \rbrace
\]
However we can see that \\(y\\) is an upper bound of \\(\lbrace a \otimes x \mid a \otimes x \leq y \rbrace\\), hence \\( \bigvee \lbrace a \otimes x \mid a \otimes x \leq y \rbrace \leq y\\), and thus the theorem by distributivity. \\( \qquad \blacksquare \\)
-----------------------------
I have been thinking about the assumption that \\(\mathcal{V}\\) has arbitrary joins.
Is there a closed monoidal partial order which does not have arbitrary joins?
Version 2.1.8p2
