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?