Adjunctions unify the treatment of the logical connectives. Generalised from propositions to types, they not only handle the operations x, ® , +, etc but also account for the ``universal properties'' that we have been meeting, such as Propositions 3.1.10, 3.2.7(b) and 3.4.12. Adjunctions themselves also arise as a common method of construction involving powersets. In view of this and the shift in the next chapter to categories, we now call the posets S and A, and their elements X Î S and A Î A.
DEFINITION 3.6.1 Let F:S® A and U:A® S be functions (not a priori monotone) between preorders. We say that F and U are

Galois and coGalois connections are also known as contravariant or symmetric adjunctions, on the right and left respectively. They are the same as covariant adjunctions ( ie the first kind) between S and A^{op}, but Section 3.8 shows how (a) and (b) arise between full powerset lattices in two idiomatic but different ways. Exercise 4.27 uses all three as interesting typeconnectives between complete semilattices.
LEMMA 3.6.2 The above definitions are respectively equivalent to
where £ is the pointwise order (Proposition 3.5.5). Moreover if S and A are posets, then in all three cases F = Fo Uo F and U = Uo Fo U.
PROOF: Suppose F\dashv U. Let X £ Y and put A = F(Y); then F(Y) £ A so X £ Y £ U(A), whence F(X) £ A. Next, F(X) £ F(X) so X £ U(F(X)). Monotonicity of U and the other inequality are the same. Conversely if F(X) £ A then X £ U(F(X)) £ U(A), and similarly F(X) £ F(U(A)) £ A. Finally F(X) £ F(U(F(X))) since X £ U(F(X)), and F(U(F(X))) £ F(X) since F(U(A)) £ A so F = Fo Uo F by antisymmetry. The results for Galois connections are obtained by reversing some of the inequalities. []
REMARK 3.6.3 A third way of expressing adjunctions, that
F(X) is the least A such that X £ U(A),
is the one which we shall prefer for categories:
omitted diagram environment
we call this the universal property of F(X).
Order, composition and equivalence
LEMMA 3.6.4 Let F\dashv U and G\dashv V. Then F £ G iff U ³ V. []
COROLLARY 3.6.5 If S is a poset and F:S® A has a right adjoint U then it is unique. Similarly for left adjoints. []
LEMMA 3.6.6 If F\dashv U and G\dashv V then F;G\dashv UoV.
omitted diagram environment
This is one of the circumstances in which it is convenient to use both the left handed (o) and righthanded (;) notations together. []

The last does not, as it stands, give an equivalence relation on the class of preorders: it is reflexive and transitive but not symmetric. But as it is also confluent (Exercise 3.27) it is easy to find the equivalence closure:
Although Proposition 3.1.10 makes these notions somewhat redundant for preorders, we shall need them for categories (Definition 4.8.9).
The adjoint function theorem Theorem 3.6.9 is the most important result about infinitary meets and joins. However, it is rarely stated: since the formula for the adjoint is notationally simple, it is used, embedded in more complicated calculations, without appreciating the significance of the theorem.
PROPOSITION 3.6.8 Let F\dashv U. Then
F preserves any (locally) least upper bounds which exist, and U preserves and greatest lower bounds which exist.
Functions which are symmetrically adjoint on the left preserve least upper bounds and functions which are symmetrically adjoint on the right preserve greatest lower bounds.
PROOF: Let C be an upper bound of Á Ì S and q likewise of the image, \leftadj_{!}(Á) = {F(X)X Î Á}. Then
The other cases are the same, switching arguments and inequalities. []
The adjoint function theorem can be proved in a similar way for meets and joins of diagrams (Definition 3.2.9) rather than subsets. Exercises 3.33ff generalise to minimal and locally least upper bounds.
THEOREM 3.6.9 Let S be a poset with all joins, A a preorder and F:S® A a function. Then F has a right adjoint U:A® S iff it preserves all joins. Similarly a function from a poset with all meets has a left adjoint iff it preserves all meets.
PROOF: As S has arbitrary joins and F preserves them, the lower subset {X:SF(X) £ A} is representable, ie of the form S¯ \typeX_{0} for some unique \typeX_{0} Î S (Definition 3.1.7). Indeed

EXAMPLES 3.6.10 Meets and joins are themselves adjoints.
Similar results hold for ^ and joins, which are given by left adjoints to the diagonal or constant functions. In particular,
REMARK 3.6.11 These observations, that Ú\dashv \constfunct \dashv Ù and meets or joins commute with adjoints, are summed up by the diagram
omitted diagram environment
where \constfunct :X® li.X:S® S^{Á} . Using the composition (Lemma 3.6.6) and uniqueness (Corollary 3.6.5) of adjoints, U;\constfunct_{S} = \constfunct_{A};U^{Á} implies FoÚ_{S} = Ú_{A}o F^{Á}, and F;\constfunct_{A} = \constfunct_{S};F^{Á} implies UoÙ_{A} = Ù_{S}o U^{Á}.
So long as there are enough meets and joins, the converse holds.
DEFINITION 3.6.12 A poset is a complete joinsemilattice if every subset has a join, and similarly a complete meetsemilattice if every subset has a meet; if both of these hold we call it a complete lattice.
Any complete joinsemilattice is a complete meetsemilattice and vice versa , but we make the distinction between complete meet and joinsemilattices and complete lattices because, although the existence of one structure forces that of the other, a monotone function preserving all meets need not preserve all joins, cf Remark 3.4.5.
By Corollary 3.6.5, a function can have at most one adjoint on each side, but it can have both of them, and there are strings of any finite length of successively adjoint monotone functions. Remark 3.8.9 characterises complete sublattices of powersets, ie inclusions with both adjoints.
EXAMPLES 3.6.13 Certain weaker conditions are of interest:
(^Ùf) = ^ (fÞ T) = T fÞ (aÙb ) (fÞ a)Ù(f Þ b),
but the most important case is the distributive law,


DEFINITION 3.6.15 A Heyting semilattice (X,T,Ù,Þ ) is a meetsemilattice with an additional binary operation Þ satisfying

A Heyting lattice also has ^ and Ú, and these are to be preserved by Heyting lattice homomorphisms. A Boolean algebra is a Heyting lattice in which x = \lnot \lnot x, where \lnot x is xÞ ^, for which the truth table (Remark 1.8.4) gives a normal form. In the language of Heyting semilattices, by contrast, expressions may require nested implications , cf Convention 2.3.2 for bracketing functiontypes. Powersets in classical and intuitionistic logic provide examples of complete Boolean and Heyting lattices respectively. See [ Joh82, p. 35] for a picture of the free Heyting lattice on one generator.
We may instead concentrate on the infinitary joins.
DEFINITION 3.6.16 A complete joinsemilattice in which Ù distributes over joins is called a frame. The open sets of any topological space form a frame, and the inverse image operation of any continuous function preserves finite meets and arbitrary joins. Implication and infinite meets exist, but need not be preserved by frame homomorphisms: once again, the name of the objects changes when the morphisms change. Frames will be discussed in Theorem 3.9.9ff.