Sophie wrote:

> Looking back, it seems like that direction of the adjoint functor theorem is conditioned on \$$\mathbb N [S]\$$ having all joins (resp. meets). But I think \$$\mathbb N [S]\$$ has neither since \$$x \leq x'\$$ means that \$$x\$$ and \$$x'\$$ must have the same number of bowls. I gave some reasons why in [#10](https://forum.azimuthproject.org/discussion/comment/18346/#Comment_18346). So this direction of the adjoint functor theorem won't apply to our specific puzzle. Is this correct?

Good point! But somewhere or other I mentioned that in this direction of the adjoint functor theorem, where we are trying to prove some monotone function \$$f : A \to B\$$ has a right adjoint, we don't really need \$$A\$$ to have _all_ joins, only those that are used in the formula for the would-be right adjoint

$g(b) = \bigvee \\{a \in A : \; f(a) \le_B b \\} .$

Similarly, we don't need \$$f\$$ to preserve _all_ joins, just those that exist in \$$A\$$. You can see this by carefully reading the proof of the adjoint functor theorem for posets.

Oh yeah - I said this in [Lecture 17](https://forum.azimuthproject.org/discussion/2037/lecture-17-chapter-1-the-grand-synthesis/p1).

(Somehow in our conversations we always wind up talking about the precise necessary and sufficient conditions for things to be true! That's probably good: it means we're getting into the details.)

So, the adjoint functor theorem can even be used in situations where not all meets (or joins) exist. However, if you're trying to prove an adjoint exists, it's almost always easier to just guess the desired adjoint and then show it works. Guessing isn't hard, since we know a formula for the adjoint if it exists!