Practical Foundations of Mathematics

5.2  Subobjects

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

(a)
a monomorphism or mono if the post cancellation property holds: given any a,b:G \rightrightarrows U, if a;m = b;m then  a = b (reading maps from G as generalised elements in the sense of Remark 4.5.3, this says exactly that m is injective Definition  1.3.10(a)),

(b)
a regular mono if it is the equaliser (Definition  5.1.1(a)) of some parallel pair ( cf Lemma 5.6.6(a) for a canonical such pair), and

(c)
a split mono if there is a postinverse e:X \twoheadrightarrow U with m;e = \idU.

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.

(a)
Then m is mono iff the square is a pullback:

 omitted diagram environment            omitted diagram environment

(b)
In particular this happens if m is the structure map of an equaliser.

Let F:C® D be a functor. Then

(c)
if m is split mono then so is Fm;

(d)
if F preserves pullbacks and m is mono then so is Fm ;

(e)
if F preserves equalisers and m is regular mono then so is Fm.

For any two maps m:X® Y and \:Y® Z,

(f)
if m and \ are mono then so is m; \, and similarly for split monos, but Example  5.7.5(d) shows that this may fail for regular monos;

(g)
conversely if m;\ is (split) mono then so is m;

(h)
if m;\ is regular mono and \ is mono then m is regular mono. []

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

The lattice of subobjects

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),

 ®x : ®X \vDash a( ®x ) = b( ®x )Þ c( ®x ) = d( ®x ),
ie that the set of solutions to one is contained in the other, by saying that there is a fill-in as shown, making this square commute:

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

 " ®x .($y.a( ®x ,y) = b( ®x ,y)) Þ c( ®x ) = d( ®x ). But if the fill-in is an isomorphism we also have the converse,  " ®x .c( ®x ) = d( ®x ) Þ$!y.a( ®x ,y) = b( ®x ,y),
where the existential quantifier is unique.

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

 tgtf = srcg  Ù   tgtg = srchÞ (f;g );h = f;(g;h).
Peter Freyd styled such theories essentially algebraic [ Fre72], since products, coproducts and equalisers (but not quotients) of models are found in the same way as for the algebraic theories in Section 4.6. Michel Coste set out the fragment of predicate calculus consisting of equality, conjunction and unique existence [Cos79]; he used the term lim-theory, since to define a classifying category analogous to that in Theorem 4.6.7 we must use (at least some) pullbacks.

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

(a)
all isomorphisms are in M,

(b)
if m:X® Y and \:Y® Z are in M then so is m;\, and

(c)
if m:X® Y is in M and u:Y¢® Y is arbitrary then the pullback u*m:X¢® Y¢ exists and is in M

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:

(a)
all monos in Set, classified by W ( Proposition 5.2.6);

(b)
upper subsets in Pos, also classified by W (Example 3.1.6(f));

(c)
algebraic equations in CRngop, the category of affine varieties (not classified);

(d)
open subsets in Dcpo, IPO, Sp or Loc, classified by the Sierpi\'nski space S (Definition 3.4.10);

(e)
recursively enumerable subsets in a certain category composed of total recursive functions; Exercise 5.10 describes the classifier.

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.