At first sight, the definition of a category is not sufficiently general to interpret l-abstraction or many-argument operations: it seems that it is only suitable for unary ones. In Section 4.3 we effectively extended the definition of category by admitting a list of objects as the source of each morphism; such structures, called multi -categories, were formalised by Joachim Lambek [ Lam89]. But this is the thin end of a wedge: for every new constructor we would need to modify the definition of a category again to make the semantics follow slavishly after the syntax. For example allowing function-types in the source too would be useful to simplify the definition of sums and lists (Remarks 2.3.11 and 2.7.10).
Our strategy will be to keep faith with categories as they are, uncovering their latent structure - what is there already. We shall show that this matches the type-theoretic phenomena of interest. Even graph theory does this in a primitive fashion, by studying features such as bridges, ie edges whose removal would disconnect the graph. Particular nodes and edges may be characterised à la Leibniz (Proposition 2.8.7) by such features - by the way in which the others see them.
But a graph may have many (different) bridges: we need descriptions (Definition 1.2.10) - properties for which the definite article ( the) can be used. We use superlatives such as greatest. These must be justified by comparatives ( greater) with all other objects. Indeed French and Italian ( il più bel prodotto) use the definite article to make superlatives out of comparatives. In a category the comparatives are the morphisms.
The Leibnizian method of description is based on quantification over the whole category, and we shall use either G or Q for the bound variable. This quantification means that universal properties are impredicative definitions; they are (loosely) related to those in Remark 2.8.11.
Variation over the ambient category may instead be expressed as an axiom scheme with an instance for each comparative object (G or Q). The maps a:G® X used to test a universal property may be seen as terms or elements of (type) X, so quantifying over the objects G in the category says ``for all terms a:X'' without specifying the parameters G occurring in them. But the definitions must be preserved by substitution for these parameters, cf Lemma 1.6.3.
The terminal object We shall begin by looking closely at the very simplest case. Category theory attracts from mathematicians derisive names such as ``abstract nonsense'' and ``empty-set theory'' because of definitions like this one and the remarks which follow it. Informaticians will be better aware of the need to get base cases right: although they appear trivial, they are where the actual work of a construction gets done, and are also where most program bugs lie. In category theory, any universal construction is the terminal object of some category.
DEFINITION 4.5.1 1 Î obC is a terminator, terminal object or final object if for each object G Î obC there is a unique morphism \terminalprojG :G® 1.
REMARK 4.5.3 In Set, for each element a Î X there is a function {*} ® X selecting a (Lemma 2.1.9(d)), so maps from the terminal object are called global elements. Although this usage came from topology via sheaf theory (Example 8.3.7(a)) its meaning is exactly what might be expected from programming: a term in the global (empty) context. By Corollary 4.3.13, a general map a:G® X is a term G\vdash a:X in the arbitrary or local context of the parameters G, so it is called a generalised or local element.
The distinction is well known and important in recursion theory: we say that two functions f,g:N® N are numeralwise equal if f(0) = g(0), f(1) = g(1), f(2) = g(2), ..., ie the two composites
omitted diagram environment
agree ( cf a predicate f[n] provable for each n separately), but this is not enough to prove f = g or "x.f[x] (Remark 2.4.9, Theorem 9.6.2).
Proposition 4.2.9 showed that every category has a faithful covariant action HX on its generalised elements (see also Theorem 4.8.12).
DEFINITION 4.5.4 If G Ì obC is such that the restriction of the action to (\GX = ÈG Î GC(G,X):X Î obC) remains faithful then it is a class of generators. Classically this is often stated as follows: if f ¹ g:X\rightrightarrows Y in C then there are some G Î G and a:G® X with fo a ¹ go a. To say that there is some set G of generators is a widely applicable way of restricting the size of a category ( cf locally small, Remark 4.1.10).
Some writers have specialised the term concrete category to this case, where the action on global elements is faithful. The standard usage of this term is that there is some faithful action. For example CSLat is manifestly described ``concretely,'' but CSLat(1,X) always has exactly one element, so {1} cannot generate. There are other categories which we would like to call concrete but in which there are few maps 1® X, or which don't have a terminal object at all. What ``concrete'' really means is that ``the action you first thought of'' is faithful, so neither definition is particularly satisfactory. However, there is no real need for any of this terminology. See also Exercise 4.12.
Unique up to unique isomorphism The account of the theory of descriptions which we gave in Section 1.2 was more liberal than Russell's, allowing interchangeable objects to share the description. This is the nature of universal properties.
THEOREM 4.5.6 The terminal object, if it exists, is unique up to unique isomorphism. Conversely, any object which is isomorphic to a terminal object is itself terminal.
PROOF: Let \typeT1 and \typeT2 be terminal objects. Then putting \typeT1 for 1 and \typeT2 for G, there is a unique map u:\typeT2® \typeT1, and with the opposite assignment a unique map |:\typeT1® \typeT2.
To show that these are mutually inverse, consider \id\typeT1 and |;u. These are both maps \typeT1® \typeT1, but casting \typeT1 in both roles (as 1 and as G), there is only one such map and so the two candidates for it must be the same, cf Lemma 1.2.11. So |;u = \id\typeT1 and similarly u;| = \id\typeT2.
omitted diagram environment
Finally, let \typeT1 be terminal and suppose u and | form an isomorphism with \typeT2. Then for any object G, the unique map G® \typeT1 extends by | to \typeT2, but if a,b:G\rightrightarrows \typeT2 then a;u = b;u since \typeT1 is terminal, and then
a = a;u;| = b;u;| = b since
u;| = \id\typeT2. []
Notice how the uniqueness of maps to 1 enabled us to deduce the equality of id and u;| and hence transfer known properties from one to the other. Mere existence of morphisms between objects is nothing like as useful.
Products The cartesian product can also be described in this way. It is what we use in type theory to describe functions of two variables.
DEFINITION 4.5.7 Let P, X and Y be objects of a category C. Then (p0:P® X,p1:P® Y) is a product if for every object G Î C and pair of morphisms (a:G® X,b:G® Y) in C there is a unique mediating map f:G® P such that p0o f = a and p1o f = b. The product is written Xx Y, and the mediator f, which is called the pair , is written a,b.
omitted diagram environment
Like the terminal object, the product together with the projections, p0 and p1, is unique up to unique isomorphism. Conversely, any isomorphic object u:Q º Xx Y may be given the structure of the product, with projections u;p0 and u;p1 and pairs u-1;a,b.
The p notation signifies selection ( 4.5.8(f)), but we often want to specify the omission of a component (4.5.8(i)); for this we use the hat notation ([^(x)]) and the triangle arrowheads. Beware that the latter indicate a type-theoretic interpretation and not an intrinsic property such as surjectivity.
G = [[(z)\vec]: [(Z)\vec]].
|
See also Exercises 4.17, 4.21, 4.22, 5.22 and 5.30.
REMARK 4.5.9 The product X×C Y in an abstract category and the cartesian product of hom-sets in Set are related by the equation
|
|
Preservation and creation of products There is no need to make a choice of products to define what it means for a functor to preserve them: if one product P is preserved then so is any other Q º P.
DEFINITION 4.5.10 Let X,Y Î obC. A functor U:C® D
So if U is a forgetful functor there is a unique structure that can be put on the product of the underlying sets and is consistent with the structure of the given objects.
EXAMPLES 4.5.11 Recall Examples 4.4.9(f) and (g).
Using the existence of products To say that a category C ``has products'' is a statement of the form
|
REMARK 4.5.12 In particular, whenever we have two particular objects A and B, we may (instantiate the universal quantifiers and) suppose that some product cone A¬ P® B is at our disposal. The way that we do this is just the same as the idiom for ($E ) in any other circumstances (Remark 1.6.5): it is a formal property of the existential quantifier that we may invent a name for such a cone and continue to use it for as long as the given A and B remain in scope. Nothing in this procedure assumes a global assignment of products to all pairs of objects in the category.
Suppose, on the other hand, that an object P has already been introduced by some other means, and that we can show that it possesses the universal property needed to be a product. Suppose also that no other name has so far been given to any product of X and Y. Then, since being a product is a description up to isomorphism (Lemma 1.2.11, Theorem 4.5.6), we may write P = XxY, electing P as the specified product, instead of P º XxY.
Usually in category theory, as throughout mathematics in action, the quantifiers do their entrances and exits unannounced. The process of inventing names for witnesses for existential statements may be repeated any finite number of times (and that number may be unspecified: we may use products of pairs of objects from a list of indeterminate length, Exercise 2.43). In a sense it may even be done infinitely: if, by methods such as in Chapter VIII, we have some way of collecting an ``indexed family'' as one object then the uniqueness feature of universal properties means that one application of a product construction suffices to provide it uniformly for all members of the family.
The point at which such methods break down is where we want to make some construction (usually a functor) globally throughout the category. There are three ways to proceed. Classically, the axiom of choice selects products once and for all. Logically, such constructions may be regarded as schemes : to be instantiated to each situation as required. The third way is to replace the category itself with an equivalent (interchangeable) one on which products are indeed defined globally. We shall show how to do this in Section 7.6, without using the axiom of choice.
Universal properties give functors We see why it is important for mediators to be unique when we extend universal constructions to maps.
PROPOSITION 4.5.13 Let U be an object of a category C for which all products Xx U for X Î obC exist and are specified. Then there is a unique functor C® C whose effect on objects is X® Xx U and such that (fx U);p0 = p0;f and (fx U);p1 = p1. It is called (-)x U.
omitted diagram environment
PROOF: The equations amount to one side of the commutative diagram. Clearly the universal property of products provides a unique fill-in, but it still remains for us to check that this is a functor. In the case f = \idX, the identity \idXx U is such a fill-in, and so by uniqueness this must be it: (\idXx U) = \idXx U. Similarly, ignoring Yx U, there is a unique fill-in (f;g)x U:Xx U® Zx U, but (fx U);(gx U) also makes the diagram commute, and so by uniqueness they are equal. []
There is similarly a functor x:CxC® C of two arguments which yields the product of an arbitrary pair of objects or morphisms.
The terminal object and binary product are the nullary and binary cases of an n-ary connective on objects, but as usual they suffice.
PROPOSITION 4.5.14 If a category has a terminal object and a product for every pair of objects then it has a product for every finite list of objects. []
REMARK 4.5.15 The cartesian products Xx(Yx Z) and (Xx Y)x Z of sets are not equal: their typical elements are x,y,z and x,y,z respectively. Although what these products are is different, what they do is the same: they both satisfy the universal property of a product of three objects, and so they must be uniquely isomorphic. That is why definition up to isomorphism is the (accepted) norm, and definition up to equality is meaningless.
Set has a canonical way of assigning binary products, but we have just seen that this is not associative. By convention, we shall take the left-associated product (···(((1x \typeX1)x\typeX2)x\typeX3)x···x\typeXn-1)x\typeXn, but notice that this depends on a notion of atomic type. We use it in Remark 4.6.5 to define [[G,x:X]] = [[G]] x X inductively and hence to interpret expressions in algebras and programming languages.
All universal properties are terminal objects
LEMMA 4.5.16 Let X,Y Î obC. Then there is a category, which we call C¯ X,Y, whose objects are spans, ie pairs of C-maps X a¬ U b® Y, and whose morphisms from this are C-maps f:U® U¢ making the two triangles below commute.
omitted diagram environment
The terminal object (if it exists) of this category is the product cone for X and Y in C.
PROOF: As with the ``concrete'' categories of Proposition 4.1.4, to show that C¯ X,Y is a category we just have to verify that (the identity \idU is a morphism and) composition preserves the defining property. This is easy, but note that it uses the associativity law in C:
|
Mainstream mathematicians tend to view this as a rather abstruse way of saying something quite simple, but the method is like programming with abstract data types. The complexity of the constructions (in this case the commutativity of the triangles in the above diagram) is hidden from the user and later applications work in an apparently effortless way, but at a certain price. The components (modules) must be fully equipped with their ancillary operations and specifications: in this case the product projections and the associativity law of the given category, which are needed to make the definitions of respectively the objects and maps meaningful. What seems to be secondary, even optional, structure in the data turns out to be primary and necessary structure in the derived constructions; conversely ``trivial'' features of the derived construction unravel into something non-trivial in the given presentation.
In order to see this ancillary structure in action, you should demonstrate in detail that the product of two objects (if it exists) in a category is unique up to unique isomorphism, both directly in terms of the definition and indirectly via the category C¯ X,Y.
The type disciplines of category theory and the abstract data type idiom in programming often ensure that the ancillary structure is complete in the following sense: When the Real Mathematician - and this applies equally to the Real Programmer - is up to his elbows in the grime of a difficult procedure, he frequently needs to prove (or to leave to the reader) lemmas and sub-lemmas (respectively to program sub-routines or perform in-line hacks) which import the notation of the immediate application but in fact only reproduce in a multitude of special cases that ancillary structure which he had disregarded as trivial. By contrast, the categorist begins by applying the parsimonious categorical tools which she has learned to trust. She then approaches applications with the calm self-confidence of one who knows that she is prepared for the occasion.
We shall collect more examples of universal properties in Chapter VII.