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 .\]


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)**