Theory and Applications of Categories, Vol. 4, No. 10, 1998, pp. 208–248.

ON GENERIC SEPARABLE OBJECTS

ROBBIE GATES

Transmitted by R.J. Wood

ABSTRACT. The notion of separable (alternatively unramified, or decidable) objects and their place in a categorical theory of space have been described by Lawvere (see [9]), drawing on notions of separable from algebra and unramified from geometry. In [10], Schanuel constructed the generic separable object in an extensive category with products as an object of the free category with finite sums on the dual of the category of finite sets and injections. We present here a generalization of the work of [10], replacing the category of finite sets and injections by a category A with a suitable factorization system. We describe the analogous construction, and identify and prove a universal property of the constructed category for both extensive categories and extensive categories with products (in the case A admits sums). In constructing the machinery for proving the required universal property, we recall briefly the boolean algebra structure of the summands of an object in an extensive category. We further present a notion of direct image for certain maps in an extensive category, to allow construction of left adjoints to the inverse image maps obtained from pullbacks.

1. Introduction

A category X is said to be extensive (see [3]) if X admits finite sums, and for each pair of objects X and Y of X, the functor

[figure: X /X; ×; X /Y; X /(X + Y); A  B  A + B; ,; X; f; Y; g; X + Y; f + g]  (1)

obtained from the sums is an equivalence. If we consider the objects of the comma category X /X as being like X-indexed families in X, this equivalence asserts that to give an (X + Y)-indexed family of objects is precisely to give both an X-indexed and a Y -indexed family of objects. A useful motivating case is that of X = Sets_{f} (the category of finite sets), where the comma category Sets_{f}/X is (equivalent to) the exponential Sets_{f}^{X}, and the assertion that the arrow of (1) is an equivalence is precisely the familiar exponential law

Sets_{f}^{X} × Sets_{f}^{Y} ≃ Sets_{f}^{(X+Y)}

Received by the editors 1998 July 24 and, in revised form, 1998 December 4. Published on 1998 December 18. 1991 Mathematics Subject Classification: 18D99 (18B15, 18C10). Key words and phrases: extensive category, separable object, generic solution, direct image. \begin{matrix}c \\ ◯ \end{matrix} Robbie Gates 1998. Permission to copy for private use granted.

An alternative (equivalent) definition of extensivity is that X admit finite sums and pullbacks along injections of finite sums, and that for any commuting diagram in X of the form

[figure: A; C; B; X; i; X + Y; j; Y]

for which the bottom row is a sum, we have that the squares are pullbacks if and only if the top row is a sum. It is this latter formulation we shall typically use in the current paper, the advantage of the former being that it shows clearly that extensivity is a property of the sums of X. In particular, an extensive category is not presupposed to admit any limits – the pullbacks arising in the second formulation arise because the sums of X are well-behaved.

In the event that an extensive category does possess finite products, it is then automatically distributive – i.e., the canonical map

X × Y + X × Z → X × (Y + Z)

obtained from products, the injections and the universal property of sums is invertible.

An object X of an extensive category with finite products is said to be separable if the diagonal Δ: X → X^{2} is a summand. The summands in an extensive category with products enjoy closure under composition (associativity), sums (commutativity), and products (distributivity). These closure properties allow construction of many summands from a given summand, such as the diagonal. In particular, given a function e: A → B in Sets_{f} and an object X of a category with products, we obtain an arrow X^{e}: X^{B} → X^{A} from the universal property of products in the usual way. The diagonal is the map obtained in this way from the surjection 1 + 1 → 1 in Sets_{f}. Using the closure properties of summands and the fact that all surjections in finite sets can be constructed from sums and composites of the surjection 1 + 1 → 1, we can show:

1.1. Proposition. Given a separable object X of an extensive category with products, and a surjection e: A → B in Sets_{f}, the arrow X^{e}: X^{B} → X^{A} is a summand.

In general, an arrow of the form X^{e} for arbitrary e: B → A may be thought of as producing A-tuples of Xs from B-tuples of Xs by rearranging, duplicating (in the event e is not injective), or omitting (in the event e is not surjective) entries.

In [10], Schanuel described the construction of a generic separable object in an extensive category with products. One considers the free category with sums on the dual of the category of finite sets and injections – this is a category of families, and the family with the single element 1 is the desired generic separable object. A natural generalization of this notion is to consider what can be said about the free category with sums on the dual of the category of Ms of an (E, M)-factorization system. This is the question considered in this paper – such categories are shown to have a universal property. The universal property is analogous to that described by proposition 1.1 – the surjection e is replaced by an E of the factorization system, and exponentiation is replaced by a suitable functor.

In the course of analyzing this universal property, one has cause to consider in reasonable detail the boolean algebra of summands of an object of an extensive category. As well as recalling well known aspects of this structure in section 3, we present in section 4 a definition for a notion of direct images of summands in an extensive category. The property is enjoyed by structural maps in the extensive category (such as summands and codiagonals) and is preserved by extensive operations (composition, sums and pullback along summands). Importantly, it is also strong enough to allow construction of a right adjoint to the inverse image map on summands given by pullback. These direct image maps considerably simplify certain calculations with summands used in establishing the universal property.

The motivation for this work is primarily a desire to understand more deeply the construction of the generic separable object in the classic case. Using objects of an extensive category with products as categorical models of data types (see [12] and [13]), an object which is separable is an object possessing an equality operation – to give a complement for the diagonal of X is precisely to give a map X^{2} → 1 + 1 with pullback against one of the injections being the diagonal, i.e., an equality predicate. Categories of families of the dual of a category with sums arise in finding generic solutions to polynomial equations (see [7]), which can be seen as generic data types of a certain kind. It would seem natural to combine these two constructions to find generic separable solutions to polynomial equations, and thus construct generic data types having equality operations. Another view of this work is that it is a specific case of universally making a given family of maps into summands – the author is not aware of general conditions on a family of arrows in an extensive category that yield a tractable construction of such a universal category.

1.2. Remark. The notation is this paper is largely standard, and new notation is described where it is introduced. A possible exception is the notation (f | g) (resp. (|_{i} f_{i})) for the arrows out of binary (resp. familial) sums constructed via the universal property. In the case of familial sums where the precise family is not clear from context, the family involved will be given in the subscript, such as (|_{i∈I} f_{i}). Also, all references to sums and products are taken to mean finite sums and finite products, although we shall occasionally say finite for emphasis. We denote the 2-category of extensive categories, sum preserving functors and natural transformations by Ext.

1.3. Acknowledgements. An earlier version of this work appeared in the author’s thesis (see [6]). This treatment clarifies somewhat the work on images, and gives a proof of the universal property for the case of extensive with products which was lacking in [6]. The author thanks the Australian Research Council for their support for this project. The author acknowledges the use of Paul Taylor’s diagrams macro package in the production of this paper. The author wishes to thank the participants of the Sussex Category Meeting, July 1996 and the members of the Australian Category Seminar for hearing talks on this material and offering insights. The author also expresses his gratitude to R. F. C. Walters, for Ph.D. supervision when the majority of this work was done, and to the markers of [6], for their detailed comments.

2. Stirling Exponents and Stirling Polynomials

As described in the introduction, our general context will be a small category A with a suitable (E, M)-factorization system and possibly with finite sums. After introducing the factorization systems of interest, we examine the category of families of M^{op}. We show this category has products when A has sums, and identify which objects are separable – that is, have their diagonal a summand (see [1] and [9]). We also investigate the relation of this category to the category of families of A^{op}. We describe how to view these categories as categories of polynomials, and give an adjunction between these categories.

For details on factorization systems the reader is referred to [2] and [5]. It should be noted that references to these below are references to standard results on factorization systems – the deeper theory of factorization systems is not required for our purposes here.

We begin by making precise what we require of our factorization system:

2.1. Definition. By a category of Stirling exponents (A, E, M) we mean a category A and an (E, M)-factorization system on A, such that

(SE1) Every e ∈ E is epic in A.

(SE2) Pushouts of any arrow along an e ∈ E exist in A.

(SE3) The collection of isomorphism classes of E-quotients of any A in A is finite.

It should be noted this definition differs from that given in [6], inasmuch as the the requirement that A possess finite sums has been removed. Rather, we shall note precisely which results depend on sums in A.

Before continuing, we note for reference a lemma which appears as a part of proposition 2.1.4 of [5] and of proposition 2.5 of [2] – in the latter reference note that the conditions on the category are unnecessary for the result we require.

2.2. Lemma. Let (E, M) be a prefactorization system on a category A such that every E is epic. Then

(i) If f: A → B and g: B → C in A are such that fg is an M, then g is an M.

(ii) If f: A → B and e: B → C in A are such that fe is an M and e is an E, then e is invertible.

Proof. The first result is dual to (a)⇒(c) in proposition 2.1.4 of [5], or precisely (a)⇒(b) in proposition 2.5 of [2] (this implication not requiring the completeness or cocompleteness conditions imposed there). The second result is an immediate corollary, on noting the fact that an arrow which is both an E and an M is invertible.

2.3. Notation. For the remainder of this section, we fix a category of Stirling exponents (A, E, M).

Combinatorially speaking, the Stirling numbers of the second kind, denoted S(n, k), count the partitions of an n element set into k blocks. Categorically, we see S(n, k) counts the isomorphism classes of surjections from an n element set to a k element set in the category of finite sets. This is the motivation behind selecting the adjective Stirling to describe these notions – as property (3) above suggests, we shall have cause to consider the isomorphism classes of E-quotients of objects of A. The following construction records the basic properties we can arrange in a class of representatives of the E-quotients of a given object:

2.4. Construction. For each A ∈ A, we select a finite set I; a distinguished element i_{∗} ∈ I; and a family (A_{i}, a_{i}) for i ∈ I, where each A_{i} ∈ A and each a_{i}: A → A_{i} is an E; such that

(i) The family (a_{i})_{i∈I} is a complete, irredundant set of representatives of the isomorphism classes of E-quotients of A.

(ii) We have A_{i_{∗}} = A and a_{i_{∗}} = 1_{A}.

(iii) If a_{i} is invertible for i ∈ I, then i = i_{∗}.

(iv) Given any f: B → A in A, we may factorize f as f = m · a_{i} for a unique i ∈ I and unique m ∈ M.

We shall write Quo_{E}(A) = (A_{i}, a_{i}, I, i_{∗}) to describe this situation.

Proof. Construct I and the family (A_{i}, a_{i}) for i ∈ I by selecting representatives as described in part (i). By property (3), the set I is finite. Since 1_{A} is an E, we may choose it to represent its isomorphism class, and denote by i_{∗} the index of this class in I. If a_{i} is invertible, then it is isomorphic to 1_{A} as an E-quotient of A. Hence irredundancy of the representatives implies that a_{i_{∗}} is the only invertible a_{i}.

For any f: A → B in A, we may factor f = m · e with m an M and e an E. For some i ∈ I, we have e ≅ a_{i} as E-quotients of A, by completeness of the representatives. Thus we may choose our factorization to be f = m · a_{i} for some i ∈ I. Finally, if m · a_{i} = n · a_{j} where m and n are Ms and i, j ∈ I, uniqueness of factorizations gives an isomorphism α: A_{i} → A_{j} commuting with the factorization; i.e., such that α · a_{i} = a_{j} and n · α = m. Irredundancy of the representatives implies that i = j, and so a_{i} = a_{j}. Now a_{i}, being an E, is epic by property (1). Hence α = 1_{A_{i}}, so m = n, and thus required uniqueness.

Recall that for a category A, we may construct the category of finite families in A^{op}, denoted Fam(A^{op}). This category is the free category with finite sums on A^{op}, and is extensive (see section 1 of [1], proposition 2.4 of [3], or section 5.2 of [4]). We use the notation P(A) for Fam(A^{op}), and think of it as a category of polynomials with exponents drawn from A. We denote objects of P(A) as sums of monomials, the family (A_{i})_{i∈I} being denoted

∑_{i∈I} X^{A_{i}}

Since sums in P(A) are given by disjoint unions of families, the sum of monomials notation yields the natural formula for sums in P(A). In the case A has sums, the category A^{op}, and hence P(A), has products. These products are given on monomials by the exponential law

X^{A} × X^{B} ≅ X^{A+B}

Products of sums of monomials are given by the distributive law, since an extensive category with products is distributive.

Similarly, we consider Fam(M^{op}) to be a category of polynomials of a kind:

2.5. Definition. Given a category of Stirling exponents (A, E, M), we define the category of A-Stirling polynomials, denoted by SP(A, E, M), or SP(A) for brevity, to be Fam(M^{op}). We shall denote the inclusion of M^{op} as one point families by

X^{[–]}: M^{op} ^{}SP(A)

and refer to X^{[A]} as a Stirling monomial. More generally, we write ∑_{i∈I} X^{[A_{i}]} for the family (A_{i})_{i∈I} in SP(A).

Informally, drawing intuition from the case of A = Sets_{f} with the surjection/injection factorization system, we think of the Es of A as describing identifications. For a surjection e: B → A, the image of X^{e} consists of those B-tuples whose entries are equal when their indices are identified by e. For an injection m: B → A in Sets_{f}, the arrow X^{m} will not duplicate entries, and thus carries distinct A-tuples to distinct B-tuples. The Stirling monomial X^{[A]} then can be thought of as distinct A-tuples, as the only arrows in SP(A) are those which “map distinct tuples to distinct tuples”.

We now show that if A has sums, then SP(A) has products. This is somewhat surprising for, as described above, the obvious way for Fam(M^{op}) to have products is for M to have sums. However, sums in A do not give sums in M in general – even if the injections in A are Ms (as they are in the case A = Sets_{f} and M is the injections), there is no reason for (m | n) to be an M even if m and n are Ms. Indeed, the product of two Stirling monomials is not usually a Stirling monomial. This situation is referred to as familial finite products in [4], however, as the category SP(A) is an object of primary interest here, we shall work with products in the category of families.

2.6. Construction. Suppose that A admits finite sums. For A, B ∈ A, consider a sum C = A + B in A with injections i: A → C and j: B → C. Writing Quo_{E}(C) = (C_{i}, c_{i}, I, i_{∗}) and

I_{×} = {i ∈ I | c_{i} · i ∈ M, c_{i} · j ∈ M}
p = (|_{i∈I_{×}} X^{[c_{i}·i]})
q = (|_{i∈I_{×}} X^{[c_{i}·j]})

the diagram

X^{[A]} ^{}^{p} ∑_{i∈I_{×}} X^{[C_{i}]} ^{q}^{}X^{[B]}  (2)

is a product in SP(A).

Proof. Firstly, observe that the claimed projection arrows are indeed arrows of SP(A), since i ∈ I_{×} implies that c_{i} · i and c_{i} · j are Ms. Secondly, extensivity of SP(A) and the fact that every object of SP(A) is a sum of Stirling monomials imply that we need only check the required universal property for cones from Stirling monomials.

To see that diagram (2) is a product diagram, take a Stirling monomial X^{[D]} together with X^{[m]}: X^{[D]} → X^{[A]} and X^{[n]}: X^{[D]} → X^{[B]} in SP(A). Factor (m|n): A+B → D uniquely as (m | n) = f · c_{j} for some j ∈ I and f: C_{j} → D an M. Now f · c_{j} · i = m and f · c_{j} · j = n are Ms. Since f is an M, we have that c_{j} · i and c_{j} · j are Ms (proposition 2.2(c) of [2]). Hence j ∈ I_{×}, and we have the arrow

X^{[D]} ^{X^{[f]}}^{}X^{[C_{j}]} ^{inj_{j}}^{}∑_{i∈I_{×}} X^{[C_{i}]}

in SP(A). We calculate

p · inj_{i} · X^{[f]} = X^{[c_{i}·i]} · X^{[f]} = X^{[f·c_{i}·i]} = X^{[m]}
q · inj_{i} · X^{[f]} = X^{[c_{i}·j]} · X^{[f]} = X^{[f·c_{i}·j]} = X^{[n]}

Thus we have produced an arrow as required for the product property.

For uniqueness, note that to give an arrow X^{[D]} to the claimed product is is to give j′ ∈ I_{×} and h: C_{j} → D in M, the given arrow being inj_{j′} · X^{[h]}. If this arrow satisfies the property defining inj_{j} · f above, a routine calculation shows and properties of sums imply that h · c_{j′} = (m | n), and uniqueness of the factorization which produced j and f implies that j′ = j and h = f.

Thinking informally, an element of the product of the distinct A-tuples and distinct B-tuples is classified by the amount of identification between the A-tuple part and the B-tuple part. However, no identification within the A-tuple part is permitted (since the A-tuple is distinct), and similarly for the B-tuple part; hence, we restrict the monomials in the sum yielding the product X^{[A]} × X^{[B]}.

2.7. Proposition. If A admits finite sums, then SP(A) admits finite products.

Proof. It suffices to consider existence of a terminal object and binary products. For the latter, construction 2.6 gives binary products of Stirling monomials. Every object of SP(A) is a sum of Stirling monomials, and so extensivity allows construction of all binary products. For the terminal object, we observe that, as for products, it suffices to produce terminal arrows from Stirling monomials.

Consider an initial object A of A and write Quo_{E}(A) = (A_{i}, a_{i}, I, i_{∗}). We claim that ∑_{i∈I} X^{[A_{i}]} is terminal in SP(A). For any Stirling monomial X^{[B]}, factoring the unique arrow A → B as m · a_{j} for j ∈ I by construction 2.4(iv) yields an arrow

X^{[B]} ^{X^{[m]}}^{}X^{[A_{j}]} ^{inj_{j}}^{}∑_{i∈I} X^{[A_{i}]}

as required by terminality. Uniqueness of this arrow follows routinely from the uniqueness in construction 2.4(iv) and the uniqueness of arrows from the initial A.

We now give the precise connection between the construction described here and the classical categorical definition of separable – namely, that the diagonal be a summand.

2.8. Proposition. Suppose that A admits sums. The following are equivalent:

(i) The object X^{[A]} of SP(A) is separable.

(ii) The codiagonal ∇: A + A → A is an E.

Proof. We use the notation of construction 2.6 with B = A. The diagonal of X^{[A]} is inj_{j} · X^{[m]}, where ∇ = m · c_{j} is the unique factorization of ∇ with j ∈ I and m an M. For this to be a summand is for m to be invertible.

To see that (i) implies (ii), observe that if m is invertible, it is an E, and so ∇ is a composite of Es and hence an E. For the converse, let us suppose that ∇ is an E. Since c_{j} is an E, we have that m is an E (proposition 2.1.1(e) of [5]). Thus m is invertible, and it follows X^{[A]} is separable.

In any extensive category with products, a sum X+Y is separable if and only if both X and Y are separable (part (3) of theorem 11 of [1]). Hence, in a category of families, such as SP(A), determining separability of the monomials is sufficient to determine separability of all objects.

We now describe a functor S: P(A) → SP(A) which, informally speaking, “separates” the objects of P(A) by classifying the A-tuples as distinct A-tuples with duplicated entries. Note that from the point of view of constructing classifying categories, or generic objects, functors from P(A) to an extensive category X are considered to be “objects” of a certain type in X. In this context, the functor S is an “object” of SP(A) – it is the “separable object” viewed as a mere “object”. In section 5, the functor S will play an integral role in the equivalence that is the universal property of SP(A).

2.9. Construction. We have a functor S: P(A) → SP(A) in Ext such that:

(i) For A ∈ A, writing Quo_{E}(A) = (A_{i}, a_{i}, I, i_{∗}), we have

SX^{A} = ∑_{i∈I} X^{[A_{i}]}  (3)

(ii) For f: B → A in A, writing Quo_{E}(A) = (A_{i}, a_{i}, I, i_{∗}) and Quo_{E}(B) = (B_{j}, b_{j}, J, j_{∗}), we have commutativity of

X^{[A_{i}]} \overline{inj_{i}_{}}SX^{A}

[figure: X^{[B_{j}]}; X^{[m_{i}]}; inj_{j}; SX^{B}; SX^{f}]

(4)

for each i ∈ I, where m_{i} · b_{j} = a_{i} · f is the unique factorization with j ∈ J and m_{i}

an M.

Proof. By the universal property of the families construction, it suffices to define S on monomials and arrows between monomials, and then this definition lifts to a unique functor P(A) → SP(A) in Ext.

Equation (3) defines S on monomials. Given an arrow between monomials X^{f} where f: B → A in A, we may uniquely factor a_{i} · f = m_{i} · b_{j} by construction 2.4(iv). This defines j ∈ J and m_{i} an M. Using universal properties of sums, we may thus take diagram (4) as the definition for S on arrows between monomials.

Functoriality of S is routine. The factorizations 1_{A_{i}} · a_{i} = a_{i} · 1_{A} (since identities are Ms), for i ∈ I, define SX^{1_{A}}. Diagram (4) and universal properties of sums imply that S preserves identities. For compositionality, use the fact that composites of Ms are Ms, paste two instances of diagram (4) to produce a third, and use universal properties of sums.

It is interesting to compare the definition of S on objects to the combinatorial identity

x^{n} = ∑_{k=0}^{n} S(n, k)(x)_{k}  (5)

where (x)_{k} = x(x − 1) … (x − k + 1), and S(n, k) is a Stirling number of the second kind (see [11], p. 35). Indeed, in the case where A is the category of finite sets with the surjection/injection factorization system, the sum defining SX^{A} is precisely an objective version of the right hand side of equation (5) – the sum of equation (5) is just that of equation (3) classified by the size of A_{i}. Note also that (x)_{k} counts the distinct k-tuples of x elements which agrees with our intuition that X^{[A]} consists of “distinct A-tuples”.

We now examine SX^{f} in the case that f is an E or an M:

2.10. Proposition. In the context of construction 2.9(ii), let f = e be an E. We have that SX^{e} is a summand.

Proof. Since e is an E, we see that a_{i} · e is an E for each i ∈ I. It follows that for each factorization a_{i} · e = m_{i} · b_{j}, the arrow m_{i} is an E (proposition 2.1.1(e) of [5]). So m_{i} is both an M and an E, and hence invertible.

Furthermore, if i, i′ ∈ I are such that a_{i} · e = m_{i} · b_{j} and a_{i′} · e = m_{i′} · b_{j} (that is, they factor through the same injection into the sum SX^{B}), then m_{i} and m′_{i} (isomorphisms by the previous paragraph) yield an isomorphism between a_{i} and a′_{i} as E-quotients of A. Irredundancy of the representatives comprising Quo_{E}(A) implies that i = i′. So the summands of SX^{A} map isomorphically to distinct summands of SX^{B}, and it follows SX^{e} is a summand in SP(A).

2.11. Proposition. In the context of construction 2.9(ii), let f = m be an M. We have a commuting diagram:

X^{[A]} \overline{inj_{i_{∗}}_{}}SX^{A}

[figure: X^{[B]}; X^{[m]}; inj_{j_{∗}}; SX^{B}; SX^{m}]

Proof. Since m is an M, we see that a_{i_{∗}} · m is an M, and thus factorizes as (a_{i_{∗}} · m) · b_{j_{∗}} (since b_{j_{∗}} is an identity). In diagram (4) then, we have j = j_{∗} and m_{i} = a_{i_{∗}} · m = m (since a_{i_{∗}} is an identity), and the result follows.

Applying Fam(–^{op}) to the inclusion of M as a subcategory of A yields an inclusion U: SP(A) → P(A), with UX^{[A]} = X^{A} on objects and UX^{[m]} = X^{m} on arrows. We now turn to showing that S is right adjoint to the inclusion U. We begin by constructing the unit and the counit of the adjunction:

2.12. Construction. In the context of construction 2.9(i), and with U the inclusion SP(A) → P(A), the data

ηX^{[A]} = inj_{i_{∗}}  (6)

gives the components of a natural transformation η: 1_{SP(A)} → SU at Stirling monomials.

Proof. To construct η it suffices to define it on Stirling monomials and lift it to SP(A) by the universal property of Fam(–). Equation (6) defines η on monomials, and naturality at m: B → A of M is precisely the result of proposition 2.11.

2.13. Construction. In the context of construction 2.9(i), and with U the inclusion SP(A) → P(A), the data

ϵX^{A} = (|_{i} X^{a_{i}})  (7)

gives the components of a natural transformation ϵ: US → 1_{P(A)} at monomials.

Proof. Again, the universal property of Fam(–) allows us to lift the above data to define ϵ fully. For naturality, it suffices to check at X^{f} in P(A) where f: B → A in A. With the notation of construction 2.9(ii), consider for each i ∈ I the diagram

X^{A_{i}}
[figure: inj_{i}; X^{a_{i}}]
∑_{i∈I} X^{A_{i}}  \overline{ϵX^{A} ^{}}X^{A}

X^{B_{j}}^{^{}X^{m_{i}}}
[figure: inj_{j}; X^{b_{j}}]
[figure: ∑_{j∈J} X^{B_{j}}; SX^{f}; ϵX^{B}; X^{B}; X^{f}]

where a_{i} · f = m_{i} · b_{j} is the unique factorization with j ∈ J and m_{i} an M. The left parallelogram is diagram (4), the definition of SX^{f}. The right parallelogram is the equation a_{i} · f = m_{i} · b_{j} expressed in terms of one element families. The triangles are the components of the definition of ϵX^{A} and ϵX^{B}, i.e., equation (7). The universal property of sums gives commutativity of the square, and hence the required naturality.

2.14. Proposition. Consider the functor S of construction 2.9 and U the inclusion SP(A) → P(A). We have an adjunction U ⊣ S with unit η and counit ϵ as defined in constructions 2.12 and 2.13.

Proof. We need only check the triangular equations, having already constructed and established naturality of η and ϵ.

Firstly, to check that 1_{S} = Sϵ · ηS, it suffices to check at monomials. For A ∈ A, write Quo_{E}(A) = (A_{i}, a_{i}, I, i_{∗}), and, for each i ∈ I, write Quo_{E}(A_{i}) = (B_{j}^{i}, b_{j}^{i}, J_{i}, j_{∗}^{i}). Then, for each i, we consider the following diagram:

X^{[A_{i}]}  \overline{X^{[1_{A_{i}}]} ^{}}X^{[A_{i}]}
∑_{j∈J_{i}} X^{[B_{j}^{i}]}  \overline{SX^{a_{i}} ^{}}SX^{A}
SX^{A}^{inj^{i}}^{}
∑_{i∈I} SX^{A_{i}}^{}^{inj^{i}}

(8)

[figure: ηX^{[A_{i}]}; inj_{i}]

[figure: SϵX^{A}] [figure: ηSX^{A}]

The left parallelogram is the definition of η lifted to sums of Stirling monomials. The triangle is S applied to the i’th component of ϵX^{A}. The top parallelogram follows from diagram (4), the definition of SX^{a_{i}}, on observing that construction 2.4(iv) gives the factorization

b_{j_{∗}^{i}}^{i} · a_{i} = 1_{B_{∗}^{i}} · a_{i} = 1_{A_{i}} · a_{i}

with 1_{A_{i}} an M. Thus diagram (8) commutes, and the top edge has composite inj_{i}. Thus the universal property of sums shows that SϵX^{A} · ηSX^{A} = 1_{SX^{A}} as required.

Now we check that 1_{U} = ϵU · Uη. Once again, it suffices to check this at Stirling monomials. Given A ∈ A with Quo_{E}(A) = (A_{i}, a_{i}, I, i_{∗}), we observe that

ϵUX^{[A]} · UηX^{[A]} = ϵX^{A} · inj_{i_{∗}} = X^{1_{A}}

using the definition of η, construction 2.4(iv), and the fact U preserves injections. This is precisely the required equality at the Stirling monomial X^{[A]}, and we have proved the claimed adjunction.

We obtain immediately

2.15. Corollary. The functor S of construction 2.9 preserves any limits of P(A).

In particular, in the case A admits sums, the functor S preserves the products then present in P(A). Let us return to the combinatorial identity of equation (5). In the case A = Sets_{f} with the surjection/injection factorization system, we have SX^{1} = X^{[1]}, and thus preservation of products gives an isomorphism

(X^{[1]})^{A} ≅ SX^{A}

which is an objective version of the equality of equation (5).

The observation of Schanuel (in [10]) described in the abstract is that, in the case of A = Sets_{f} with the surjection/injection factorization system, the category SP(A) possesses a universal property, namely, that the object X^{[1]} is the generic separable object in an extensive category with products. The proof proceeds by constructing, for a finite set A and a separable object X in an extensive category with products, an object which can be viewed as “distinct” A-tuples of X. This construction is carried out by manipulating summands of X^{A}.

In section 5, we shall identify and prove an analogous universal property for the category SP(A) in general – for an extensive category X (possibly with products), we identify which functors P(A) → X arise by composing S with a functor SP(A) → X. As described in the introduction, the analogue of proposition 1.1 identifies these functors. To facilitate a proof, we shall first develop some machinery for computing with summands of objects in extensive categories.

3. Calculating with Summands

In this section we present the basic results for the algebra of summands of an object in an extensive category. The results here are well known – the author learnt the basic theory at the CT’95 Summer School at Halifax [10].

3.1. Notation. For this section, we fix an extensive category X.

For an object X of X, the summands of X are preordered by the arrows of X – for summands s: S → X and t: T → X we shall write s ≤ t if there exists an arrow a: S → T of X such that t · a = s. Since summands are monic in an extensive category, the arrow a is necessarily unique if it exists – we shall refer to such an a as the comparison arrow exhibiting s ≤ t. We digress briefly to establish a property of comparison arrows, which may also thought of as the closure of summands under left division.

3.2. Lemma. Let s: S → X and t: T → X be summands in X. If a is a comparison arrow exhibiting s ≤ t, then a is a summand.

Proof. Consider a pullback of s and t:

U \overline{u ^{}}S
[figure: a]
[figure: T; v; t; X; s]

The arrow a, together with the identity of S and properties of pullbacks, yields a section of u, and note u is a summand (being a pullback of t), and hence monic. Thus u is invertible, and so a is isomorphic to v, which is a summand (being a pullback of u).

In the usual manner, the preorder on summands induces an equivalence relation “s ≤ t and t ≤ s” on the summands, and the equivalence class of s is denoted [s]. The set of such equivalence classes of a given object X is denoted by X^{∗}, which is a poset with the order induced by the preordering of summands.

In fact, the poset X^{∗} is a boolean algebra. We shall now describe the boolean structure of X^{∗} for X ∈ X, but omit the verification of most of the details. Note that the terms meet and join are understood to refer only to finite meets and joins.

The top element of the boolean algebra X^{∗} is ⊤ = [1_{X}]. The meet of [s] and [t] is the diagonal of the square formed by pulling back s and t, and we denote this diagonal s ∧ t. The requisite universal property follows from that of pullbacks in X.

Given a summand s: S → X, consider a complement ¬s: ¬S → X. Any summand isomorphic to s (as a summand) is complemented by ¬s, and extensivity of X implies that ¬s is unique up to isomorphism (as a summand). This allows us to define ¬[s] = [¬s] for any [s] in X^{∗}. We see that ¬¬[s] = [s], and can show that for any [s], [t] ∈ X^{∗}, we have [s] ≤ ¬[t] if and only if [t] ≤ ¬[s]. Hence ¬ gives an isomorphism of posets (X^{∗})^{op} → X^{∗}.

Since X^{∗} has a top and meets, it follows from (X^{∗})^{op} ≅ X^{∗} that X^{∗} has a bottom and joins. We compute immediately that ⊥ = ¬⊤ = [!], where !: 0 → X is the unique arrow. For elements [s] and [t] ∈ X^{∗}, their join is given by [s] ∨ [t] = ¬(¬[s] ∧ ¬[t]). Consider the following diagram, where all the squares are formed by pullback.

[figure: S ∧ T; T; ¬S ∧ T; S; s; X; t; ¬s; ¬S; S ∧ ¬T; ¬T; ¬t; ¬S ∧ ¬T]  (9)

Let S ∨ T be a sum (S ∧ ¬T) + (S ∧ T) + (¬S ∧ T), and let s ∨ t: S ∨ T → X be the arrow constructed by properties of sums from the diagonals of the pullback squares. Since pullbacks of sums are sums, and using associativity of sums, we see that s ∨ t is a complement for the diagonal of the lower right pullback square. Thus s∨t is a complement for the summand ¬s ∧ ¬t. It follows [s ∨ t] = [s] ∨ [t] in X^{∗}. We shall record two lemmas about joins.

3.3. Lemma. Consider summands s: S → X and t: T → X in X, together with a summand s ∨ t: S ∨ T → X such that [s ∨ t] = [s] ∨ [t] in X^{∗}. Let e_{s,t}: S + T → S ∨ T be the arrow constructed from the comparison arrows S → S ∨ T and T → S ∨ T using the universal property of sums. The arrow e_{s,t} is split epic, and moreover

(s ∨ t) · e_{s,t} = (s | t)

Proof. It suffices to do this for any representative of [s] ∨ [t] – in particular the representative given in the preceding paragraph. Now S ∨ T can, by associativity of sums, be expressed as a sum S + (¬S ∧ T), and e_{s,t} is split by the arrow mapping the summand S to the summand S, and including ¬S ∧ T in the summand T. The required factorization of (s | t) follows by direct computation of composites with injections.

3.4. Lemma. Consider summands s: S → X and t: T → X in X such that [s] ∧ [t] = ⊥ in X^{∗}. The arrow (s | t): S + T → X is a summand, and [(s | t)] = [s] ∨ [t].

Proof. With the notation of diagram (9), disjointness of s and t gives S ∧ T ≅ 0. Thus S ∧ ¬T ≅ S and ¬S ∧ T ≅ T, with both these isomorphisms being isomorphisms of summands. It follows that (s | t): S + T → X is isomorphic to s ∨ t: S ∨ T → X, and hence the result of the lemma.

The final stage in this exploration of X^{∗} is to show that it is distributive, and thus a boolean algebra. We commence by showing that meets distribute over binary disjoint joins. Given summands s: S → X, t: T → X and u: U → X, where [s] ∧ [t] = ⊥, we see that ([u] ∧ [s]) ∧ ([u] ∧ [t]) = ⊥, and applying lemma 3.4 we obtain the formulas

[s] ∧ [t] = [(s | t)]
([u] ∧ [s]) ∨ ([u] ∧ [t]) = [(u ∧ s | u ∧ t)]

Given pullbacks

[figure: U ∧ S; f; U; S; g; s; X; u; and; U ∧ T; h; U; T; k; t; X; u]

it is routine to check that

[figure: U ∧ S + U ∧ T; (f | h); U; S + T; (g + k); (s | t); X; u]

is a pullback. Together with the formulas above, we deduce

[u] ∧ ([s] ∨ [t]) = ([u] ∧ [s]) ∨ ([u] ∧ [t])

Inductively, we see that meets distribute over pairwise disjoint joins.

For any [s], [t] ∈ X^{∗}, we have [s] ∨ ¬[s] = ⊤ and [t] ∨ ¬[t] = ⊤, and note that

[s] ∨ [t] = ([s] ∧ ⊤) ∨ ([t] ∧ ⊤)
= (([s] ∧ [t]) ∨ ([s] ∧ ¬[t])) ∨ (([s] ∧ [t]) ∨ (¬[s] ∧ [t]))
= ([s] ∧ ¬[t]) ∨ ([s] ∧ [t]) ∨ (¬[s] ∧ [t])

reducing the case of arbitrary joins to that of disjoint joins. Hence meets distributive over joins in general. The other distributive law is a consequence of this, and we have that X^{∗} is a boolean algebra.

The fact that meets distribute over joins, together with the above observations on disjoint joins, has the following useful consequence:

3.5. Proposition. Let s_{i}: S_{i} → X, for i ∈ I, be a finite family of pairwise disjoint summands in X. The arrow (|_{i} s_{i}): ∑_{i∈I} S_{i} → X is a summand, and

[(|_{i} s_{i})] = ⋁_{i∈I}[s_{i}]

Proof. Use lemma 3.4, and proceed inductively using distributivity to show that the required joins are disjoint.

Given an arrow f: Y → X in X, the existence of pullbacks along summands in X allows us to obtain a map from the preorder of summands of X to the preorder of summands of Y by pullback with f. A routine argument using the properties of pullbacks shows that this map is order preserving. Further, since pullbacks of isomorphs are isomorphic, this map induces an order preserving map of posets f^{∗}: X^{∗} → Y^{∗}.

In fact, the arrow f^{∗} is a map of boolean algebras. Extensivity implies that pullbacks of sums are sums, thus the map f^{∗} preserves complements. Furthermore, routine arguments with pullbacks show that f^{∗} preserves meets. Since we can write a formula for joins in terms of meets and complements, the map f^{∗} preserves joins and is thus a boolean algebra map as claimed.

We thus obtain a functor –^{∗}: X^{op} → Bool, defined on objects by X ↦ X^{∗} and on arrows by f ↦ f^{∗}. Functoriality is an immediate consequence of the nature of pullbacks along identities and the fact that pullback squares compose. Further, it is a direct consequence of extensivity that this functor preserves products. One useful feature of this notion of inverse image is that it facilitates construction of arrows between summands of objects of an extensive category by “restriction”:

3.6. Proposition. Let f: X → Y in X. For summands s: S → X and t: T → Y, we have s ≤ f^{∗}t if and only if there exists g: S → T such that t · g = f · s. The arrow g is necessarily unique.

Proof. In the case s ≤ f^{∗}t, form the pullback defining f^{∗}t, and observe that we may compose the comparison arrow S → f^{∗}T (exhibiting s ≤ f^{∗}t) with the pullback projection f^{∗}T → T to produce a g with the required property. Now t, being a summand, is monic, so this g is unique. Conversely, given such g, form the pullback defining f^{∗}t. The arrows g and t provide the required data to obtain a comparison arrow exhibiting s ≤ f^{∗}t from the pullback property.

Functors in Ext map summands to summands and thus induce transformations of the summand posets. In fact, these transformations are boolean algebra maps. Before proving this, we present a lemma that may be interpreted as saying that functors which preserve sums are “the right morphisms” for Ext, as they preserve the relevant pullback structure automatically. We also observe a nice property of natural transformations between such functors. We note that part (i) appears as lemma 4.13 of [4], but for distributive extensive categories.

3.7. Lemma. Let X and Y be extensive categories.

(i) A functor F: X → Y in Ext preserves pullbacks along summands.

(ii) For a natural α: F → G in Ext, naturality squares at summands are pullbacks.

Proof. Let us be given a summand s: S → X, an arrow f: Y → X and a pullback of s along f. Take a complement ¬s: ¬S → X of s, and pull ¬s back along f to produce a sum decomposition of Y. Apply F to the pullback squares – since F preserves sums this yields a diagram

[figure: F f^{∗}S; F f^{∗}s; F Y; F f^{∗}¬s; F f^{∗}¬S; F S; F s; F X; F f; F ¬s; F ¬S]

with both top and bottom rows sums. By extensivity the squares are pullbacks, thus the pullback of s along f is preserved by F.

For a natural α: F → G and a summand s: S → X in X, consider the diagram

[figure: F S; F s; F X; F ¬s; F ¬S; GS; αS; Gs; GX; αX; G¬s; G¬S; α¬S]

The bottom and top rows are sum diagrams (since F and G preserve sums), and thus the squares are pullbacks by extensivity.

3.8. Construction. Consider a functor F: X → Y in Ext. For X ∈ X, defining maps F_{∗}X: X^{∗} → (F X)^{∗} by

F_{∗}X([s]) = [F s]

gives a family of boolean algebra maps natural in X.

Proof. The functor F preserves sums, hence F s is a summand in Y. Since functors preserve isomorphisms, we have a well-defined map X^{∗} → (F X)^{∗}. Applying F to comparison arrows shows that this map is order preserving.

Now F preserves the initial object, so F preserves the bottom element ⊥ ∈ X^{∗}. The binary meets of X^{∗} are formed by pulling back along summands, and such pullbacks are preserved by F, so F_{∗}X also preserves binary meets. Thus F_{∗}X preserves meets. The fact F preserves sums implies that F_{∗}X preserves the complements of X^{∗}, and the existence of a formula for the joins of X^{∗} in terms of complements and meets shows that F_{∗}X preserves joins, and is thus a boolean algebra map.

Naturality of F_{∗} at f: Y → X in X is the equality (F f)^{∗} · F_{∗}X = F_{∗}Y · f^{∗}. For any [s] ∈ X^{∗}, the pullback square defining f^{∗}s is preserved by F, and thus

[figure: F (f^{∗}S); F S; F Y; F (f^{∗}s); F f; F X; F s]

is a pullback. Pullbacks are unique up to an isomorphism commuting with the projections, and the claimed naturality follows.

4. A Notion of Image

In general, an extensive category X does not have enough structure to get a general notion of direct image; we can, however, produce a useful notion of direct image for certain specific arrows in an extensive category. The object of this section is to show that certain arrows (the “structural” arrows of the extensive category) have left adjoints to the inverse image maps described in section 3, and that these adjoints have nice objective descriptions in X.

In what follows, some of the definitions and basic results are phrased in terms of a composition and sum closed class of epics in X, with smaller classes yielding more restrictive notions. All the examples of interest in this paper are for the case where the class is that of split epics. However, in the interests of generality, the broader notion is presented as basic. It should be noted that the class of epics is not intended to be related to the factorization system used in section 2.

4.1. Notation. For this section, we fix an extensive category X and a composition and sum closed class of epics F in X.

By composition and sum closed, we mean that composites and sums of Fs are again Fs and that F contains all identities. The classes all epics, all strong epics, and all split epics are well known to be composition closed and it follows routinely from properties of sums that these classes are also closed under sums. The reader is referred to [8] for terminology and analysis of the various classes of monics and epics.

4.2. Definition. An arrow f: X → Y in X is said to admit clean F-images if, for any summand s: S → X, we have a commuting diagram

[figure: S; f|_{S}; f_{∗}S; X; s; f; Y; f_{∗}s]  (10)

such that f_{∗}s: f_{∗}S → Y is a summand, and f|_{S} ∈ F.

The term clean is chosen to emphasise the fact that we are only taking images of summands, which in some sense are the subobjects which sit cleanly within X. If F and F′ are composition closed classes of epics of X such that F ⊆ F′, then it is clear that any f that admits clean F-images also admits clean F′-images. In particular, we shall say f admits clean images to mean f admits clean F-images where F consists of all epics of X. If f admits clean F-images for any F then f admits clean images.

It is worth observing that to admit clean F-images is a very strong condition on a monic f – if f is either strongly monic or every element of F is strong, then diagram (10) with s = 1_{X} admits a diagonal fill-in which is easily seen to be invertible, and thus f is a summand (being isomorphic to the summand f_{∗}1_{X}). Another easy consequence of the definition is that for an arrow f: X → Y such that X is connected and f ∈ F, the arrow f admits clean F-images – the only summands of X are the initial object 0 and X itself, and one easily verifies that f_{∗}0 = 0 with f|_{0} = 1_{0}, and f_{∗}X = Y with f|_{X} = f.

Before continuing our analysis of this notion of image, we record some facts about summands of an extensive category – note the second two parts are applications of [8] to the first part of the lemma.

4.3. Lemma. If s: S → X is a summand in X, then

(i) The arrow s is a regular monic.

(ii) If s is epic, then s is invertible

(iii) A diagram

\overline{e ^{}}
........... w
[figure: S; s; X]

in which e is epic admits a diagonal fill-in w making both triangles commute.

Proof. For (i), consider the arrow f: X → X + X which is constructed from properties of sums by mapping S into the first summand, and the complement of S into the second summand. It is routine to check s is the equalizer of f and the first injection of the sum X + X, and thus s is regular.

Part (ii) is an immediate corollary of the fact such an s is both regular monic and epic. See for example propositions 3.1 and 3.3 of [8], and dualize. Part (iii) follows from the fact that regular monics are strong monics, that is to say, admit diagonal fill-ins from any epic (dualize proposition 3.1 of [8]).

4.4. Proposition. In the context of definition 4.2, the data defining the clean F-image is unique up to an isomorphism of f_{∗}S commuting with the data.

Proof. Given another commuting square of the form of diagram (10), say

[figure: S; g; T; X; s; f; Y; t]

with t a summand and g ∈ F, then since t and f_{∗}s are summands we may form the following pullback

[figure: U; v; f_{∗}S; T; w; t; Y; f_{∗}s]

in which v and w are summands. Now

t · g = f · s = f_{∗}s · f|_{S}

and the pullback property gives an arrow k: S → U such that v · k = f|_{S} and w · k = g. Thus the summands v and w are epic, since precomposing with k yields the epics f|_{S} and g. Hence v and w are isomorphisms by lemma 4.3(ii). It follows that v · w^{−1} is an isomorphism T ≅ f_{∗}S, and we calculate

f_{∗}s · v · w^{−1} = t · w · w^{−1} = t

and

v · w^{−1} · g = v · w^{−1} · w · k = v · k = f|_{S}

and thus the isomorphism respects the structure of the clean F-image.

4.5. Construction. For an arrow f: X → Y in X which admits clean images, defining f_{∗}[s] = [f_{∗}s] induces an order preserving map f_{∗}: X^{∗} → Y^{∗}.

Proof. Given summands s: S → X and t: T → X such that s ≤ t, we shall prove f_{∗}s ≤ f_{∗}t. Together with proposition 4.4, this suffices to show both that f_{∗} is well-defined and order preserving. Consider the diagram

S  [figure: f|_{S}] f_{∗}S
[figure: a; ........; b]
T [figure: f|_{T}] f_{∗}T
[figure: t; f_{∗}t]
[figure: X; s; f; Y; f_{∗}s]

showing the construction of f_{∗}s and f_{∗}t along with a comparison arrow a exhibiting s ≤ t. We wish to obtain the dotted arrow b such that f_{∗}t · b = f_{∗}s.

We note that

f_{∗}t · f|_{T} · a = f · t · a = f · s = f_{∗}s · f|_{S}

and use lemma 4.3(iii) to find a diagonal fill-in b for the square

S [figure: f|_{S}] f_{∗}S
.......... b
[figure: f_{∗}T; f|_{T} · a; f_{∗}t; Y; f_{∗}s]

such that the triangles commute. Commutativity of the lower right triangle shows that b is a comparison arrow exhibiting f_{∗}s ≤ f_{∗}t as required.

The following proposition may be considered the justification of the definition of clean image. We show that f_{∗} is a direct image, in the sense of being left adjoint to inverse image.

4.6. Proposition. If f: X → Y in X admits clean images, then f_{∗} ⊣ f^{∗}.

Proof. We need only produce the unit and counit – the triangular equations being automatic since X^{∗} and Y^{∗} are posets.

Given a summand s: S → X, construct f^{∗}f_{∗}s as shown:

S

[figure: s; f|_{S}; ..........]
f^{∗}f_{∗}S \overline{}f_{∗}S

[figure: X; f^{∗}f_{∗}s; f; Y; f_{∗}s]

Properties of pullbacks yield a comparison arrow S → f^{∗}f_{∗}S, and so s ≤ f^{∗}f_{∗}s. Thus [s] ≤ f^{∗}f_{∗}[s] for any [s] ∈ X^{∗}, and we have a unit as claimed.

Given a summand t: T → Y, construct f_{∗}f^{∗}t as shown:

f^{∗}T  [figure: f|_{f^{∗}T}] f_{∗}f^{∗}T
[figure: g]
T
[figure: t]
[figure: X; f^{∗}t; f; Y; f_{∗}f^{∗}t]

The map g is provided by the pullback defining f^{∗}t (this pullback being the lower-left part of the above square). We observe that

t · g = f · f^{∗}t = f_{∗}f^{∗}t · f|_{f^{∗}T}

and thus the diagonal fill-in property for the summand t provides an arrow a in the following square

f^{∗}T [figure: f|_{f^{∗}T}] f_{∗}f^{∗}T
.............. a
[figure: T; g; t; Y; f_{∗}f^{∗}t]

So a is a comparison arrow exhibiting f_{∗}f^{∗}t ≤ t, as required. Hence f_{∗}f^{∗}[t] ≤ [t] for any [t] ∈ Y^{∗}, and we have the required counit.

Thus we have the adjunction as claimed.

As a consequence of this adjunction, we record the corollary:

4.7. Corollary. If f: X → Y in X admits clean images, then f_{∗} preserves joins.

We now provide ourselves with a reasonable supply of arrows admitting clean images in X. We shall use the term clean split-image for a clean F-image in the case F consists of all split epics in the category under consideration.

4.8. Proposition.

(i) Any summand s: S → X admits clean F-images, and for any summand t of S, we have s_{∗}[t] = [st].

(ii) Any codiagonal ∇: X + X → X admits clean split-images, and for any two summands t and u of X, we have ∇_{∗}[t + u] = [t] ∨ [u].

Proof. For case (i), consider a summand t: T → S. The definitions

s_{∗}T = T s_{∗}t = s · t s|_{T} = 1_{T}

provide the data for a clean split-image, since composites of summands are summands and F contains all identities. The required diagram is immediate.

For case (ii), consider a summand s: S → X + X. By extensivity, we have that s = t + u for summands t: T → X and u: U → X. Now ∇ · (t + u) = (t | u), and we factor (t | u) = (t ∨ u) · e_{t,u} using lemma 3.3, where e_{t,u} is split epic. The definitions

∇_{∗}S = T ∨ U ∇_{∗}s = t ∨ u ∇|_{S} = e_{t,u}

provide the data for a clean split-image. The required diagram commutes by the following calculation:

∇_{∗}s · ∇|_{S} = (t ∨ u) · e_{t,u} = (t | u) = ∇ · (t + u) = ∇ · s

4.9. Proposition. Let X be an extensive category, and F be a composition and sum closed family of epics of X, then

(i) Given arrows f: X → Y and g: Y → Z of X admitting clean F-images, the composite g · f admits clean F-images, and for any summand s of X, we have (g · f)_{∗}[s] = g_{∗}f_{∗}[s].

(ii) Given arrows f: X → Y and g: Z → W of X admitting clean F-images, the sum f + g: X + Z → Y + W admits clean F-images, and for any summands t of X and u of Z, we have ∇_{∗}[t + u] = f_{∗}[t] + g_{∗}[u].

(iii) Given an arrow f: X → Y admitting clean F-images, the pullback of f along a summand admits clean F-images.

Proof. For case (i), consider a summand s: S → X of X, and define

(g · f)_{∗}S = g_{∗}(f_{∗}S) (g · f)_{∗}s = g_{∗}(f_{∗}s) (g · f)|_{S} = g|_{g_{∗}S} · f|_{S}

This yields the data required for a clean F-image, since composites of Fs are Fs. The required diagram is obtained by pasting those for f_{∗}s and g_{∗}(f_{∗}s).

For case (ii), consider a summand s: S → X + Z – by extensivity we have s = t + u for summands t: T → X and u: U → Y. Defining

(f + g)_{∗}S = f_{∗}T + g_{∗}U (f + g)_{∗}s = f_{∗}t + g_{∗}u (f + g)|_{S} = f|_{T} + g|_{U}

gives the data for a clean F-image, since sums of summands are summands and sums of Fs are Fs. The required diagram is the sum of those for f_{∗}t and g_{∗}u.

For case (iii), consider a summand s: S → Y and a pullback g: f^{∗}S → S of f along s. Given a summand t: T → f^{∗}S, consider the diagram

[figure: T; t; f^{∗}S; f^{∗}s; X; S; g; ........; a; s; f_{∗}T; f|_{T}; f_{∗}(f^{∗}s · t); Y; f]  (11)

formed by finding the clean F-image of f^{∗}s · t under f, noting f^{∗}s · t is a composite of summands and hence a summand.

We now produce the comparison arrow a shown dotted on diagram (11). Observe that f^{∗}s · t ≤ f^{∗}s as summands of Y (the arrow t being the comparison), and thus by proposition 4.6, we have f_{∗}(f^{∗}s · t) ≤ s. The data

g_{∗}T = f_{∗}T g_{∗}t = a g|_{T} = f|_{T}

gives the data for a clean F-image, since a is a summand by lemma 3.2. The required diagram is the left trapezoid in diagram (11).

Observe that the formulas given for codiagonals and sums cover all summands by extensivity, as noted in the proof. Further, the previous two propositions imply that, in the case F contains all split epics, the subcategory of an extensive category with objects all objects and arrows those admitting clean F-images is an extensive category in its own right, for universal arrows from sums can be constructed using sums, composites and the codiagonal, and we have the required pullbacks.

We now address the question of the extent to which the sums of an extensive category are disjoint joins. For X ∈ X, the connection between joins of X^{∗} and clean images is given by proposition 4.8(ii) – joins are precisely clean split-images along a codiagonal. Given summands s and t of X, we note

(s | t) = ∇ · (s + t)

and apply propositions 4.8 and 4.9 to obtain

(s | t)_{∗}[⊤] = [s] ∨ [t]

More generally, for a finite family of summands s_{i} (for i ∈ I), we have

(|_{i} s_{i})_{∗}[⊤] = ⋁_{i∈I}[s_{i}]

4.10. Proposition. Consider a finite family of summands s_{i}: S_{i} → X (for i ∈ I) in X. If the s_{i} are pairwise disjoint and ⋁_{i}[s_{i}] = ⊤, then the family s_{i} is a sum decomposition of X.

Proof. Applying propositions 4.8 and 4.9, we see that (|_{i} s_{i}) admits clean split-images. Now

(|_{i} s_{i})_{∗}[⊤] = ⋁_{i}[s_{i}] = ⊤

and examining the square defining clean split-images we see that (|_{i} s_{i}) is isomorphic to a split epic, and hence split epic. By proposition 3.5, the arrow (|_{i} s_{i}) is also a summand, and hence monic. Thus (|_{i} s_{i}) is invertible, from which it follows that the s_{i} are the injections of a sum.

In the next section we shall use this result to show invertibility of arrows where actual construction of the inverse is difficult or overly complicated. Since the condition of this theorem is stated in terms of meets and joins, we have the full machinery of boolean algebra to assist us, together with the image adjunction give by proposition 4.6. We conclude this section with a lemma on clean images of complements under summands.

4.11. Lemma. Given summands s: S → X and t: T → S in X, we have

s_{∗}(¬[t]) = [s] ∧ ¬(s_{∗}[t])

Proof. By associativity of sums, we have the disjoint union

[s · t] ∨ [s · ¬t] ∨ ¬[s] = ⊤

Hence [s·¬t] = ¬([s·t]∨¬[s]). Now [s·¬t] = s_{∗}(¬[t]) and [s·t] = s_{∗}[t] by proposition 4.8(i), and so

s_{∗}(¬[t]) = [s · ¬t] = ¬([s · t] ∨ ¬[s]) = [s] ∧ ¬(s_{∗}[t])

as claimed.

5. Stirling Polynomials are Generic Separables

We now turn to the universal property of the category of Stirling polynomials SP(A) described in section 2. For a category of Stirling exponents A, what universal property do we expect SP(A) to possess? That is to say, given an extensive category X and a functor H: P(A) → X in Ext, when do we expect a factorization

[figure: P(A); S; SP(A); H; X; . . . . . . . . .; F]  (12)

through the functor S of construction 2.9 ? More precisely, can we identify the image of precomposition by S as a subcategory of Ext[P(A), X] ?

Given e: B → A in E, we have seen in proposition 2.10 that SX^{e} is a summand. Moreover, given a pushout along e in A, it is routine to check that this yields a pullback in P(A). Since S preserves limits by corollary 2.15, we obtain a pullback diagram in SP(A) after applying S. Since functors in Ext map summands to summands, and, by lemma 3.7, preserve pullbacks along summands, we see that a composite F S must also map X^{[e]} to a summand, and preserve pullbacks along arrows of the form X^{[e]} in P(A). For a natural transformation α: F → G between functors F and G: SP(A) → X in Ext, lemma 3.7 implies that a naturality square of α at a summand is a pullback. Thus the naturality square of αS at X^{e} is a pullback square.

Considering these restrictions on the functors and natural transformation arising by precomposition with S, and comparing them to the result of proposition 1.1 which motivated the generalization, it seems reasonable to make the following definition:

5.1. Definition. Given a category of Stirling exponents (A, E, M) and an extensive category X,

(AS1) a functor H: P(A) → X in Ext is A-separable if, for all e ∈ E, the arrow HX^{e} is a summand and H preserves pullbacks along X^{e}.

(AS2) a natural transformation γ: H → K between A-separable functors H and K is A-separable if, for all e ∈ E, the naturality square at X^{e} is a pullback square.

The subcategory of Ext[P(A), X] with objects the A-separable functors and arrows the A-separable natural transformations is denoted A-Sep(X).

Note that since pullback squares compose, it is immediate that the composite of A-separable natural transformations is again A-separable, and thus we indeed obtain a subcategory A-Sep(X) of Ext[P(A), X].

5.2. Notation. For this section, we fix a category of Stirling exponents (A, E, M) and an extensive category X. The functor S is that of construction 2.9, and U denotes the inclusion SP(A) → P(A).

5.3. Proposition. The functor S induces a functor Ext[SP(A), X] → A-Sep(X) by precomposition.

Proof. This is precisely the content of the discussion motivating definition 5.1.

We now turn to factorizing A-separable functors and natural transformations through the functor S. The main result we are aiming for is that a factorization as in diagram (12) exists precisely when H is A-separable, and moreover that this factorization leads to an equivalence between A-Sep(X) and Ext[SP(A), X].

Given an A-separable functor H: P(A) → X, we now describe the lifting of H to a functor \overline{H}: SP(A) → X in Ext such that \overline{H}S ≅ H. It shall transpire in what follows that \overline{H}X^{[A]} is a summand of HX^{A}. We begin by identifying these summands:

5.4. Construction. Consider an A-separable functor H: P(A) → X. For each A ∈ A, write Quo_{E}(A) = (A_{i}, a_{i}, I, i_{∗}) and I^{∗} = I \ {i_{∗}}. Construct a summand

ϕ_{H}X^{[A]}: \overline{H}X^{[A]} ^{}HX^{A}

such that

[ϕ_{H}X^{[A]}] = ¬ ⋁_{i∈I^{∗}}[HX^{a_{i}}]  (13)

in (HX^{A})^{∗}. The summand ϕ_{H}X^{[A]} is termed the distinct A-tuples of H.

Proof. Each HX^{a_{i}} is a summand, since a_{i} is an E and H is A-separable. So we have a well defined element of (HX^{A})^{∗}, and we take any representative for the result of the construction.

To be precise, one should consider the symbols ϕ_{H}X^{[A]} and \overline{H}X^{[A]} in this definition indivisible, but it will of course transpire that we can lift \overline{H} to a functor and ϕ_{H} to a natural transformation. Informally, justifying our choice of language for this definition, we are locating the distinct A-tuples by complementing the join of all the A-tuples with duplicated entries.

5.5. Lemma. Consider an A-separable functor H: P(A) → X. If m: B → A is an M, then

[ϕ_{H}X^{[A]}] ≤ (HX^{m})^{∗}[ϕ_{H}X^{[B]}]

Proof. Write Quo_{E}(B) = (B_{j}, b_{j}, J, j_{∗}) and J^{∗} = J \ {j_{∗}}, and observe

(HX^{m})^{∗}(¬ ⋁_{j∈J^{∗}}[HX^{b_{j}}]) = ¬ ⋁_{j∈J^{∗}}(HX^{m})^{∗}[HX^{b_{j}}]

since inverse image maps are maps of boolean algebras. Now ¬[s] ≤ ¬[t] if and only if [t] ≤ [s], so it suffices to show

⋁_{j∈J^{∗}}(HX^{m})^{∗}[HX^{b_{j}}] ≤ ⋁_{i∈I^{∗}}[HX^{a_{i}}]  (14)

To show this, we shall show that each term in the left hand join is at most some term in the right hand join. Given j ∈ J^{∗} then, push m out along b_{j} in A, since A admits pushouts along Es. Since pushouts of Es are Es (proposition 2.1.1(b) of [5]), we may assume that this pushout has the form

[figure: B; m; A; B_{j}; b_{j}; f; A_{i}; a_{i}]

for some i ∈ I. Observe that if a_{i} is invertible, then f · b_{j} = a_{i} · m is an M. Thus b_{j} is invertible by lemma 2.2(ii), contrary to j ∈ J^{∗}. We deduce that i ∈ I^{∗}, and the A-separability of H gives a pullback

HX^{A} \overline{HX^{m}_{}}HX^{B}

[figure: HX^{A_{i}}; HX^{a_{i}}; HX^{f}; HX^{B_{j}}; HX^{b_{j}}]

Hence (HX^{m})^{∗}[HX^{b_{j}}] = [HX^{a_{i}}] in (HX^{A})^{∗}. In particular (HX^{m})^{∗}[HX^{b_{j}}] is at most [HX^{a_{i}}], and equation (14) follows.

Given this inequality, we can define \overline{H} on arrows between Stirling monomials by restriction:

5.6. Construction. Consider an A-separable functor H: P(A) → X. For m: B → A an M, we construct \overline{H}X^{[m]}: \overline{H}X^{[A]} → \overline{H}X^{[B]} as the unique arrow making commutative:

\overline{H}X^{[A]} \overline{ϕX^{[A]}_{}}HX^{A}

[figure: \overline{H}X^{[B]}; \overline{H}X^{[m]}; ϕX^{[B]}; HX^{B}; HX^{m}]

(15)

Proof. Use lemma 5.5 and proposition 3.6.

Constructions 5.4 and 5.6 together yield:

5.7. Construction. Given an A-separable functor H: P(A) → X, we have:

(i) a functor \overline{H}: SP(A) → X in Ext consistent with constructions 5.4 and 5.6.

(ii) a natural transformation ϕ_{H}: \overline{H} → HU whose component at X^{[A]} is the distinct A-tuples of H for each A ∈ A. Moreover, every component of ϕ_{H} is a summand.

Proof. We construct \overline{H} by lifting the relevant data using the universal property of the category of families SP(A). The necessary functoriality of the data follows from the fact that \overline{H}X^{[m]} is unique in diagram (15). For ϕ_{H}, lift the data given for Stirling monomials, noting diagram (15) gives the required naturality. Since the components of ϕ_{H} in general are given by sums of components at Stirling monomials and sums of summands are summands, we see that every component of ϕ_{H} is a summand.

The construction \overline{(–)} gives the data on objects for the functor which is equivalence inverse to precomposition with S. Our next goal is to lift this construction to A-separable natural transformations.

5.8. Lemma. Consider an A-separable natural transformation γ: H → K and A ∈ A. We have

[ϕ_{H}X^{[A]}] ≤ (γX^{A})^{∗}[ϕ_{K}X^{[A]}]

Proof. Write Quo_{E}(A) = (A_{i}, a_{i}, I, i_{∗}) and I^{∗} = I \ {i_{∗}}. For each i ∈ I, since γ is A-separable we obtain a pullback

HX^{A_{i}} \overline{HX^{a_{i}}_{}}HX^{A}

[figure: KX^{A_{i}}; γX^{A_{i}}; KX^{a_{i}}; KX^{A}; γX^{A}]

So [HX^{a_{i}}] = (γX^{A})^{∗}[KX^{a_{i}}], and it follows that

(γX^{A})^{∗}¬( ⋁_{i∈I^{∗}}[KX^{a_{i}}]) = ¬(γX^{A})^{∗}( ⋁_{i∈I^{∗}}[KX^{a_{i}}])
= ¬ ⋁_{i∈I^{∗}}(γX^{A})^{∗}[KX^{a_{i}}]
= ¬ ⋁_{i∈I^{∗}}[HX^{a_{i}}]

Thus (γX^{A})^{∗}[ϕ_{K}X^{[A]}] = [ϕ_{H}X^{[A]}], and hence the required inequality.

It is interesting to note that the proposition actually gives a stronger result. One can check if γ is a mere natural transformation (not known to be A-separable), then the inequality given by the naturality square is the reverse of the inequality we are seeking.

5.9. Construction. Consider an A-separable natural transformation γ: H → K. We construct a natural transformation \overline{γ}: \overline{H} → \overline{K} unique such that

\overline{H}X^{[A]} \overline{ϕ_{H}X^{[A]}_{}}HX^{A}

[figure: \overline{K}X^{[A]}; \overline{γ}X^{[A]}; ϕ_{K}X^{[A]}; KX^{A}; γX^{A}]

(16)

commutes for each A ∈ A, where \overline{H} and \overline{K} are as in construction 5.7(i).

Proof. Using lemma 5.8 and proposition 3.6, we can produce components of \overline{γ} at Stirling monomials X^{[A]} for each A ∈ A, and then lift via the universal property of families. It suffices to check naturality of \overline{γ} at X^{[m]} for m: B → A an M. Consider the following diagram:

\overline{H}X^{[A]}  \overline{\overline{H}X^{[m]}  ^{}}\overline{H}X^{[B]}
[figure: ϕ_{H}X^{[A]}; ϕ_{H}X^{[B]}]
HX^{A}  \overline{HX^{m}  ^{}}\overline{γ}X^{[B]}  HX^{B}

[figure: \overline{K}X^{[A]}; \overline{γ}X^{[A]}; \overline{K}X^{[m]}; \overline{K}X^{[B]}]
[figure: ϕ_{K}X^{[A]}; ϕ_{K}X^{[B]}]
[figure: KX^{A}; γX^{A}; KX^{m}; KX^{B}; γX^{B}]

The left (resp. right) face is the definition of \overline{γ} at X^{[A]} (resp. X^{[B]}). The top (resp. bottom) face is the naturality of ϕ_{H} (resp. ϕ_{K}) at X^{[m]}. The front face is naturality of γ at X^{m}. Thus we may deduce that the back face (the required naturality of \overline{γ} at X^{[m]}) commutes when postcomposed with ϕ_{K}X^{[B]}. But ϕ_{K}X^{[B]} is a summand, and hence monic, and thus the back face commutes giving the required naturality.

We now have all the data required to construct the functor which the the equivalence inverse to precomposition with S.

5.10. Construction. There is a functor \overline{(–)}: A-Sep(X) → Ext[SP(A), X] consistent with constructions 5.7 and 5.9.

Proof. The only remaining validation is functoriality of \overline{(–)} – this follows from uniqueness of \overline{γ}X^{[A]} in diagram (16) and by pasting such diagrams together. Preservation of identities is likewise routine.

Having described the functor which is the equivalence inverse to precomposing S, we now turn to a proof of this equivalence. While the proof requires a few technical lemmas, the method of proof is by no means difficult. We simply describe the two required natural isomorphisms – \overline{H}S ≅ H natural in H and \overline{F S} ≅ F natural in F. The required invertibility in each case is shown by using equality in the boolean algebra of summands.

We first show that \overline{H}S ≅ H natural in H for each A-separable H. We shall show that the natural transformation Hϵ · ϕ_{H}S: \overline{H}S → H is invertible, where ϵ is the counit of U ⊣ S. Informally, the next two lemmas describe the fact that any A-tuple of H is obtained uniquely by duplicating entries of a distinct A_{i}-tuple of H for some a_{i}: A → A_{i}.

5.11. Lemma. Consider an A-separable functor H: P(A) → X. For each A ∈ A, writing Quo_{E}(A) = (A_{i}, a_{i}, I, i_{∗}), the family of summands

HX^{a_{i}} · ϕ_{H}X^{[A_{i}]}

of HX^{A} for i ∈ I is pairwise disjoint.

Proof. We note firstly this is indeed a family of summands, as each arrow is a composite of summands. For each i ∈ I, let us write Quo_{E}(A_{i}) = (B_{j}^{i}, b_{j}^{i}, J_{i}, j_{∗}^{i}) and J_{i}^{∗} = J_{i} \ {j_{∗}^{i}}.

Take distinct i_{1}, i_{2} ∈ I, and form a pushout of a_{i_{1}} and a_{i_{2}} in A, noting that A admits pushouts along Es. Since pushouts of Es are Es and Quo_{E}(A), Quo_{E}(A_{i_{1}}) and Quo_{E}(A_{i_{2}}) are complete sets of representatives, we may assume that we have a commuting diagram

[figure: A; a_{i_{1}}; A_{i_{1}}; a_{i}; b_{j_{1}}^{i_{1}}; A_{i_{2}}; a_{i_{2}}; A_{i}; ≅; B_{j_{1}}^{i_{1}}; b_{j_{2}}^{i_{2}}; B_{j_{2}}^{i_{2}}; ≅]  (17)

in A, where j_{1} ∈ J_{i_{1}}, j_{2} ∈ J_{i_{2}}, and the square is a pushout. The unlabelled arrows are unique (since Es are epic), and we shall leave them unnamed.

Observe that at least one of b_{j_{1}}^{i_{1}} and b_{j_{2}}^{i_{2}} is not invertible – if both were invertible then a_{i_{1}} and a_{i_{2}} would be isomorphic as E-quotients of A, and thus i_{1} = i_{2} contrary to the fact they are distinct. That is to say, either j_{1} ∈ J_{i_{1}}^{∗} or j_{2} ∈ J_{i_{2}}^{∗}.

Since HX^{a_{i_{1}}} is a summand, it admits clean split-images, and these are formed by composition. Thus we may compute

[HX^{a_{i_{1}}} · ϕ_{H}X^{[A_{i_{1}}]}] = (HX^{a_{i_{1}}})_{∗}(¬ ⋁_{j∈J_{i_{1}}^{∗}}[HX^{b_{j}^{i_{1}}}])
= [HX^{a_{i_{1}}}] ∧ (¬(HX^{a_{i_{1}}})_{∗}( ⋁_{j∈J_{i}^{∗}}[HX^{b_{j}^{i_{1}}}]))
= [HX^{a_{i_{1}}}] ∧ ¬( ⋁_{j∈J_{i}^{∗}} (HX^{a_{i_{1}}})_{∗}[HX^{b_{j}^{i_{1}}}])
= [HX^{a_{i_{1}}}] ∧ ⋀_{j∈J_{i}^{∗}} ¬[HX^{a_{i_{1}}} · HX^{b_{j}^{i_{1}}}]
= [HX^{a_{i_{1}}}] ∧ ⋀_{j∈J_{i}^{∗}} ¬[HX^{b_{j}^{i_{1}}·a_{i_{1}}}]

where we have applied lemma 4.11 to compute the direct image of a complement under a summand, and used the fact that direct images preserve joins by corollary 4.7. Similarly, we obtain:

[HX^{a_{i_{2}}} · ϕ_{H}X^{[A_{i_{2}}]}] = [HX^{a_{i_{2}}}] ∧ ⋀_{j∈J_{i}^{∗}} ¬[HX^{b_{j}^{i_{2}}·a_{i_{2}}}]

Since H is A-separable, the pushout formed in diagram (17) yields a pullback in X, and thus we have [HX^{a_{i_{1}}}] ∧ [HX^{a_{i_{2}}}] = [HX^{a_{i}}]. We deduce that

[HX^{a_{i_{1}}} · ϕ_{H}X^{[A_{i_{1}}]}] ∧ [HX^{a_{i_{2}}} · ϕ_{H}X^{[A_{i_{2}}]}]

= [HX^{a_{i_{1}}}] ∧ ( ⋀_{j∈J_{i}^{∗}} ¬[HX^{b_{j}^{i_{1}}·a_{i_{1}}}]) ∧ [HX^{a_{i_{2}}}] ∧ ( ⋀_{j∈J_{i}^{∗}} ¬[HX^{b_{j}^{i_{2}}·a_{i_{2}}}])

= [HX^{a_{i}}] ∧ ( ⋀_{j∈J_{i}^{∗}} ¬[HX^{b_{j}^{i_{1}}·a_{i_{1}}}]) ∧ ( ⋀_{j∈J_{i}^{∗}} ¬[HX^{b_{j}^{i_{2}}·a_{i_{2}}}])

Since j_{1} ∈ J_{i_{1}}^{∗} or j_{2} ∈ J_{i_{2}}^{∗}, at least one of the terms ¬[HX^{b_{j_{1}}^{i_{1}}·a_{i_{1}}}] or ¬[HX^{b_{j_{2}}^{i_{2}}·a_{i_{2}}}] appears in one of the familial meets in the preceding calculation. The isomorphisms in diagram (17) show that each of these terms is equal to ¬[HX^{a_{i}}]. Thus the above meet is contained in [HX^{a_{i}}] ∧ ¬[HX^{a_{i}}] = ⊥, and we have the claimed disjointness.

5.12. Lemma. In the context of lemma 5.11, we have

⋁_{i∈I}[HX^{a_{i}} · ϕ_{H}X^{[A_{i}]}] = ⊤

Proof. We proceed by induction of the size of Quo_{E}(I), noting this is finite by property (3) of definition (2.1).

Suppose that #Quo_{E}(I) = 1; then Quo_{E}(I) has a unique element i_{∗}, and recall that A_{i_{∗}} = A and a_{i_{∗}} = 1_{A}. Also, in this case, I^{∗} is empty. Thus

⋁_{i∈I}[HX^{a_{i}} · ϕ_{H}X^{[A_{i}]}] = [HX^{1_{A}} · ϕ_{H}X^{[A]}] = ¬ ⋁_{i∈I^{∗}}[HX^{a_{i}}] = ¬⊥ = ⊤

as claimed.

Suppose that #Quo_{E}(I) > 1. We compute

⋁_{i∈I}[HX^{a_{i}} · ϕ_{H}X^{[A_{i}]}] = [HX^{a_{i∗}} · ϕ_{H}X^{[A_{i∗}]}] ∨ ( ⋁_{i∈I^{∗}}[HX^{a_{i}} · ϕ_{H}X^{[A_{i}]}])
= [ϕ_{H}X^{[A]}] ∨ ( ⋁_{i∈I^{∗}}[HX^{a_{i}} · ϕ_{H}X^{[A_{i}]}])
= (¬ ⋁_{i∈I^{∗}}[HX^{a_{i}}]) ∨ ( ⋁_{i∈I^{∗}}[HX^{a_{i}} · ϕ_{H}X^{[A_{i}]}])

To show that this equals ⊤, it suffices to show that for each i_{1} ∈ I^{∗} we have

[HX^{a_{i_{1}}}] ≤ ⋁_{i∈I^{∗}}[HX^{a_{i}} · ϕ_{H}X^{[A_{i}]}]  (18)

For each i ∈ I, write Quo_{E}(A_{i}) = (B_{j}^{i}, b_{j}^{i}, J_{i}, j_{∗}^{i}) and J_{i}^{∗} = J_{i} \ {j_{∗}^{i}}. Inductively then,

⋁_{j∈J_{i_{1}}^{∗}}[HX^{b_{j}^{i_{1}}} · ϕ_{H}X^{[B_{j}^{i_{1}}]}] = ⊤

in (HX^{A_{i_{1}}})^{∗}, and taking direct images by HX^{a_{i_{1}}}, we have

[HX^{a_{i_{1}}}] = (HX^{a_{i_{1}}})_{∗}( ⋁_{j∈J_{i_{1}}^{∗}}[HX^{b_{j}^{i_{1}}} · ϕ_{H}X^{[B_{j}^{i_{1}}]}])
= ⋁_{j∈J_{i_{1}}^{∗}} (HX^{a_{i_{1}}})_{∗}(HX^{b_{j}^{i_{1}}})_{∗}[ϕ_{H}X^{[B_{j}^{i_{1}}]}]
= ⋁_{j∈J_{i_{1}}^{∗}} (HX^{b_{j}^{i_{1}}·a_{i_{1}}})_{∗}[ϕ_{H}X^{[B_{j}^{i_{1}}]}]

using the formula of proposition 4.9(i) to compute the composed direct images. Now, for each j ∈ J_{i_{1}}^{∗}, since b_{j}^{i_{1}} · a_{i_{1}} is an E, it is isomorphic as an E-quotient to a_{k} for some k ∈ I. Moreover, the arrow a_{k} cannot be invertible – this would imply b_{j}^{i_{1}} · a_{i_{1}} is invertible and hence an M, and thus a_{i_{1}} invertible by lemma 2.2(ii), which contradicts i_{1} ∈ I^{∗}. Hence k ∈ I^{∗}, and each term in the above join decomposition of [HX^{a_{i_{1}}}] appears as a term (HX^{a_{k}})_{∗}[ϕ_{H}X^{[A_{k}]}] in the right hand side of equation (18). The result follows.

We are now in a position to prove the claimed isomorphism \overline{H}S ≅ H.

5.13. Proposition. Consider an A-separable functor H: P(A) → X. With ϵ the counit of U ⊣ S (construction 2.13), the natural transformation Hϵ·ϕ_{H}S: \overline{H}S → H is invertible.

Proof. To show that Hϵ·ϕ_{H}S is invertible it suffices to check invertibility of the component at X^{A} for each A ∈ A. We have

HϵX^{A} · ϕ_{H}SX^{A} = (|_{i} HX^{a_{i}}) · ∑_{i∈I} ϕ_{H}X^{[A_{i}]} = (|_{i} HX^{a_{i}} · ϕ_{H}X^{[A_{i}]})  (19)

and thus this arrow is produced using the universal property of sums from a family of summands HX^{a_{i}} · ϕ_{H}X^{[A_{i}]}. To show that this is invertible, we apply proposition 4.10, the required conditions being the content of lemmas 5.11 and 5.12, to deduce that this family of summands is a sum decomposition of HX^{A}. It follows that the component HϵX^{A}·ϕ_{H}SX^{A} is invertible, and hence the result.

At this point, we have shown that for each A-separable functor H, the natural transformation Hϵ·ϕ_{H}S is invertible. It remains to show that this isomorphism is natural in H – this is a consequence of the 2-categorical structure of Cat, on noting that diagram (16) shows that the family of natural transformations ϕ is natural in H.

We now show that \overline{F S} ≅ F natural in F for each F: SP(A) → X. We shall use the natural family of boolean algebra maps obtained from F using construction 3.8. We begin with a lemma giving naturality of families of comparison arrows constructed from natural transformations.

5.14. Lemma. Consider functors F, G, and H: X → Y and natural transformations α: F → H and β: G → H in Ext. If each component of both α and β is a summand, and for each X ∈ X

[αX] ≤ [βX]  (20)

then there is a natural transformation γ: F → G such that β ·γ = α. Moreover, if equality holds for all X in equation (20), then γ is invertible.

Proof. The components of γ are the comparison arrows F X → GX exhibiting equation (20). To see that γ so defined is natural at f: X → Y in X, consider the diagram:

F X  \overline{γX ^{}}GX
[figure: αX; βX]
HX

[figure: F Y; F f; γY; Hf; GY; Gf]
[figure: αY; βY]
HY^{}

The square is the desired naturality – the parallelograms commute by naturality of α and β, and the triangles commute by construction of γ. This gives commutativity of the square postcomposed with βX. Since βX is a summand, it is monic, and hence the desired naturality. With equality in equation (20), each component of γ is invertible, and hence γ is invertible.

We shall use this lemma to construct the isomorphism \overline{F S} ≅ F. The desired summand equality is the image under F of the summand equality in SP(A) given by the following lemma.

5.15. Lemma. For each A ∈ A, writing Quo_{E}(A) = (A_{i}, a_{i}, I, i_{∗})we have

¬ ⋁_{i∈I^{∗}}[SX^{a_{i}}] = [inj_{i_{∗}}]  (21)

in the boolean algebra (SX^{A})^{∗}.

Proof. Sums in a category of families, such as SP(A), are formed by by disjoint unions of families. Thus to give a summand of an object of SP(A) is just to give a subset of the Stirling monomials comprising the object, and complementation of summands is just complementation of the subset of monomials comprising the summand.

With this in mind, let us examine the subset of monomials describing the left hand side of equation (21), which we endeavour to show consists solely of X^{[A]}. Note that this summand of SX^{[A]} is indexed by the distinguished i_{∗} ∈ I, and is thus the right hand side of equation (21).

Consider the join of summands appearing in this equation, and note that for any i ∈ I^{∗}, writing Quo_{E}(A_{i}) = (B_{j}^{i}, b_{j}^{i}, J_{i}, j_{∗}^{i}), so B_{j_{∗}}^{i} = A_{i}, we have commutativity of

X^{[A_{i}]} \overline{inj_{j_{∗}}_{}}SX^{A_{i}}

[figure: X^{[A_{i}]}; X^{[1_{A_{i}}]}; inj_{i}; SX^{A}; SX^{a_{i}}]

from diagram (4), the definition of S on arrows, since

b_{j_{∗}}^{i} · a_{i} = 1_{B_{j∗}^{i}} · a_{i} = 1_{A_{i}} · a_{i}

is the unique factorization of the left hand term with 1_{A_{i}} an M. Collapsing the left hand side identity, we see that inj_{i} ≤ SX^{A_{i}}, and hence X^{[A_{i}]} occurs in the subset of monomials making up the join on the left hand side of equation (21).

It remains to consider the monomial X^{[A]}, corresponding to i_{∗} ∈ I. Suppose by way of contradiction this were included in the subset of monomials representing the join. Since monomials are atomic in the boolean algebra of summands of SX^{A}, there is some i ∈ I^{∗} for which inj_{i_{∗}} ≤ SX^{a_{i}}. Consider the monomials of SX^{A} comprising the summand SX^{a_{i}}. Writing Quo_{E}(A_{i}) = (B_{j}^{i}, b_{j}^{i}, J_{i}, j_{∗}^{i}), the definition of S on arrows show that SX^{a_{i}} maps the summand X^{[B_{j}^{i}]} to the summand X^{[A_{k}]} of SX^{A}, where b_{j}^{i} · a_{i} = m · a_{k} is the unique factorization for some k ∈ I and m an M. To obtain the monomial X^{[A]}, we would require k = i_{∗}, and thus a_{k} an identity. Thus b_{j}^{i} · a_{i} = m is an M. By lemma 2.2(ii), we would have that a_{i} is invertible, contrary to i ∈ I^{∗}.

Thus we see that the subset of monomials of SX^{A} making up the join appearing on the left hand side of equation (21) is precisely all monomials except X^{[A]}. It follows that the complement is precisely the monomial X^{[A]}, which is the result of the lemma. 5.16. Lemma. Consider a functor F: SP(A) → X in Ext. With η the unit of U ⊣ S (construction 2.12), for each A ∈ A we have

[ϕ_{F S}X^{[A]}] = [F ηX^{[A]}]

Proof. We note that we may consider the distinct A-tuples of F S, as this functor is A-separable by proposition 5.3. Using the natural transformation F_{∗} of construction 3.8, and writing Quo_{E}(A) = (A_{i}, a_{i}, I, i_{∗}), we observe that

[ϕ_{F} SX^{[A]}] = ¬ ⋁_{i∈I^{∗}}[F SX^{a_{i}}] = ¬ ⋁_{i∈I^{∗}}(F_{∗}SX^{A})[SX^{a_{i}}] = (F_{∗}SX^{A})(¬ ⋁_{i∈I^{∗}}[SX^{a_{i}}])

using the fact that the components of F_{∗} are boolean algebra maps. We also have

[F ηX^{[A]}] = (F_{∗}SX^{A})[ηX^{[A]}] = (F_{∗}SX^{A})[inj_{i_{∗}}]

The lemma follows by applying (F_{∗}SX^{A}) to the result of lemma 5.15.

The desired natural isomorphism now follows:

5.17. Proposition. Consider a functor F: SP(A) → X in Ext. There is a natural isomorphism \overline{F S} ≅ F. Moreover, the collection of these transformations as F varies is natural in F.

Proof. We may apply lemma 5.14 to the result of lemma 5.16 to produce the required natural isomorphism from the comparison arrows of the summand equality of the latter lemma. Since we have equality in lemma 5.16, we indeed obtain a natural isomorphism \overline{F S} ≅ F.

It remains to show that this isomorphism \overline{F S} ≅ F is natural in F. Given a natural transformation α: F → G for another G: SP(A) → X in Ext, we have the diagram:

\overline{F S}  \overline{≅  ^{}}F
[figure: ϕ_{F S}; F η]
F SU

[figure: \overline{GS}; \overline{αS}; ≅; αSU; G; α]
[figure: ϕ_{GS}; Gη]
GSU^{}

and wish to show commutativity of the square (the isomorphisms being those produced by lemma 5.14). Each triangle commutes by the result of the lemma. The left parallelogram is an instance of diagram (16), and 2-categorical properties of Cat give the right parallelogram. A diagram chase gives the desired commutativity postcomposed with Gη. Now G preserves summands, and every component of η is a summand, thus every component of Gη is a summand. Since summands are monic in the extensive category X, we have the desired commutativity.

Thus we have a proof of the claimed universal property of SP(A):

5.18. Theorem. Precomposing the functor S of construction 2.9 gives and equivalence

A-Sep(X) ≃ Ext[SP(A), X]

Proof. This is precisely the content of propositions 5.13 and 5.17.

The equivalence of theorem 5.18 applies to extensive categories X, which do not necessarily possess products. However, in the event A possesses sums, proposition 2.7 shows that SP(A) possesses products, and corollary 2.15 shows that these products are preserved by S. It follows that, if the category X possesses products, the equivalence induced by precomposition with S carries product preserving functors to product preserving functors. We now aim to prove that in this case precomposition with S restricts to an equivalence between the product preserving subcategories of A-Sep(X) and Ext[SP(A), X].

5.19. Lemma. Suppose that A admits sums and X admits products. Let H: P(A) → X be an A-separable functor which preserves products. For A, B ∈ A, and with the notation of construction 2.6 for the product X^{[A]} × X^{[B]} in SP(A), let

α: HX^{A} × HX^{B} → HX^{A+B}

be the isomorphism arising from H preserving this product. Then

α · (HUp, HUq) = (|_{i∈I_{×}} HX^{c_{i}})

Proof. This is a routine calculation using the formulas

p · inj_{i} = X^{[c_{i}·i]}
q · inj_{i} = X^{[c_{i}·j]}

for the projections. The projections of the product HX^{A+B} of HX^{A} and HX^{B} in X are HX^{i} and HX^{iB}, and we observe

HX^{i} · α · (HUp, HUq) · inj_{i} = HUp · inj_{i} = HX^{c_{i}·i} = HX^{i} · HX^{c_{k}}

A similar calculation for j in place of i and the universal properties of sums and products then yields the desired result.

Now, in the notation of this lemma and with \overline{H} and ϕ_{H} as in construction 5.7, the diagram

\overline{H}(X^{[A]} × X^{[B]})  \overline{ϕ_{H}(X^{[A]} × X^{[B]}) ^{}}HU(X^{[A]} × X^{[B]})

[figure: \overline{H}X^{[A]} × \overline{H}X^{[B]}; (\overline{H}p, \overline{H}q); ϕ_{H}X^{[A]} × ϕ_{H}X^{[B]}; HUX^{[A]} × HUX^{[B]}; (HUp, HUq)]

(22)

commutes. This follows directly from general facts about products. The square commutes after postcomposing the projection p – paste the square defining p · (ϕ_{H}X^{[A]} × ϕ_{H}X^{[B]}) on the bottom of the above square, and the exterior square is naturality of ϕ_{H} at p. Similarly, the square commutes on postcomposition with q, and the desired commutativity follows from properties of products.

For \overline{H} to preserve products is precisely for the left arrow of diagram (22) to be invertible (for all A and B). Using the formula of the previous lemma, we can show that the diagonal of this square is a summand, and thus allow us to use the summand calculus in trying to prove that (\overline{H}p, \overline{H}q) is invertible.

5.20. Lemma. In the context of lemma 5.19, the arrow

(|_{i} HX^{c_{i}}) · ϕ_{H}(X^{[A]} × X^{[B]})

is a summand of HX^{A+B}.

Proof. The arrow ϕ_{H}(X^{[A]}×X^{[B]}) is constructed by lifting the definition of ϕ on monomials to sums of monomials by the universal property of the family construction. Thus

ϕ_{H}(X^{[A]} × X^{[B]}) = ∑_{i∈I_{×}} ϕX^{[C_{i}]}

It follows the arrow in question may be rewritten as

(|_{i} HX^{c_{i}} · ϕX^{[C_{i}]})

and we may then apply lemma 5.11 with C in place of A to see that the family of summands

HX^{c_{i}} · ϕX^{[C_{i}]}

for i ∈ I is pairwise disjoint. Restricting to i ∈ I_{×}, we still obtain a pairwise disjoint family of summands. Applying proposition 3.5 yields the desired result.

Thus (\overline{H}p, \overline{H}q) is a comparison of the summand comprising the diagonal of diagram (22) in the summand ϕX^{[A]} × ϕX^{[B]}. If we can show a reverse comparison, we shall have proved the invertibility of (\overline{H}p, \overline{H}q).

5.21. Lemma. In the context of lemma 5.19, we have

¬[(|_{i} HX^{c_{i}}) · ϕ_{H}(X^{[A]} × X^{[B]})] ∧ [α · (ϕ_{H}X^{[A]} × ϕ_{H}X^{[B]})] = ⊥

in (HX^{A+B})^{∗}.

Proof. We have that

(|_{i∈I_{×}} HX^{c_{i}}) · ϕ_{H}(X^{[A]} × X^{[B]}) = (|_{i∈I_{×}} HX^{c_{i}} · ϕ_{H}X^{[C_{i}]})  (23)

To compute the complement of this summand, we consider the extension of the above arrow to the sum over all i ∈ I. The arrow

(|_{i∈I} HX^{c_{i}} · ϕ_{H}X^{[C_{i}]})

is invertible – this is precisely the result of proposition 5.13 on considering the calculation of equation (19) in the proof. Thus the complement of the summand of equation (23) is

(|_{i∈I\I_{×}} HX^{c_{i}} · ϕ_{H}X^{[C_{i}]})

– we have restricted the arrow to those summands not included in the summand of equation (23). This summand is a join in (HX^{A+B})^{∗} of the summands HX^{c_{i}} · ϕX^{[C_{i}]} for i ∈ I \ I_{×}, and thus to show it disjoint from α · (ϕ_{H}X^{[A]} × ϕ_{H}X^{[B]}) it suffices to show

[HX^{c_{i}} · ϕ_{H}X^{[C_{i}]}] ∧ [α · (ϕ_{H}X^{[A]} × ϕX^{[B]})] = ⊥  (24)

for each i ∈ I \ I_{×}.

Given i ∈ I \ I_{×} then, we observe that either c_{i} · i or c_{i} · j is not an M (from the definition of I_{×}). Without loss of generality we shall consider the case where c_{i} · i is not an M. Write Quo_{E}(A) = (A_{j}, a_{j}, J, j_{∗}), and factor c_{i} · i = m · a_{j} for m an M and j ∈ J. Now a_{j} is not invertible (since c_{i} ·i is not an M). Considering equation (13), the definition of ϕ_{H}X^{[A]}, we see that

[ϕ_{H}X^{[A]}] ∧ [HX^{a_{j}}] = ⊥  (25)

since HX^{a_{j}} is one of the summands included in the join which is the complement of ϕ_{H}X^{[A]}.

Consider the meet of HX^{c_{i}} · ϕ_{H}X^{[C_{i}]} and α · (ϕ_{H}X^{[A]} × ϕ_{H}X^{[B]}) – that is, the pullback P in the following diagram:

P  \overline{}\overline{H}X^{[A]} × \overline{H}X^{[B]}
[figure: ϕ_{H}X^{[A]} × ϕ_{H}X^{[B]}]
HX^{A} × HX^{B}  \overline{H}X^{[A]}
[figure: ϕ_{H}X^{[A]}]
HX^{A}
[figure: HX^{i}; HX^{a_{j}}]
HX^{C}^{α^{}}HX^{A_{j}}
[figure: HX^{c_{i}}; HX^{m}]
[figure: \overline{H}X^{[C_{i}]}; ϕ_{H}X^{[C_{i}]}; HX^{C_{i}}]

The upper diamond (whose unlabelled sides are product projections) commutes by definition of ϕ_{H}X^{[A]} × ϕ_{H}X^{[B]}. The lower diamond follows from c_{i} · i = m · a_{j}. The triangle is the definition of the isomorphism α showing preservation of products by H (recall that C = A + B). Thus we can use the pullback projections of P to obtain arrows P → \overline{H}X^{[A]} and P → HX^{A_{j}} with commutativity so as to yield an arrow from P to the pullback of ϕ_{H}X^{[A]} and HX^{a_{j}}. Equation (25) shows these summands are disjoint, and hence this pullback is initial. Thus P admits an arrow to an initial, and is hence initial. This proves equation (24), and the result follows.

We now show the required preservation of products.

5.22. Proposition. Suppose that A admits sums and X admits products. For an A-separable H: P(A) → X which preserves products, the functor \overline{H} of construction 5.7 preserves products.

Proof. The terminal object of P(A) is X^{0}, where 0 is initial in A. Since S preserves limits, the terminal object of SP(A) is SX^{0}. Now \overline{H}S ≅ H, and so preservation of the terminal object by \overline{H} follows from preservation of the terminal object by H.

For binary products, we need only check at monomials. Given A, B ∈ A, use notation of construction 2.6 for their product. For \overline{H} to preserve products is for the arrow (\overline{H}p, \overline{H}q) given by properties of products to be invertible.

Consider the commutative square (22). The diagonal of this square is a summand, being isomorphic via α to the summand of lemma 5.20. It follows (\overline{H}p, \overline{H}q) is a comparison arrow, and thus to show it invertible we need only show the reverse comparison. It suffices to do this in the summands of HX^{C}, translating via the isomorphism α. That is, we need only show

(|_{i} HX^{c_{i}}) · ϕ_{H}(X^{[A]} × X^{[B]}) ≤ α · (ϕ_{H}X^{[A]} × ϕ_{H}X^{[B]})

This follows using boolean algebra from the result of lemma 5.21.

We can thus state the universality of SP(A) for extensive categories with products:

5.23. Theorem. Suppose that A admits sums and X admits products. The equivalence of theorem 5.18 restricts to an equivalence between the full subcategories of A-Sep(X) and Ext[SP(A), X] with objects the product preserving functors in each case.

Proof. That the restriction induces an equivalence between appropriate subcategories follows from the fact S preserves products from corollary 2.15, and that the construction \overline{(–)} of 5.10 takes product preserving functors to product preserving functors by proposition 5.22.

References

[1] A. Carboni and G. Janelidze. Decidable (= separable) objects and morphisms in lextensive categories. Journal of Pure and Applied Algebra, 110(3):219–240, 1996.

[2] A. Carboni, G. Janelidze, G. M. Kelly, and R. Paré. On localization and stabilization for factorization systems. Applied Categorical Structures, 5(1):1–58, 1997.

[3] A. Carboni, S. Lack, and R.F.C. Walters. Introduction to extensive and distributive categories. Journal of Pure and Applied Algebra, 84(2):145–158, Februrary 1993.

[4] J.R.B. Cockett. Introduction to distributive categories. Mathematical Structures in Computer Science, 3:277–307, 1993.

[5] P. J. Freyd and G. M. Kelly. Categories of continuous functors, I. Journal of Pure and Applied Algebra, 2:169–191, 1972.

[6] R. Gates. On extensive and distributive categories. PhD thesis, University of Sydney, 1997.

[7] R. Gates. On the Generic solution to P (X) ≅ X in Distributive Categories. Journal of Pure and Applied Algebra, 125(1–3):191–212, 1998.

[8] G. M. Kelly. Monomorphisms, epimorphisms, and pull-backs. Journal of the Australian Mathematical Society, IX:124–142, 1969.

[9] F.W. Lawvere. Some thoughts on the future of category theory. In A. Carboni, M.C. Pedicchio, and G. Rosolini, editors, Category Theory, Proceedings, Como 1990, Springer Lecture Notes in Mathematics 1488, pages 1–13. Springer-Verlag, 1991.

[10] S.H. Schanuel. Objective number theory. Notes from CT’95 Halifax Summer School, July 1995.

[11] R.P. Stanley. Enumerative Combinatorics Volume I. Wadsworth & Brooks/Cole, 1986.

[12] R.F.C. Walters. Data types in distributive categories. Bulletin of the Australian Mathematical Society, 40(1):79–82, August 1989.

[13] R.F.C. Walters. Categories and Computer Science. Carslaw Publications, 1991.

School of Mathematics and Statistics University of Sydney NSW, 2006 Australia

Email: robbie@maths.usyd.edu.au
http://cat.maths.usyd.edu.au/~robbie

This article may be accessed via WWW at http://www.tac.mta.ca/tac/ or by anony-

mous ftp at ftp://ftp.tac.mta.ca/pub/tac/html/volumes/1998/n10/n10.{dvi,ps}

THEORY AND APPLICATIONS OF CATEGORIES (ISSN 1201-561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods.

Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication.

The method of distribution of the journal is via the Internet tools WWW/ftp. The journal is archived electronically and in printed paper format.

Subscription information. Individual subscribers receive (by e-mail) abstracts of articles as they are published. Full text of published articles is available in .dvi and Postscript format. Details will be e-mailed to new subscribers and are available by WWW/ftp. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor, Robert Rosebrugh, rrosebrugh@mta.ca.

Information for authors. The typesetting language of the journal is TEX, and L^{A}TEX is the preferred flavour. TEX source of articles for publication should be submitted by e-mail directly to an appropriate Editor. They are listed below. Please obtain detailed information on submission format and style files from the journal’s WWW server at URL http://www.tac.mta.ca/tac/ or by anonymous ftp from ftp.tac.mta.ca in the directory pub/tac/info. You may also write to tac@mta.ca to receive details by e-mail.

Editorial board.

John Baez, University of California, Riverside: baez@math.ucr.edu Michael Barr, McGill University: barr@math.mcgill.ca Lawrence Breen, Université de Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of North Wales: r.brown@bangor.ac.uk Jean-Luc Brylinski, Pennsylvania State University: jlb@math.psu.edu Aurelio Carboni, Università dell Insubria: carboni@fis.unico.it P. T. Johnstone, University of Cambridge: ptj@pmms.cam.ac.uk G. Max Kelly, University of Sydney: kelly m@maths.usyd.edu.au Anders Kock, University of Aarhus: kock@imf.au.dk F. William Lawvere, State University of New York at Buffalo: wlawvere@acsu.buffalo.edu Jean-Louis Loday, Université de Strasbourg: loday@math.u-strasbg.fr Ieke Moerdijk, University of Utrecht: moerdijk@math.ruu.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mscs.dal.ca Andrew Pitts, University of Cambridge: ap@cl.cam.ac.uk Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca Jiri Rosicky, Masaryk University: rosicky@math.muni.cz James Stasheff, University of North Carolina: jds@charlie.math.unc.edu Ross Street, Macquarie University: street@macadam.mpce.mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Rutgers University: tierney@math.rutgers.edu Robert F. C. Walters, University of Sydney: walters b@maths.usyd.edu.au R. J. Wood, Dalhousie University: rjwood@mscs.dal.ca