I wrote:

> So, here's what we've shown:

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

> And we can copy our whole line of reasoning and show this:

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

Jonathan wrote:

> My take is that the formula tells us what values the [...] adjoint must take if it exists.

That's true, and that's what I said in my lecture: I derived each of these formulas assuming the adjoint in question exists.

But I think the situation is much better than this. I believe that if the formulas give well-defined functions, these are necessarily the desired adjoints! It would be fun to try to show this, straight from the definitions. My hunch is that it's easy.

> So, here's what we've shown:

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

> And we can copy our whole line of reasoning and show this:

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

Jonathan wrote:

> My take is that the formula tells us what values the [...] adjoint must take if it exists.

That's true, and that's what I said in my lecture: I derived each of these formulas assuming the adjoint in question exists.

But I think the situation is much better than this. I believe that if the formulas give well-defined functions, these are necessarily the desired adjoints! It would be fun to try to show this, straight from the definitions. My hunch is that it's easy.