DEFINITION 4.4.1 A functor F:C® D between categories is
which preserves the structure (identity and composition), ie
\funcFX,X(id\CX) = id\D\funcF o(X) \funcFX,Z(f;C g) = \funcFX,Y(f);D \funcFY,Z(g).
A functor F:C® Dop or F:Cop® D may be called a contravariant functor from C to D, the usual case being styled covariant if emphasis is needed. To avoid the confusion caused by discussing morphisms of an opposite category explicitly when describing contravariant functors, it is usual simply to define \funcFX,Y:C(X,Y)® D(\funcFoY,\funcFoX).
Since the essence of a functor is that it is defined in a ``coherent'' fashion for all objects and morphisms together, the subscripts and superscripts are omitted: we write F X and F f for the application of the functor to an object or morphism. If it is defined on objects by built-in notation such as C(X,-) or Y(-) this can look a bit strange when applied to maps.
Of course given another functor G:D® E we can apply this too, writing the result as G(F X) or G(F f), with the brackets. The abstract theory of functors is a good example of a unary language (Definition 4.2.5), and would be clearer in the left-to-right notation without operators or brackets. For the sake of conformity with other notations and concepts, we shall, however, always write composition of functors from right to left as G·F, and not using juxtaposition.
EXAMPLES 4.4.2 Following 4.1.5 and 4.1.6 , a functor
EXAMPLES 4.4.3 The following are often known as forgetful functors or underlying set functors. This terminology should only ever be used when the meaning, ie just what is being forgotten, is completely clear from the presentation of the category. Notice that we may forget (a) properties of objects, (b) properties of morphisms or (c) structure on an object together with the property of morphisms that they preserve the structure. The last is the commonest situation. In all cases composition is preserved because it is defined in the same way on both sides.
Heyt® Lat® SLat® Pos® Set , Dcpo® Pos, Mon ® Set and Rng® AbGp which forget operations and their preservation.
Besides forgetting things, functors also arise from constructions, where now one may need to check preservation of (identities and) composites.
EXAMPLES 4.4.4 The following are functors:
PROOF:
The other examples rely on composition of adjunctions (Lemma 3.6.6) and of continuous functions. []
A classifying category We saw that a category is what is required to express a unary algebraic theory. An interpretation of such a theory is similarly given by a functor. Any category may play the role of Set: we restrict to the special case simply because we did in Section 4.2.
THEOREM 4.4.5 Let L be a unary language and \CloneL the category it presents by Theorem 4.2.12. Then interpretations of L correspond to functors \CloneL® Set.
omitted diagram environment
PROOF: Let the interpretation be \typeAX on sorts and \typeAr:\typeAX® \typeAY on operations. These are already part of the required data for a functor \typeA(-):\CloneL® Set, but it remains to define its effect on strings. This is uniquely determined by preservation of (the identity and) composition. Using list recursion, the identity is the base case and composition ( cons) the recursion step. Proposition 2.7.5, which showed that append is associative, guarantees that this too is preserved.
Where a law is given to hold in the interpretation of L, this means exactly that the functor takes equal values on the corresponding strings of operation-symbols. Conversely any functor \CloneL® Set restricts to the sorts and generating arrows in a way which satisfies the laws. []
How interpretations and functors correspond is what matters here, not just the fact that they do. (Category theory is in a real sense constructive logic, since the proofs are usually needed to give an accurate statement of the theorems.) Theorem 4.6.7 extends the result to Cn×L and, since it discusses algebra, has a more type-theoretic flavour; later we shall do the same for larger fragments of logic. Example 4.8.2(d) shows how the correspondence deals with homomorphisms.
The propositional analogue at the unary level is simply that a function f:(S, < )® (Q, £ Q ) obeys x < yÞ f(x) £ Q f(y) iff the same function p:\CloneL = (S, £ )®Q is monotone when the source is considered to carry the reflexive- transitive closure (Section 3.8). A model of a unary Horn theory is a < -upper subset. Similarly any function f:S®Q from a set to a monoid extends uniquely to a monoid homomorphism \CloneL = List(S)® Q (Section 2.7).
Theorem 4.2.12 generated a category freely from a sketch in the sense (of universal algebra) that it satisfies only those laws which are forced. By Theorem 4.4.5, it is the free category in the categorical sense of satisfying a universal property (next section). Classifying categories for algebra and the l- calculus will be given in Theorem 4.6.7 and Remark 4.7.4.
The force of functoriality It is easy to get into the (bad) habit of only defining the effect of a functor on objects, since we usually write them in this way. The force of functoriality, however, lies in the definition on morphisms and the preservation of composition.
EXAMPLES 4.4.6 The following are not functors.
Category theory was first used in algebraic topology, which aims to assign an (easily calculable) algebraic structure to each topological space in order to distinguish between spaces. For example (only) the nth reduced homology group is non-trivial for the sphere Sn which embeds in (n+1)- dimensional space. The homeomorphisms ( ie topological isomorphisms, and even the continuous functions) between the spaces also give rise to isomorphisms (respectively homomorphisms) between the corresponding groups. It is this property which enables algebraic structures to distinguish the spaces.
REMARK 4.4.7 Suppose \typeX1 º \typeX2 in C, ie there is a pair of morphisms u:\typeX1® \typeX2 and |:\typeX2®\typeX1 with u;| = \id\typeX1 and |;u = \id\typeX2; we say that the two objects are isomorphic ( cf Lemma 1.3.11).
Hence if \typeX1,\typeX2 Î C are two objects and F:C® D is a functor (such as homology) for which F \typeX1 and F \typeX2 are not isomorphic in D, then \typeX1 and \typeX2 are not isomorphic in C. []
Full and faithful Since objects are only defined up to isomorphism, it is harmless (and often useful) to make isomorphic duplicates of them (for example in our use of variables, Remark 4.3.14). For this reason injectivity and surjectivity on objects are not particularly important for functors. The force of functoriality is, as we have said, on morphisms.
DEFINITION 4.4.8 Let F:C® D be a functor.
Similarly, a full subcategory is one whose inclusion functor is full, so it shares the same hom-sets and is determined by its objects. Conversely, a wide or lluf subcategory is one with the same objects, but perhaps fewer morphisms. A replete subcategory U Ì C is one which is full with respect to isomorphisms and is such that if X Î obU and X º Y in C then Y Î obU; this happens, for example, when U is defined by a universal property.
There is a moral to this: the full subcategory of CSLat consisting of powerset lattices has forgetful functors successively to CSLat, Pos\dashv, Pos, Set and finally Rel, but is itself equivalent to Rel. This shows that it is misleading to regard forgetful functors as providing a hierarchy of simplicity amongst categories: the notion is entirely dependent upon presentation, and indeed some of the functors in Examples 4.4.4 would be regarded as forgetful by certain authors.
The ``true form'' (in Plato's sense) of a mathematical object is the totality of constructions from it - its presentations are only images (in both the Platonist and functorial senses). This is in the modern spirit of object-oriented programming, in which data-objects are available only via constructions and not as their substance (machine representation).