Now we shall transform universal maps from their logically quantified statement into a purely algebraic form. This involves making a Choice (Exercise 3.26) of universal and co-universal maps, which provide the components of two natural transformations. Although they are unique up to unique isomorphism, these play a crucial role , and are just as much part of the definition as are the functors U and F. In particular we shall show that the laws which they obey express the b- and h-rules in type theory (Sections 2.3 and 2.7), and (as in Definition 4.7.2(c)) the naturality condition handles substitution or continuation.
In this section we drop the Convention 4.1.2 for brackets (which arose from Currying, Convention 2.3.2): F UA means F(UA), etc .
DEFINITION 7.2.1 An adjunction F\dashv U consists of
satisfying the following triangular laws:
omitted diagram environment
cf Lemma 3.6.2 for posets. The letters L and R will be used to identify the triangles in the same way as N and Z for naturality in Definition 4.8.1.
THEOREM 7.2.2 The following are equivalent:
|
The components are derived from one another by
|
REMARK 7.2.3 Naturality of l means that the following square in Set commutes, which, for p:F X® B, says that l(Fu;p;z) = u;l(p);Uz.
omitted diagram environment
Hence if the square on the left below commutes in A then so does that on the right in S (and conversely since l is bijective).
omitted diagram environment
Put z = id and compare these diagrams with Definition 4.7.2(c).
Applications Recall from Sections 2.3 and 2.7 that the introduction, elimination, equality, b- and h-rules for the product, sum, function-type and List constructions are summed up by adjoint correspondences.
REMARK 7.2.4 Consider the common situation in which a universal property is used to define a new construction in terms of an old functor. Indeed the definition of universal maps, unlike that of adjunctions, was phrased in just this way.
EXAMPLE 7.2.5 For products, F:S® SxS is the diagonal functor and U = x. Then l is -,-, the co-unit e is the family of projections (pi) and the unit h is the diagonal map D:X® XxX. The product functor is defined on maps,
|
|
omitted diagram environment
Notice that y:1® Y is a global element: if it is only partially defined then commutativity of the square on the right becomes an inequality, so strict naturality fails in p-categories (Exercise 5.15).
EXAMPLE 7.2.6 For colimits, l-1 is case analysis [ , ], the unit h is the family of inclusions (ni) and the co-unit e is the codiagonal.
omitted diagram environment
The naturality condition on the left (the new side) defines + on maps. On the right (old) it states invariance under continuation z (Remark 2.3.13). This says that the (+E)- box is open-ended, cf Remark 1.6.5.
EXAMPLE 7.2.7 For function-types, F = (-)xY and U = ( = )Y. The adjoint transposition (l) is l-abstraction and the co-unit e is evaluation. Naturality on the left (the old side) states substitution-invariance of l (Definition 4.7.2(c)), and on the right (new) is postcomposition. The naturality of e is (-)X on morphisms; and that of h:x® ly.x,y is substitution under l.
The left triangle law is the essence of the b-rule, but in the special case p = x,y, (ly¢.x,y¢)y = x,y. To see it at work we must pre- and postcompose with the argument and the function, and use naturality, cf Remark 2.3.9.
omitted diagram environment
The right triangle law is the h-rule in a more direct way.
omitted diagram environment
EXAMPLE 7.2.8 List:Set® Mon is left adjoint to the forgetful functor. The unit is the singleton list, and the co-unit List(A)® A multiplies out a list of elements of the monoid A. The adjoint transposition l-1 is (roughly) what we called fold in Proposition 2.7.5 and [[-]] in Section 4.6 and elsewhere. Naturality on the left (the new side) for u:X® Y is the action mapu of the functor (Example 2.7.6(d)). On the right it is the action of a monoid homomorphism z (Remark 2.7.12).
Example 7.4.6 shows how eA:List(A)® A captures the structure of the algebra A.
REMARK 7.2.9 This account is connected with the binary rules for List ( append and fold) in Definition 2.7.4ff, whereas recursion in Section 6.1 was based on the unary form ( cons and listrec). The unary and binary theories employ universal properties in different ways, which are related to the different roles of the alphabet X.
Proof of the equivalence It is surprising how little structure need exist in advance: we need naturality of l on one side, for which we must know what the morphisms are. The rest of the structure is derivable: the naturality and triangle laws are the essential part.
PROOF OF THEOREM 7.2.2: We must show that the eight expressions are functorial, natural, mutually inverse or universal as appropriate.
The proofs of [bÞ d] and [dÞ a] are dual, ie they are obtained from [bÞ cÞ a] by interchanging the parameters and reversing the arrows. []
Reflections and representables The equivalence amongst these four presentations explains how various other terminologies arise. Recall from Theorem 4.8.12(b) that the Yoneda embedding identifies X Î obS with \HX = S(-,X) in SetSop, cf S¯ x in Definition 3.1.7.
PROOF: The first part is immediate and the other two are similar to Lemma 7.1.5. Recall the characterisations of
By the R law hUA is invertible iff UeA is; indeed the latter being mono suffices. This holds if e is mono because U, being a right adjoint, preserves limits (Theorem 7.3.5) and hence monos (Proposition 5.2.2(d)). Conversely if U is the inclusion of a reflective subcategory then it is full and faithful, so e is invertible. []
The natural bijection is a simple and symmetrical way of presenting an adjunction and remembering (in a subject with plenty of traps for the dyslexic) which is left and which is right. Although an ``intuitively'' natural construction usually turns out to be natural in the formal sense, Theorem 7.6.9 shows that naturality may be the point at issue. We saw in Remark 7.2.3 how checking it can be built into the idiom.
The formulation using representables shows how to generalise the notion of universal property, for example to that of Cn[]L.
REMARK 7.2.11 Let A and C be 2-categories. The isomorphism A(F(-),( = )) º C(-,U( = )) may be replaced by either a strong or a weak equivalence of hom-categories (Definition 4.8.9). The various forms are illustrated by C/at: this has limits, exponentials and coproducts in the `` isomorphism'' sense ( cf Exercise 4.49), but other colimits can only be defined by an adjoint correspondence which is an equivalence functor. These different situations are distinguished by referring to 2-limits, but bi-colimits. Definition 7.3.8 also gives a new kind of 2-limit. An even more general situation is where A and C are enriched, ie A(A,B) and C(X,Y) belong to some other category |[thick] such as AbGp [Kel82].
Adjunctions are more common than the newcomer to category theory might expect, and individual cases are correspondingly less remarkable. Not unusually they are produced like a rabbit out of a hat, following an argument in which the more canny reader has watched the conjurer stuffing them in, as free algebras. The point is that, if the categories (S and A) and the functors (F and U) are artificial (A = SxS for the product, to give a mild example), then the significance of the adjunction F\dashv U is not particularly cogent. The universal property in the style of Definition 7.1.1 expresses the important facts more directly. It also avoids the question of Choice, which is, frankly, a red herring: this is a side-effect of imposing one-dimensional algebraic notation on a logical situation which is naturally a little subtler.