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.