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?