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 co-Galois 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 Aop, 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 type-connectives 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 right-handed (;) 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:S|F(X) £ A} is representable, ie of the form S¯ \typeX0 for some unique \typeX0 Î 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;\constfunctS = \constfunctA;UÁ implies FoÚS = ÚAo FÁ, and F;\constfunctA = \constfunctS;FÁ implies UoÙA = ÙSo UÁ.
So long as there are enough meets and joins, the converse holds.
DEFINITION 3.6.12 A poset is a complete join-semilattice if every subset has a join, and similarly a complete meet-semilattice if every subset has a meet; if both of these hold we call it a complete lattice.
Any complete join-semilattice is a complete meet-semilattice and vice versa , but we make the distinction between complete meet- and join-semilattices 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 meet-semilattice 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 function-types. 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 join-semilattice 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.