The definition of adjoint functors in terms of universal morphisms lends itself to very economical proofs in situations where one has a functor but no "direct" candidate for the left adjoint functor (only something looking like a unit and/or a suggestion for maps $\overline f$ as above)

I am now in a situation where I have something I suspect will be a left adjoint functor and something I suspect will be the unit of an adjunction. And I am now wondering if there is a similar characterisation of adjoint functors applicable in the case.

I realise that since adjoints are unique just the functor uniquely determines the, possible, adjunction. I guess I am looking for a way to check whether what I suspect is a unit can be part of an adjunction, and if that is the case, what minimal additional structure I need to define the other components of the adjunction.

Concretely, in this case, the problem is related to pointfree topology. I'm working on proving the existence of a right adjoint to the functor $\Omega \; \colon \mathbf{Top} \to \mathbf{Loc}$ (sending a space to its open set lattice and a continuous function to the corresponding frame homomorphism). I know this will turn out to be a topology on the set of points $\operatorname{Pt} X$ of the locale.

What I'm trying to do is prove this by defining the quotient map $X \to \operatorname{Pt} (\Omega \, X)$ where $\operatorname{Pt} (\Omega X)$ is given the quotient topology induced by the equivalence relation defined by two points being equivalent if they correspond to the same point of the spaces locale (I think this is called the soberisation of the space). Formally this is done by associating to each element $x \in X$ the map $p_x \; \colon 1 \to X$ such that $p_x(\cdot) = x$ where $1$ is some fixed one element topology. Two points $x$ and $y$ then correspond to the same point if $\Omega \, p_x = \Omega \, p_y$.

I thus have the left adjoint $\Omega$ and something looking like a unit (the quotient map), and I'm wondering if I can get away without "explicitly" defining how $\operatorname{Pt}$ acts on morphisms, instead defining some other structure. For example, but not necesserily, something like the universal morphisms in the one definition of adjunction.

I know there are other (more or less intuitive) ways to prove this by making $\operatorname{Pt}$ a functor explicitly, I just found the quotient topology construction above very natural, and I wondered if one could make a nicer proof by applying it.

-
I did a major rewrite of the question, I hope it is more clear now. –  Tilo Wiklund Jul 23 '11 at 1:47
Have you looked at Freyd's adjoint functor theorem? Mac Lane [CWM, 1998, p. 125] gives the example of constructing the Stone–Čech compactification using it. –  Zhen Lin Jul 25 '11 at 1:35
@Zhen: I don't see how the adjoint functor theorem should help here. We know that there is a right adjoint to $\Omega$ and that it is given on objects by $\operatorname{Pt}$ as tilo describes it above. We also know that the unit of the adjunction is given by the construction described here. The question is: Can we use this construction in proving that $\operatorname{Pt}$ is the right adjoint? The obvious way to proceed is to write down the counit and check universality at the other end of the adjunction (that's straightforward). But that's not what's asked here (as far as I can tell). –  t.b. Jul 25 '11 at 4:21
Quite right, the main issue is that I would like to avoid having to make $\operatorname{Pt}$ (explicitly) a functor, letting its action on morphisms be decieded by $\Omega$ and this unit. I wouldn't mind having to construct some additional structure, as long as doing so is less work (or, at least, a more natural feeling construct) than making $\operatorname {Pt}$ a functor. –  Tilo Wiklund Jul 26 '11 at 0:16