Keith asked:

> So then, why is John using infs and sups when defining the unique formulas in lecture 6?

Matthew replied:

> For complete lattices such as power set algebras and \$$\mathbb{R}\$$, those characterize adjoints.

No, that wasn't my reasoning. Right or wrong, my position in [Lecture 6](https://forum.azimuthproject.org/discussion/1901/lecture-6-chapter-1-computing-adjoints#latest) was this: I wasn't _assuming_ the posets in question have _all_ infs and sup, I was _claiming_ that they _must_ have the infs and sups _in question_, given my assumptions.

In more detail, suppose \$$A\$$ and \$$B\$$ are arbitrary preorders. If \$$f : A \to B\$$ has a right adjoint \$$g : B \to A\$$ and \$$A\$$ is a poset, this right adjoint is unique and we have a formula for it:

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

Here's the proof, [as fleshed out by Alex Chen](https://forum.azimuthproject.org/discussion/comment/16556/#Comment_16556).

1) Since

$$f(a) \le_B b \textrm{ if and only if } a \le_A g(b)$$

we know \$$g(b)\$$ is an upper bound of the set \$$\\{a \in A : \; f(a) \le_B b \\} \$$. So, we just need to show it's _the least_ upper bound.

2) However, \$$g(b)\$$ is in the set \$$\\{a \in A : \; f(a) \le_B b \\} \$$, i.e. \$$f(g(b)) \le_B b\$$. Why? Because

$$f(g(b)) \le_B b \textrm{ if and only if } g(b) \le_A g(b) .$$

So, any lower bound of this set must be \$$\ge g(b)\$$. Thus, \$$g(b)\$$ is _a_ least upper bound.

3) So far we haven't used the assumption that \$$A\$$ is a poset. We need this only to conclude that \$$g(b)\$$ is _the unique_ least upper bound. In a poset, if a set has two least upper bounds \$$x\$$ and \$$x'\$$, we must have \$$x \le x'\$$ and \$$x' \le x\$$, so \$$x = x'\$$. So, in a poset, upper bounds are unique.

Similarly, if \$$g : B \to A\$$ has a left adjoint \$$f : A \to B\$$ and \$$B\$$ is a poset, this left adjoint is unique and we have a formula for it:

$$f(a) = \bigwedge \\{b \in B : \; a \le_A g(b) \\} .$$

To repeat: I'm not assuming or claiming the existence of any sups or infs other than those I'm actually using here. I'm saying that these particular sups and infs _must exist_ given the assumptions.