Posets help us talk about resources: the partial ordering \$$x \le y\$$ says when you can use one resource to get another. Monoidal posets let us combine or 'add' two resources \$$x\$$ and \$$y\$$ to get a resource \$$x \otimes y\$$. But closed monoidal posets go further and let us 'subtract' resources! And the main reason for subtracting resources is to answer questions like

> _If you have \$$x\$$, what must you combine it with to get \$$y\$$?_

When dealing with money the answer to this question is called \$$y - x\$$, but now we will call it \$$x \multimap y\$$. Remember, we say a monoidal poset is **closed** if for any pair of elements \$$x\$$ and \$$y\$$ there's an element \$$x \multimap y\$$ that obeys the law

$x \otimes a \le y \text{ if and only if } a \le x \multimap y .$

This says roughly "if \$$x\$$ combined with \$$a\$$ is no more than \$$y\$$, then \$$a\$$ is no more than what you need to combine with \$$x\$$ to get \$$y\$$". Which sounds complicated, but makes sense on reflection.

One reason for using funny symbols like \$$\otimes\$$ and \$$\multimap\$$ is that they don't have strongly pre-established meanings. Sometimes they mean addition and subtraction, but sometimes they will mean multiplication and division.

For example, we can take any set and make it into a poset by saying \$$x \le y\$$ if and only if \$$x = y\$$: this is called a **discrete poset**. If our set is a monoid we can make it into a monoidal poset where \$$x \otimes y \$$ is defined to be \$$x y\$$. And if our set is a _group_ we can make it into a _closed_ monoidal poset where \$$x \multimap y\$$ is \$$y\$$ divided by \$$x\$$, or more precisely \$$x^{-1} y\$$, since we have

$x a = y \text{ if and only if } a = x^{-1} y .$

I said last time that if \$$\mathcal{V}\$$ is a closed monoidal poset we can make it into a \$$\mathcal{V}\$$-enriched category where:

* the objects are just elements of \$$\mathcal{V}\$$

* for any \$$x,y \in \mathcal{V}\$$ we have \$$\mathcal{V}(x,y) = x \multimap y\$$.

This is the real reason for the word 'closed': \$$\mathcal{V}\$$ becomes a category _enriched over itself_, so it's completely self-contained, like a hermit who lives in a cave and never talks to anyone but himself.

Let's show that we get a \$$\mathcal{V}\$$-enriched category this way.

**Theorem.** If \$$\mathcal{V}\$$ is a closed monoidal category, then \$$\mathcal{V}\$$ becomes a \$$\mathcal{V}\$$-enriched category as above.

**Proof.** If you look back at the [definition of enriched category](https://forum.azimuthproject.org/discussion/2121/lecture-29-chapter-2-enriched-categories/p1) you'll see we need to check two things:

a) For any object \$$x\$$ of \$$\mathcal{V}\$$ we need to show

$I\leq\mathcal{V}(x,x) .$

b) For any objects \$$x,y,z\$$ of \$$\mathcal{V}\$$ we need to show

$\mathcal{V}(x,y)\otimes\mathcal{V}(y,z)\leq\mathcal{V}(x,z).$

I bet these are follow-your-nose arguments that we can do without really thinking. For a) we need to show

$I \leq x \multimap x$

but by the definition of 'closed' this is true if and only if

$x \otimes I \le x$

and this is true, since in fact \$$x \otimes I = x\$$. For b) we need to show

$(x \multimap y) \otimes (y \multimap z) \leq x \multimap z$

but by the definition of closed this is true if and only if

$x \otimes (x \multimap y) \otimes (y \multimap z) \le z.$

Oh-oh, this looks complicated! But don't worry, we just need this lemma:

**Lemma.** In a closed monoidal category we have \$$a \otimes (a \multimap b) \le b\$$.

Then we just use this lemma twice:

$x \otimes (x \multimap y) \otimes (y \multimap z) \le y \otimes (y \multimap z) \le z .$

Voilà!

How do we prove the lemma? That's easy: the definition of closed monoidal category says

$a \otimes (a \multimap b) \le b \text{ if and only if } a \multimap b \le a \multimap b$

but the right-hand statement is true, so the left-hand one is too! \$$\qquad \blacksquare \$$

Okay, let me leave you with some puzzles:

**Puzzle 193.** We know that for any set \$$X\$$ the power set \$$P(X)\$$ becomes a monoidal poset with \$$S \le T\$$ meaning \$$S \subseteq T\$$, with product \$$S \otimes T = S \cap T\$$, and with the identity element \$$I = X\$$. Is \$$P(X)\$$ closed? If so, what is \$$S \multimap T\$$?

**Puzzle 194.** From [Lecture 11](https://forum.azimuthproject.org/discussion/1991/lecture-11-chapter-1-the-poset-of-partitions/p1) we know that for any set \$$X\$$ the set of partitions of \$$X\$$, \$$\mathcal{E}(X)\$$, becomes a poset with \$$P \le Q\$$ meaning that \$$P\$$ is finer than \$$Q\$$. It's a monoidal poset with product given by the meet \$$P \wedge Q\$$. Is this monoidal poset closed? How about if we use the join \$$P \vee Q\$$?

**Puzzle 195.** Show that in any closed monoidal poset we have

$I \multimap x = x$

for every element \$$x\$$.

In terms of resources this says that \$$I\$$ acts like 'nothing', since it says

> _If you have \$$I\$$, what do you need to combine it with to get \$$x\$$? \$$\; \; x\$$!_

Of course \$$I \otimes x = x = x \otimes I \$$ also says that \$$I\$$ acts like 'nothing'.

**Puzzle 196.** Show that in any closed monoidal poset we have

$x \multimap y = \bigvee \lbrace a : \; x \otimes a \le y \rbrace .$

**[To read other lectures go here.](http://www.azimuthproject.org/azimuth/show/Applied+Category+Theory#Chapter_4)**