Jade wrote:

> Why do we need prove this extra condition about the monoidal product commuting with joins?

We don't "need to" prove it. As mathematicians we _enjoy_ proving stuff.

The reason this condition is cool is the following theorem, which gives _two equivalent conditions_ for \\(\mathcal{V}\\) to be a quantale:

**Theorem.** If \\(\mathcal{V}\\) is a monoidal poset with all joins, \\(\mathcal{V}\\) is closed if and only if

\[ a \otimes \left( \bigvee\_{b\in B} b\right) = \bigvee\_{b \in A} (a \otimes b) \]

for every element \\(a\\) and every subset \\(B\\) of \\(\mathcal{V}\\).

So, we can either say a quantale is a monoidal poset with all joins that is _closed_, or a monoidal poset with all joins where _tensoring distributes over all joins._

This is especially cool when you realize that \\(\otimes\\) is like multiplication, being closed is like having division, and joins are like (possibly infinite) sums. It's almost as if we're saying multiplication distributes over sums iff we can divide!

That's not true in plain old algebra, but here we are doing 'slightly categorified' algebra, working with posets rather than mere sets, and defining our 'sums' by a universal property... so we have new magic powers.

**Proof Sketch.** For every element \\(a\\) of \\(\mathcal{V}\\) there is a monotone function

\[ a \otimes - \, \colon \mathcal{V} \to \mathcal{V} \]

sending each \\(x \in \mathcal{V}\\) to \\(a \otimes x\\) . By the [Adjoint Functor Theorem for Posets](https://forum.azimuthproject.org/discussion/2031/lecture-16-chapter-1-the-adjoint-functor-theorem-for-posets/p1), this monotone function has a right adjoint iff it preserves all joins. It a right adjoint iff \\(\mathcal{V}\\) is closed, since \\(\mathcal{V}\\) being closed says that

\[ a \otimes x \le y \text{ if and only if } x \le a \multimap y \]

for all \\(x, y\\) in \\(\mathcal{V}\\), which means that

\[ a \multimap - \, \colon \mathcal{V} \to \mathcal{V} \]

is a right adjoint of

\[ a \otimes - \, \colon \mathcal{V} \to \mathcal{V} \]

On the other hand, \\(a \otimes -\\) preserves all joins iff

\[ a \otimes \left( \bigvee\_{b\in B} b\right) = \bigvee\_{b \in B} (a \otimes b) \]

for every element \\(a\\) and every subset \\(B\\) of \\(\mathcal{V}\\). \\( \qquad \blacksquare \\)