Practical Foundations of Mathematics

Paul Taylor

5.5  Extensive Categories

Now we shall look more closely at disjoint unions as we find them in Set, in some categories of ``spaces,'' in type theory and in programming languages. In particular, in the last setting we find two constructs which involve branching or case analysis, namely if then else, and the tagged sum type. In mathematics, Examples 4.6.4 (including the theory of fields and the characterisation of free algebras such as N and List(X)) have an algebraic flavour but involve exceptions such as zero; coproducts are needed to define classifying categories for them.

The notion of stable (or universal) disjoint coproduct was recognised by the Grothendieck school ( c. 1960), and is part of Jean Giraud's characterisation of sheaf toposes. However, our categorical account is based on ideas of Steve Schanuel and Bill Lawvere from about 1990. The details are due to Robin Cockett [Coc93], Aurelio Carboni, Steve Lack and Robert Walters [CLW93].

The weaker of the two notions which we consider corresponds exactly to a type theory with products and sums (Section 2.3), but I do not know of a syntactic calculus for the stronger one, other than by restricting full predicate logic. This is unfortunate, as it is this one which we want, but the actual difference between the two is less than it may seem.

Distributivity   Recall the second diagram in Example 5.3.10: this omitted the variable a because it is not used during the conditional. Clearly we do not want the local behaviour of the program to depend on how many (unused) global variables are also present.

DEFINITION 5.5.1 A category with finite products and coproducts is said to be distributive if, for all G,Y,N Î obS,

omitted diagram environment

is a coproduct diagram ( cf Definition 5.4.1 ). The analogous property for nullary coproducts is Gx0 º 0, which is equivalent to saying that any map G® 0 is an isomorphism ( cf Proposition 2.1.9(b)); in this case we call 0 a strict initial object.

This restores the parameter-context G to the rule in Remark  2.3.10,

omitted diagram environment

(Recall from Definition 4.5.7 the use of ® for the product projection p₁.) In this case the maps

In particular, for total programs f,g:G\rightrightarrowsQ and c:G® 2, we have

REMARK 5.5.2 Theorem 4.6.7 showed that each algebraic theory  L is classified by a category \Clone_L^x with products. The objects of \Clone_L^x were contexts, consisting of variables of base type. In Section 4.7 we gave a similar construction ( Cn^® _L) for the l- calculus, where the objects are still contexts, but consisting of type- expressions in the constructor ® . If L was just an algebraic theory then Cn^® _L is the free cartesian closed category on \Clone_L^x.

The same can be done for sum types, by allowing the types listed in contexts to be expressions such as X+Y rather than X® Y. The terms may now involve the coproduct injections n₀ and n₁ together with the conditional [  ,  ], for which the b-, h-, substitution and continuation rules were given in Section 2.3. The category \Clone_L^x+ of such contexts and substitutions is distributive (from the substitution rule), and the models of L in S correspond to (x,+)-preserving functors \Clone_L^x+® S. As these automatically preserve Definition 5.5.1, the semantic category S must be distributive too. If L was only an algebraic theory then \Clone_L^x+ is the free distributive category on \Clone_L^x; the inclusion \Clone_L^x\hookrightarrow\Clone_L^x+ can be shown to be full and faithful, so the extension is conservative (Sections 7.6- 7.7).

Extensive categories   For categories rather than lattices, it is natural to state the distributive law more generally: that coproducts are to be stable under pullback. That is, if we replace Gx(Y+N) above with an arbitrary object C and form the two squares as pullbacks, the top row still has the universal property of a coproduct. (In fact this stronger property does already hold for distributive lattices, but trivially, as pullbacks exist but are no more general than meets, by Example 5.1.3(a).)

What distinguishes the sums we require from joins in lattices is that joins are idempotent, but we want components to be disjoint. This property can be formulated as the ``converse'' of stability under pullback. The term extensive describes properties such as mass, volume and force which increase with quantity, as opposed to intensive properties like density and acceleration which remain the same.

DEFINITION 5.5.3 An extensive category is one which has finite coproducts, such that every commutative diagram of the form

omitted diagram environment

is a pair of pullbacks iff the top row is a coproduct diagram.

If the category has 1, by Lemma 5.1.2 it suffices to consider A = B = 1.

In a distributive lattice, the rows can be coproducts (joins) without the squares being pullbacks (meets), as NÇB and YÇA can be non-trivial.

LEMMA 5.5.4 Consider the following commutative diagram, in which the rows are coproducts.

omitted diagram environment

(a)

Then the two lower squares are pullbacks iff

(b)

for all commutative trapezia there are unique N¢® N and Y¢® Y making the whole diagram commute.

PROOF: To test Y, put N¢ = 0. []

COROLLARY 5.5.5 A category S with finite coproducts is extensive iff

PROOF: By the lemma, this functor is full and faithful iff coproducts imply pullbacks. Essential surjectivity says that the source of any map into A+B must be a coproduct N+Y that makes the squares commute, but these squares are pullbacks by the first part. []

EXAMPLES 5.5.6

(a)

Set enjoys these properties by Exercise  2.13.

(b)

Pos, Dcpo, Sp, Gpd and Cat are extensive, since the forgetful functor to Set creates coproducts and pullbacks.

(c)

Loc º Frm^op and CRng^op are also extensive (Exercise  5.31). []

Exercise 5.35 explains, using partial maps, why the category of virtual objects in Section 5.3 must be extensive rather than just distributive to interpret conditionals.

Stable disjoint sums   This is the traditional formulation.

LEMMA 5.5.7 In an extensive category with finite limits,

(a)

coproducts are stable, ie the pullback of any coproduct diagram is another one (in particular the distributive law holds);

(b)

the initial object 0 is strict;

(c)

the components of the coproduct are disjoint, ie the square on the left is always a pullback. omitted diagram environment

From these three properties, rather than extensivity, it follows that

(d)

if the middle square commutes then U º 0;

(e)

for disjointness of general binary coproducts, it suffices that 0 be strict and that the square on the right be a pullback, ie yes ¹ no;

(f)

the maps Y® Y+N¬ N are monos ( cf Example  5.4.6(e));

(g)

in fact they are regular monos, assuming extensivity.

PROOF: [a] is part of Definition 5.5.3. For [b,c] consider

omitted diagram environment

which are clearly coproducts, therefore pairs of pullbacks; so X¬ 0 is the pullback of the isomorphism 1¬ 1.

(a)

[[d]] The mediator to the pullback is U® 0 by (c), so U º 0 by (b).

(b)

[[e]] Form a cube from the middle and right hand squares.

(c)

[[f]] Form the pullbacks U and V in the left hand diagram below, then U º 0 by disjointness; but B = U+V by stability, so B º V is the pullback in Proposition  5.2.2(a). omitted diagram environment

(d)

[[g]] The inclusions 1\hookrightarrow 2 \hookleftarrow 1 are split mono, so general coproduct inclusions are regular mono by Remark  5.2.3. []

THEOREM 5.5.8 A category with pullbacks is extensive iff it has stable disjoint sums and a strict initial object.

PROOF: It remains to show that Y is a pullback in the diagram below, so take a commutative square with vertex G. Form the pullbacks U and V, so G = U+V since the coproduct Y+N is stable ( cf the proof of Lemma 5.5.7(f)). Now we have a commutative trapezium from U to A+B via A and B, so U º 0 by Lemma 5.5.7(d).

omitted diagram environment

G º V® Y is the pullback mediator: the triangle G® Y+N is actually the top right square, which commutes; that to B commutes because the composites as far as A+B are equal and B\hookrightarrow A+B by Lemma  5.5.7(f). The mediator is unique because Y\hookrightarrow Y+N. []

Interpretation of theories with disjunction   Examples 4.6.4 listed some mathematical structures that are almost algebraic theories, but which have exceptions such as (division by) zero and ( popping) the empty stack, cf the predecessor (Remark 2.7.9).

EXAMPLES 5.5.12 The theories of natural numbers, lists (Section 2.7), number fields and projective planes involve axioms of the form

omitted eqnarray* environment

in which there is only one witness to each existential quantifier, and only one term of each disjunction can be satisfied. These things can be proved from the theory because they also have axioms of the form

REMARK 5.5.13 Unique existential quantification has already arisen for ``essentially'' algebraic theories (Remark 5.2.9), but the unique disjunction is a new feature of extensive categories. The property

How can we define a classifying category for such a theory, short of interpreting the whole of the predicate calculus? The sum calculus of Remark 2.3.10ff can express N º 1+N and L º 1+XxL, but, without extending the fragment [] = (x,+) of logic to include pullbacks, there is nothing to force [[-]]:Cn^[]_L® S to preserve the pullback which expresses disjointness. ( A priori we do not even know that this square is a pullback in Cn^x+_L, though it follows from Section 7.7 that in fact it is.) However, the tradition of sketch theory, like that of model theory, has only considered the situation where S = Set, so the coproduct diagram in the semantics is necessarily stable and disjoint.

There is no avoiding other finite limits in the cases of fields and projective planes, as the axioms themselves involve equations.

REMARK 5.5.14 The category Mod(L) of models and homomorphisms of such a theory need not have products, though it still has pullbacks, equalisers, and indeed limits of all connected diagrams (Examples  5.1.5).

The axioms above say that lists and natural numbers can be parsed, an idea which we shall take up again in Chapter VI. Infinitary sums will be treated type-theoretically in Section 9.3. The rest of this chapter is about coequalisers, but we postpone stability for them until Section 5.8, where it is also combined with extensivity to give the notion of pretopos. Virtual objects reappear there and in Section 6.4, which interprets an imperative language with while.