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.
Version 2.1.8p2
