# Practical Foundations of Mathematics

### Paul Taylor

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

(a)

 "X,A.    omitted prooftree environment
we also say that F is the lower or left adjoint of U, and U is the upper or right adjoint of F (also, ``F is left adjoint to U'' etc );

(b)
a Galois connection if "X,AA £ AF (X)Û X £ SU(A);

(c)
a co-Galois connection if "X,AF(X) £ AA Û U(A) £ S X.

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

(a)
F and U being monotone with \idS £ Uo F and Fo U £ \idA;

(b)
F and U being antitone with \idS £ Uo F and \idA £ F o U;

(c)
F and U being antitone with Uo F £ \idS and Fo U £ \idA;

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. []

REMARK 3.6.7

(a)
Any isomorphism between preorders is an adjunction, in two ways, with £ replaced by equality. Likewise any duality (isomorphism S º Aop) is both a Galois connection and a co-Galois connection.

(b)
Replacing £ in Definition 3.6.1 by the equivalence relation ~ (the conjunction of £ and ³ , Proposition 3.1.10), we obtain the notion of a strong equivalence of preorders: \idS ~ UoF and FoU ~ \idA.

(c)
A full monotone function F:S® A for which
 "A:A.\$X:S.F(X) ~ A
is called an equivalence function; for example Proposition 3.1.10 showed that any preorder is equivalent to a poset. Using the axiom of choice, every equivalence function is part of a strong equivalence (see Exercise 3.26 for why Choice is necessary).

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:

(d)
Two preorders S and \cat T are said to be weakly equivalent if a third preorder A and equivalence functions S® A¬ \cat T are given.

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

(a)
F(C) is an upper bound of \leftadj!(Á) by monotonicity.

(b)
Since "X.F(X) £ q, we have "X.X £ U(q) by adjointness, so U(q) is an upper bound of Á.

(c)
If C is a least upper bound of Á then C £ U(q), so F(C) £ q.

(d)
If C is locally least and F(C) £ A ³ q then C £ U(A ) ³ U(q), so C £ U(q) and F(C) £ q.

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

 U(A) = \typeX0 = Ú {X|F(X) £ A}.
Similarly F(X) = Ù{A:S|X £ U(A)}. []

EXAMPLES 3.6.10 Meets and joins are themselves adjoints.

(a)
The unique function F:S® {*} has a right adjoint iff S has a greatest element. The right adjoint U is *® T, and T is the join of the whole poset (considered as a diagram id:S® S).

(b)
The diagonal function F:S® SxS has a right adjoint iff S has meets of pairs, and then the right adjoint is U(X,Y) = XÙY.

(c)
More generally, let Á be any diagram shape, and put A = SÁ and \constfunct (X) = li.X Î A. Then g Î S is a lower bound for a diagram d:Á® S iff \constfunct (g) £ Ad. The right adjoint, \constfunct \dashv U, provides the meet, U(d) = Ù\fund!(Á); it is given by Ú{g: S|\constfunct (g) £ Ad}. (Notice that this repeats the same calculation at each co-ordinate i Î Á.)

Similar results hold for ^ and joins, which are given by left adjoints to the diagonal or constant functions. In particular,

(d)
the regular representation X¯ (-):A ® shv(A) (Definition  3.1.7), which preserves meets by Proposition  3.2.7(a), has a left adjoint iff A has all joins, and then the left adjoint is Ú.

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:

(a)
The inverse image operation F = g* on open sets for a continuous function g between topological spaces preserves finite intersections.

(b)
In domain theory, if \idS = UoF and FoU £ \idA with U Scott-continuous ( ie preserving directed joins) then F:S\hookrightarrow A is called an embedding and U:A\twoheadrightarrow S a projection. Scott-continuous adjunctions with \idS £ UoF also arise in this subject.

Frames and Heyting algebras   Let us consider when F:W® W by a® aÙf has a right adjoint.

PROPOSITION 3.6.14

(a)
Let U:b® (fÞ b), so F\dashv U; then these operations preserve joins and meets respectively,

(^Ùf)   =   ^       (fÞ T)    =   T fÞ (aÙb ) (fÞ a)Ù(f Þ b),

but the most important case is the distributive law,

 (aÚb)Ùf (aÙ f)Ú(bÙf).

(b)
Conversely, by the adjoint function theorem, in a complete lattice, F has a right adjoint iff binary meet distributes over arbitrary joins,

 fÙ Ú i ai = Ú i (fÙai)        (fÞ b) = Ú {a|f Ùa £ b},
cf the Frobenius law, fÙ \$x.a[x] = \$x.fÙa[x] (Lemma  1.6.3). []

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

 omitted prooftree environment
cf the introduction and elimination rules for implication (Remark 1.4.3 and Definition  1.5.1). Exercise 3.28 gives a purely equational version. Heyting semilattice homomorphism s by definition preserve Þ , whereas semilattice homomorphisms need not.

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.