This section and the next study the categorical notions of subsets and injective functions, cf Exercise 1.16; Remark 5.8.4 discusses surjective functions for their own sake, rather than by duality. In Set a function which is both mono and epi is an isomorphism, but this fails in most other categories of interest: Proposition 5.8.10 shows what is needed.
DEFINITION 5.2.1 A map m:U® X in a category is called
Dually we have (regular, split) epimorphisms or epis - please, not ``epics.'' Monos are often indicated by a hook on the arrow (\hookrightarrow or \rightarrowtail ) and similarly epis by \twoheadrightarrow (or, but not in this book, by ® ); notice that the hook is at the end where the cancellation properties hold.
See Examples 5.7.5 for the familiar cases.
PROPOSITION 5.2.2 Let m:U® X be any map of any category.
|
Let F:C® D be a functor. Then
For any two maps m:X® Y and \:Y® Z,
REMARK 5.2.3 The class of split monos is not closed under pullback, but instead generates the class of regular monos (so a regular mono is ``possibly split'' in the sense of Definition 3.8.2). For if m is the equaliser of f,g:X\rightrightarrows Z then it is the pullback along f,g of the diagonal Z® ZxZ (assuming that this exists). The pullback u*m:V® Y of m along any map u:Y® X is also regular mono, being the equaliser of (u;f) and (u;g).
omitted diagram environment
The class of plain monos is also stable under pullback. See Example 5.4.6(e) and Lemma 5.5.7 regarding coproduct inclusions X® X+Y, and Exercise 5.37 for pullbacks of split epis. []
DEFINITION 5.2.4 A subobject of an object X is an equivalence class of monos m:U\hookrightarrow X, where this is identified with \:V\hookrightarrow X if there is an isomorphism f:U º V such that m = f;\.
omitted diagram environment
If there is any map f (necessarily a unique mono, by the cancellation properties) making this triangle commute, we write m £ \ or U Ì X V.
REMARK 5.2.5 We write \SubS(X) for the class of subobjects. It is the full subcategory (S¯ X) of the slice S¯ X (Definition 5.1.8) consisting of those objects d:U® X for which d is mono. There is no a priori restriction on the morphisms, but in the case of monos (and not in the similar but more general situation, S¯ X, of Definition 8.3.8) f is forced to be mono and unique. The latter makes \SubS(X) a preorder, so we take the poset reflection (Proposition 3.1.10). If this is small (a set) for all X then we say that S is well powered.
We said that pullbacks arise in type theory as equality types, products and substitution. When restricted to subobjects, the equality types become trivial (Proposition 5.2.2(a)), but the product and substitution are known as intersection and inverse image (u-1). The pullback u* considered as a functor says that if U Ì V then u-1(U) Ì u-1(V).
If the category S is well powered and has inverse images then there is a functor Sub:Sop® SLat, with Sub(u) = u-1.
PROPOSITION 5.2.6 In Set, the type W of propositions is a subobject classifier. That is, for any mono m:U\hookrightarrow X, there is a unique function cm:X® W which makes the square a pullback:
omitted diagram environment
In other words, the natural transformation S(-,W)® Sub(-) defined by the square is an isomorphism, so the functor Sub is representable (Definition 4.8.13) by W (we introduced the symbol W in Notation 2.8.2).
PROOF: For x:X, define cm(x) º (x Î U):W.
Although the pullback is given only up to isomorphism, the subobject is unique, being defined as an isomorphism class. To show that the isomorphism S(-,W)® Sub(-) is natural, use Lemma 5.1.2.[]
Using cartesian closure, the functor \SubS(-xX) is also representable, by the powerset P(X) = WX (Definition 2.2.5). These properties, including the existence of pullbacks, are precisely what we need to model Zermelo type theory, ie to axiomatise the category of sets and functions. Such a category is called an elementary topos. These properties extend to the functor category SetCop for any small category C, by Exercises 4.41, 5.8 and 5.13, so presheaves form a topos.
COROLLARY 5.2.7 Every mono m in Set is regular, because it is the equaliser of cm and x® T. []
We are running way ahead of ourselves in discussing higher order logic at this point: the purpose of this chapter is to present the traditional categorical account of the first order logic of sets. Section 9.5 returns to the comprehension and powerset axioms in type theory.
Sets of solutions of equations There is no recognisable axiom of comprehension in toposes, because they use monos instead of actually considering the predicate calculus ( cf Remark 2.2.4). We do, however, have a theory of equations, and can reconstruct a certain amount of logic around them. Recall the context notation [[(x)\vec]:[(X)\vec]] from Definition 4.3.11.
REMARK 5.2.8 A subobject defined as the equaliser of a pair of maps,
omitted diagram environment
is the set of solutions to the equation a([(x)\vec]) = b([(x)\vec]).
For example, this could be the set of roots of a polynomial, or some geometrical figure such as the circle x2+y2 = r2.
Either by replacing A with a context, or by using pullbacks (intersection of subobjects), this treatment of a single equation extends easily to the simultaneous solution of a family of them, a = b, ie to conjunction.
omitted diagram environment
Given the interpretations of equations a = b and c = d, we may express the (semantic) entailment ( cf Corollary 4.6.8),
|
omitted diagram environment
We may consider a general map (substitution) u:[[(x)\vec]:[(X)\vec]]® [[(y)\vec]:[(Y)\vec]] instead of repeating the object [[(x)\vec]:[(X)\vec]] in this diagram, but this only substitutes u([(x)\vec]) for [(y)\vec] in c and d.
If the fill-in is invertible then a = bÛ c = d.
Besides equality and conjunction, there is another connective which can be expressed using finite limits.
REMARK 5.2.9 Recall that we wrote [^(y)]:XxY® X for the product projection in Definition 4.5.7. In this case, if there is a fill-in
omitted diagram environment
then
|
|
The inverse map, which we have already supposed to be present in the category, is an operation of arity [(X)\vec]\vdash Y, defined conditionally on the equations c([(x)\vec]) = d([(x)\vec]). We may give it a name, ie conservatively extend the language, using the i-calculus (Lemma 1.2.11).
Entailments of this form may be used as axioms for a generalised algebraic theory. For example, categories may be defined using the condition
|
Peter Gabriel and Friedrich Ulmer [GU71] proved the duality linking small lex categories qua theories to their categories of models, which are locally finitely presentable categories (Definition 6.6.14(c)). Chapters 2 and 3 of [MR77] provide a textbook account of this approach (there's no need to read Chapter 1 first), as does [BW85] , which uses sketches.
Proposition 5.6.4 describes equivalence relations categorically in this way. Remark 5.8.5 discusses $ without the uniqueness condition. In my view it is more natural to describe the theory of categories using dependent types (Example 8.1.12).
Special subobjects Algebraic equations typically describe a smaller class of subobjects than general predicates do. We may similarly wish to restrict attention to recursively enumerable sets or those of some other low degree of logical complexity. In categories other than Set, perhaps not all monos are regular or ``well behaved'' in some other sense. For such a class to be useful it must at least be closed under inverse image, ie be invariant under substitution.
DEFINITION 5.2.10 A class M Ì morS of monos such that
is called a class of supports or a dominion. Of particular interest is the case where there is an object S equipped with a global element T:1® S having the same property for M that W has for all monos in Set. This is called a support classifier or dominance. If both S and W exist then there is a Ù-semilattice inclusion S\hookrightarrow W (Exercise 5.12) .
EXAMPLES 5.2.11 The following are dominions:
Classes of monos will be used as the supports of partial functions in the next section. Pullback-stable classes of maps which are not necessarily monos will be needed to interpret dependent types in Chapters VIII and IX. We study support classifiers and the powerset in Section 9.5.