Theory and Applications of Categories, Vol. 8, No. 22, 2001, pp. 541–554.

THE EXTENSIVE COMPLETION OF A DISTRIBUTIVE CATEGORY

J.R.B. COCKETT AND STEPHEN LACK

ABSTRACT. A category with finite products and finite coproducts is said to be distributive if the canonical map A × B + A × C → A × (B + C) is invertible for all objects A, B, and C. Given a distributive category 𝒟, we describe a universal functor 𝒟 → 𝒟_{ex} preserving finite products and finite coproducts, for which 𝒟_{ex} is extensive; that is, for all objects A and B the functor 𝒟_{ex} /A × 𝒟_{ex} /B → 𝒟_{ex} /(A + B) is an equivalence of categories. As an application, we show that a distributive category 𝒟 has a full distributive embedding into the product of an extensive category with products and a distributive preorder.

1. Introduction

A category with finite products and finite coproducts is said to be distributive, if for all objects A, B, and C, the canonical map

δ : A × B + A × C → A × (B + C)

is invertible. These categories have proved to be important in theoretical computer science as they facilitate reasoning about programs with control and the specification of abstract data types. Every topos is a distributive category, so the categories Set, Gph, Set^{G}, and Shv(X) of sets, (directed) graphs, G-sets, and sheaves on a space are all distributive. But there are many other examples which are not toposes, such as the category Top of topological spaces and continuous maps, the category Hty of topological spaces and homotopy classes of maps, the poset 𝒫(X) of subsets of a set X, or the opposite of the category of commutative rings. The papers [3, 6] contain an introduction to distributive categories; see also the book [16].

A category ℰ with finite coproducts is said to be extensive if the functors ℰ /A×ℰ /B → ℰ /(A + B) sending a pair (f : X → A, g : Y → B) to f + g : X + Y → A + B are equivalences of categories for all objects A and B. These categories are particularly important in geometry – see for instance [13, 15] — but also in proof theory [1], categorical Galois theory [2], and descent morphisms for internal structures [14]. All of the above examples of distributive categories are also extensive except for 𝒫(X). More generally, any distributive lattice, viewed as a preorder, is a distributive category which is not extensive.

The first author gratefully acknowledges the support of NSERC, Canada; the second author that of the Australian Research Council.

Received by the editors 2001 May 21 and, in revised form, 2001 December 4.

Transmitted by Walter Tholen. Published on 2001 December 15.

2000 Mathematics Subject Classification: 18D99, 18A40, 18B15.

Key words and phrases: distributive category, extensive category, free construction.

\begin{matrix}c \\ ◯ \end{matrix} J.R.B. Cockett and Stephen Lack, 2001. Permission to copy for private use granted.

On the other hand, the full subcategory of Top consisting of those spaces which can be embedded in three-dimensional Euclidean space ℝ^{3} is extensive, but it is not distributive, because it does not have finite products — it’s not hard to show that the product of two three-dimensional spaces would have to have dimension greater than three. Thus an extensive category can fail to be distributive by failing to have finite products, but this is in fact the only possible problem: every extensive category with finite products is distributive. For a proof of this, and a general introduction to extensive categories, see once again either of the papers [3, 6].

Thus among the distributive categories are the extensive categories with products. Our main result is to construct for each distributive category 𝒟 an extensive category with products 𝒟_{ex} equipped with a functor 𝒟 → 𝒟_{ex} which preserves finite products and finite coproducts and is the universal such functor into an extensive category with products. More formally, a functor between distributive categories is called a distributive functor if it preserves finite products and finite coproducts. There is a 2-category Dist of distributive categories, distributive functors, and natural transformations; and this 2category Dist has a full sub-2-category Ext_{pr} consisting of those distributive categories which are also extensive. We construct a left biadjoint to the inclusion of Ext_{pr} into Dist, sending a distributive category 𝒟 to 𝒟_{ex}. We call 𝒟_{ex} the extensive completion of the distributive category 𝒟.

This construction was found independently by the two authors in 1995, and appeared in the second author’s unpublished thesis [11]. Since then, we have found a more conceptual approach than the explicit construction given here. This conceptual approach has lead to the series of papers [7, 8, 9], and is described fully in the last of them [9].

Since the explicit construction may be of interest to some people who do not want to work through the theoretical machinery involved in this conceptual approach, we decided to write this paper to provide an exposition of this more elementary construction using Boolean propositions. The “cost” of avoiding the theory developed in these papers is that the proof we give below involves lengthy, and rather uninspiring, diagram-chasing in distributive categories.

In any case, the general idea of the conceptual approach can be easily described: for a distributive category 𝒟, there is a monad +1 on 𝒟 sending an object A to A + 1, and the Kleisli category of this monad can be viewed as an “abstract category of partial maps” (a restriction category in the sense of [7]). This means in particular that it embeds canonically in an actual category of partial maps (obtained from the Kleisli category by splitting certain idempotents) and the subcategory of total maps is now 𝒟_{ex}. There is a striking analogy with the exact completion of a regular category. In that case one starts with a regular category 𝒞, forms the category of relations in 𝒞, then splits certain idempotents in this category; the resulting category is then the category of relations in the exact completion 𝒞_{ex/reg}: see [4] or [12] and the references therein.

Notation. The identity morphism on an object A is denoted by A. Our notation for coproducts is: (f g) : A+B → C for the morphism induced by f : A → C and g : B → C, and i_{n} for the injection of the nth summand, i_{n,m} for the injection of the nth and mth summands, and so on. Our notation for products is: \binom{f}{g} : C → A × B for the morphism induced by f : C → A and g : C → B, and p_{n} for the projection onto the nth factor, while the unique map from an object A to the terminal object 1 is denoted by !. We sometimes write tw for the canonical isomorphism A + B → B + A.

2. The category of Boolean propositions

Let 𝒟 be a distributive category. A Boolean proposition in 𝒟 is an object A equipped with a morphism a : A → 1 + 1. The aim of this section is to define a category Bool(𝒟) whose objects are the Boolean propositions in 𝒟, to define the inclusion functor 𝒟 → Bool(𝒟) taking each object to the “always true” proposition on that object, and to show that Bool(𝒟) is extensive and has finite products. In the following section we shall show that Bool(𝒟) has the universal property of the extensive completion 𝒟_{ex} of 𝒟.

The description of Bool(𝒟) is very easy, but even to prove that it is a category involves some diagram-chasing in 𝒟. An object of Bool(𝒟) is a Boolean proposition (A, a) in 𝒟, while a morphism in Bool(𝒟) from (A, a) to (B, b) is a morphism f : A → B + 1 in 𝒟 rendering commutative

\xymatrix{A \ar[r]^{f} \ar[d]_{a} & B + 1 \ar[d]^{b+1} \\ 1 + 1 \ar[r]_{i_{1,3}} & 1 + 1 + 1.}

The composite of arrows f : (A, a) → (B, b) and g : (B, b) → (C, c) is the “Kleisli composite”:

\xymatrix{A \ar[r]^{f} & B + 1 \ar[r]^{g+1} & C + 1 + 1 \ar[r]^{C+!} & C + 1}

and this composition is clearly associative. The identities are a little more delicate: the identity at an object (A, a) is the map ι_{a} : A → A + 1 given by

[figure: A; ^{\binom{A}{a}}; A × (1 + 1); δ^{−1}; A + A; A+!; A + 1.]

2.1. Proposition. Bool(𝒟) is a category.

Proof. We must show that each ι_{a} is an endomorphism of (A, a), and that it satisfies the two identity laws.

The fact that ι_{a} is a morphism in Bool(𝒟) follows from commutativity of

[figure: A; ^{\binom{A}{a}}; a; A × (1 + 1); δ^{−1}; a×(1+1); A + A; A+!; a+a; A + 1; a+1; 1 + 1; Δ; (1 + 1) × (1 + 1); δ^{−1}; 1 + 1 + 1 + 1; 1+1+!; 1 + 1 + 1]

and the fact that the composite of the three arrows across the bottom of the diagram is i_{1,3} : 1 + 1 → 1 + 1 + 1. We shall sometimes write 1_{(A,a)} if we wish to emphasize that ι_{a} is being thought of as an arrow in Bool(𝒟).

The fact that f1_{(A,a)} = f for a map f : (A, a) → (B, b) follows from commutativity of

[figure: A; ^{\binom{A}{a}}; f; _{\binom{f}{f}}; A × (1 + 1); δ^{−1}; f×(1+1); A + A; A+!; f+f; A + 1; f+1; (B + 1) × (B + 1); (B+1)×(!+!); (B + 1) × (1 + 1); δ^{−1}; B + 1 + B + 1; B+!; B+1+1; B+!; B + 1; Δ; 1; B + 1]

while the fact that 1_{(B,b)}f = f follows from commutativity of

[figure: A; f; _{\binom{A}{a}}; B + 1; \binom{B}{b}+1; _{\binom{B+1}{(b i_{2})}}; B × (1 + 1) + 1; δ^{−1}+1; B + B + 1; B+!; A × (1 + 1); f×(1+1); δ^{−1}; (B + 1) × (1 + 1); δ^{−1}; B + 1 + B + 1; B+!; B + 1; A + A; f+f; A+!; A + 1; (f i_{2})]

and the previous result.

For an object A of 𝒟, we write t : A → 1 + 1 for the Boolean proposition on A given by the composite of i_{1} : 1 → 1 + 1 with the unique map ! : A → 1. We think of this as the “always true” proposition on A. There is a functor I : 𝒟 → Bool(𝒟) sending an object A of 𝒟 to (A, t) and sending a morphism f : A → B to the composite of f with the injection B → B + 1. Since in a distributive category the coproduct injections are monic (see [3, Proposition 3.3]), the functor I is clearly faithful. We shall see in the following section that it exhibits Bool(𝒟) as the extensive completion of 𝒟.

We define the disjoint union of Boolean propositions (A, a) and (B, b) to be (A+B, a⊔ b), where a ⊔ b is (a b) : A + B → 1 + 1.

2.2. Proposition. Bool(𝒟) has finite coproducts; the coproduct of (A, a) and (B, b) is (A + B, a ⊔ b), while the initial object is (0, t). The functor I : 𝒟 → Bool(𝒟) preserves finite coproducts.

Proof. The fact that (0, t) is initial is trivial. As for binary coproducts, observe that there is a bijection between arrows (f g) : A + B → C and pairs (f : A → C, g : B → C) of arrows in 𝒟, natural in C. If now c : C → 1 + 1, then (f g) : A + B → C + 1 is an arrow in Bool(𝒟) from (A+B, a⊔b) to (C, c) if and only if f and g are arrows in Bool(𝒟) from (A, a) to (C, c) and from (B, b) to (C, c). One easily sees that the resulting bijection between maps (A + B, a ⊔ b) → (C, c) and pairs of maps ((A, a) → (C, c), (B, b) → (C, c)) is natural in (C, c). Thus (A + B, a ⊔ b) is the coproduct in 𝒟_{ex} of (A, a) and (B, b).

The fact that I preserves finite coproducts is clear from the description of these coproducts in Bool(𝒟).

It will also be useful to have an explicit description of the injections of the coproduct (A + B, a ⊔ b). These are the maps corresponding to the identity 1_{(A+B,a⊔b)} under the bijection described in the proposition; that is, the composites of ι_{a⊔b} : A + B → A + B + 1 with the injections A → A + B and B → A + B. The reader will easily verify that these are the maps

\xymatrix{A \ar[r]^{ι_{a}} & A + 1 \ar[r]^{i_{1,3}} & A + B + 1 & B + 1 \ar[l]_{i_{2,3}} & B. \ar[l]_{ι_{b}}}

We now turn to finite products. We define the cartesian conjunction of Boolean propositions (A, a) and (B, b) to be (A × B, a ⊓ b), where a ⊓ b is the composite &(a × b), and & is

\xymatrix{(1 + 1) × (1 + 1) \ar[r]^{δ^{−1}} & 1 + 1 + 1 + 1 \ar[r]^{1+!} & 1 + 1.}

2.3. Proposition. Bool(𝒟) has finite products; the product of (A, a) and (B, b) is (A × B, a ⊓ b), while the terminal object is (1, t) The functor I : 𝒟 → Bool(𝒟) preserves finite products. Proof. A map f : (A, a) → (1, t) is a map f : A → 1 + 1 in 𝒟 satisfying i_{1,3}a = i_{1,3}f, but since i_{1,3} is (split) monic, a is the unique such map. This proves that (1, t) is terminal.

We claim that the maps

\xymatrix{A + 1 & A × B + 1 \ar[l]_{π_{A}+1} & A × B \ar[l]_{ι_{a⊓b}} \ar[r]^{ι_{a⊓b}} & A × B + 1 \ar[r]^{π_{B}+1} & B + 1}

exhibit (A × B, a ⊓ b) as the product of (A, a) and (B, b). Given f : (C, c) → (A, a) and g : (C, c) → (B, b), the induced map (C, c) → (A × B, a ⊓ b) is

[figure: C; ^{\binom{f}{g}}; (A + 1) × (B + 1); ε; A × B + B + A + 1; A×B+!; A × B + 1]

where ε : (A + 1) × (B + 1) → A × B + B + A + 1 is the evident isomorphism arising from distributivity of 𝒟. We leave the verifications to the reader.

The fact that I preserves finite products is clear from the description of these products in Bool(𝒟). 2.4. Theorem. The category Bool(𝒟) is an extensive category with finite products, and so in particular is distributive. Proof. It remains only to prove that Bool(𝒟) is extensive. It suffices by [3, Proposition 4.1] to prove that Bool(𝒟) has pullbacks along the injections of the coproduct (1 + 1, t ⊔ t) and also that if

\xymatrix{(A_{1}, a_{1}) \ar[r]^{j_{1}} \ar[d] & (A, a) \ar[d]^{f} & (A_{2}, a_{2}) \ar[l]_{j_{2}} \ar[d] \\ (1, t) \ar[r]_{i_{1}} & (1 + 1, t ⊔ t) & (1, t) \ar[l]^{i_{2}}}

are commutative squares, then they are pullbacks if and only if the top row is a coproduct diagram.

We observe that t ⊔ t is the composite of the unique map ! : 1 + 1 → 1 with the injection i_{1} : 1 → 1 + 1. To say that f : A → 1 + 1 + 1 is a map in Bool(𝒟) from (A, a) to (1 + 1, t ⊔ t) is to say that

\xymatrix{A \ar[rr]^{a} \ar[d]_{f} &  & 1 + 1 \ar[d]^{i_{1,3}} \\ 1 + 1 + 1 \ar[r]_{!+1} & 1 + 1 \ar[r]_{i_{1,3}} & 1 + 1 + 1}

commutes, which amounts to saying that a = (! + 1)f. In this case, write f_{1} for (1+!)f : A → 1 + 1. We claim that

\xymatrix{(A, f_{1}) \ar[r]^{κ_{f}} \ar[d]_{!} & (A, a) \ar[d]^{f} \\ (1, t) \ar[r]_{i_{1}} & (1 + 1, t ⊔ t)}

is a pullback square in Bool(𝒟), where κ_{f} is the map represented by ι_{f_{1}}. Commutativity of

[figure: A; ^{\binom{A}{f}}; f; A × 3; A×(1+!); A × (1 + 1); δ^{−1}; f×(1+1); A + A; A+!; f+f; A + 1; f+1; 3; Δ; 1+!; 3 × 3; 3×(1+!); 3 × (1 + 1); δ^{−1}; 3 + 3; 3+!; 3 + 1; 1 + 1; i_{1}+1]

says that (f + 1)ι_{f_{1}} = (i_{1} + 1)f_{1}, whence it follows easily that κ_{f} is indeed a map in Bool(𝒟) and that the purported pullback square commutes.

As for universality, let

\xymatrix{(B, b) \ar[r]^{g} \ar[d]_{b} & (A, a) \ar[d]^{f} \\ (1, t) \ar[r]_{i_{1}} & (1 + 1, t ⊔ t)}

be a commutative square in Bool(𝒟). We must show that there is a unique arrow g′ : (B, b) → (A, f_{1}) for which κ_{f}g′ = g. But if g′ : (B, b) → (A, f_{1}), then ι_{f_{1}}g′ = g′, by one of the identity laws, so that g = κ_{f}g′ = g′, giving the uniqueness. It remains only to show that g is in fact an arrow from (B, b) to (A, f_{1}) in Bool(𝒟); that is, that

\xymatrix{B \ar[rr]^{b} \ar[d]_{g} &  & 1 + 1 \ar[d]^{i_{1,3}} \\ A + 1 \ar[r]_{f+1} & 3 + 1 \ar[r]_{1+!+1} & 1 + 1 + 1}

commutes, but this follows from the commutativity of

\xymatrix{B \ar[rr]^{b} \ar[d]_{g} &  & 1 + 1 \ar[d]^{i_{1,3}} & B \ar[rr]^{b} \ar[d]_{g} &  & 1 + 1 \ar[d]^{i_{1,3}} \\ A + 1 \ar[r]_{f+1} & 3 + 1 \ar[r]_{!+1+1} & 1 + 1 + 1 & A + 1 \ar[r]_{f+1} & 3 + 1 \ar[r]_{1+1+!} & 1 + 1 + 1}

which express the fact that g : (B, b) → (A, a) is a morphism and that the square involving g commutes.

Thus Bool(𝒟) has pullbacks along injections. To see that the coproduct (1 + 1, t ⊔ t) is stable under pullback, let f : (A, a) → (1 + 1, t) be given, and form the pullback (A, f_{1}) along the first injection, as above. Similarly, the pullback along the second injection can be formed as (A, f_{2}), where f_{2} is the composite (1+!)(tw + 1)f. Thus we have pullback squares

\xymatrix{(A, f_{1}) \ar[d] \ar[r]^{κ_{f}} & (A, a) \ar[d]^{f} & (A, f_{2}) \ar[l]_{λ_{f}} \ar[d] \\ (1, t) \ar[r]_{i_{1}} & (1 + 1, t ⊔ t) & (1, t) \ar[l]^{i_{2}}}

where λ_{f} is the map represented by ι_{f_{2}}; and we must show that the top row is a coproduct diagram. In other words, we must show that the map (κ_{f} λ_{f}) : (A + A, (f_{1} f_{2})) → (A, a) represented by (ι_{f_{1}} ι_{f_{2}}) : A + A → A + 1 is invertible. It is so with inverse represented by the composite

[figure: A; ^{\binom{A}{f}}; A × (1 + 1 + 1); δ^{−1}; A + A + A; A+A+!; A + A + 1.]

To show that Bool(𝒟) is extensive, it will now suffice to show that

\xymatrix{(A, a) \ar[r] \ar[d] & (A, a) + (B, b) \ar[d]^{!+!} \\ (1, t) \ar[r]_{i_{1}} & (1 + 1, t ⊔ t)}

is a pullback, where the upper horizontal arrow is the coproduct injection i_{1,3}ι_{a} : A → A + B + 1. Given our explicit calculation of pullbacks along injections, this amounts to proving, for c equal to the composite

\xymatrix{A + B \ar[r]^{a+b} & 1 + 1 + 1 + 1 \ar[r]^{1+tw+1} & 1 + 1 + 1 + 1 \ar[r]^{1+1+!} & 1 + 1 + 1}

that the map (A, a) → (A + B, c) represented by i_{1,3}ι_{a} is invertible. It is so, with inverse

\xymatrix{A + B \ar[r]^{ι_{a}+!} & A + 1 + 1 \ar[r]^{A+!} & A + 1.}

3. The extensive completion of a distributive category

In this section we show that the functor I : 𝒟 → Bool(𝒟) sending an object to the “always true” Boolean proposition on it exhibits Bool(𝒟) as the extensive completion of 𝒟. In fact we shall do more than this: we show that Bool(𝒟) has a universal property not just with respect to distributive functors, but with respect to arbitrary functors which preserve finite coproducts and whose codomain is extensive. More precisely, we show that for any extensive category ℰ, composition with I induces an equivalence of categories between the category of finite-coproduct-preserving functors from 𝒟 to ℰ, and the category of finitecoproduct-preserving functors from Bool(𝒟) to ℰ. Then the statement that Bool(𝒟) is the extensive completion of 𝒟 amounts to the further claim that if ℰ has finite products, then a finite-coproduct preserving functor Bool(𝒟) → ℰ preserves finite products if and only if its composite with I does so.

Let ℰ be an arbitrary extensive category — we do not assume that ℰ has products — and let F : 𝒟 → ℰ be a finite-coproduct-preserving functor. For each object (A, a) of Bool(𝒟), we may form the pullback

\xymatrix{\overline{F} (A, a) \ar[r]^{k_{a}} \ar[d]_{l_{a}} & F A \ar[d]^{F a} \\ F 1 \ar[r]_{F i_{1}} & F (1 + 1)}

in ℰ, since ℰ has pullbacks along coproduct injections because ℰ is extensive, and F i_{1} is a coproduct injection because F preserves finite coproducts. We shall show that this gives the object-part of a functor \overline{F} : Bool(𝒟) → ℰ. We define \overline{F} on an arrow f : (A, a) → (B, b) in Bool(𝒟) using the cube

[figure: \overline{F} (A, a); \overline{F} f; l_{a}; k_{a}; \overline{F} (B, b); F (i_{B})k_{b}; l_{b}; F A; F f; F a; F (B + 1); F (b i_{2}); F 1; F 1; F i_{1}; F 1; F i_{1}; F (1 + 1); F (1+1); F (1 + 1)]

where the left and right faces are pullbacks by definition of \overline{F} (A, a) and \overline{F} (B, b) and by extensivity of ℰ, and where the remaining faces commute.

This defines a finite-coproduct-preserving functor \overline{F} : Bool(𝒟) → ℰ. Of course it is only defined up to isomorphism unless specific choices of the relevant pullbacks have been made, but clearly we can ensure that \overline{F} I = F. Similarly, if G : 𝒟 → ℰ is another finite-coproduct-preserving functor and α : F → G a natural transformation, define \overline{G} as for \overline{F}, and there is now a unique way to extend α to a natural transformation \overline{α} : \overline{F} → \overline{G}: one defines \overline{α}_{(A,a)} so as to render commutative the cube

[figure: \overline{F} A; ^{\overline{α}^{(A,a)}}; k_{a}; l_{a}; \overline{G}A; k_{a}; l_{a}; F A; α_{A}; F a; GA; Ga; F 1; α_{1}; F i_{1}; G1; Gi_{1}; F (1 + 1); α_{1+1}; G(1 + 1).]

This proves:

3.1. Proposition. If ℰ is an extensive category, then composition with I induces an equivalence of categories between the category of finite-coproduct-preserving functors from Bool(𝒟) to ℰ, and the category of finite-coproduct-preserving functors from 𝒟 to ℰ

In particular, this means that, up to isomorphism, \overline{F} is the unique finite-coproduct-preserving functor for which \overline{F} I ≅ F.

3.2. Remark. Write Sums for the 2-category of categories with finite coproducts, finitecoproduct-preserving functors, and natural transformations; write Ext for the full sub-2-category consisting of the extensive categories. A little 2-categorical wizardry can be used to show that the inclusion Ext → Sums has a left biadjoint. An explicit construction of this biadjoint is probably quite complicated, but the proposition shows that for an object 𝒟 of Sums which happens to be distributive, the value of the left biadjoint is Bool(𝒟).

3.3. Theorem. Bool(𝒟) is the extensive reflection of 𝒟, in the sense that for any extensive category ℰ with finite products, composition with I : 𝒟 → Bool(𝒟) induces an equivalence between the category of distributive functors from Bool(𝒟) to ℰ and the category of distributive functors from 𝒟 to ℰ.

Proof. It remains only to show that \overline{F} : Bool(𝒟) → ℰ preserves finite products if and only if F does so. Since F = \overline{F} I and I preserves finite products, F will certainly preserve finite products if \overline{F} does so; we must prove the converse.

Suppose then that F : 𝒟 → ℰ is a distributive functor, and that \overline{F} : Bool(𝒟) → ℰ is the (essentially unique) finite-coproduct-preserving functor satisfying \overline{F} I = F. Clearly \overline{F} preserves the terminal object; we must show that it preserves the product of any pair of objects (A, a) and (B, b). To see this, consider the following diagrams in ℰ:

\xymatrix{\overline{F} (A, a) × \overline{F} (B, b) \ar[r]^{k_{a}×k_{b}} \ar[d]_{l_{a}×l_{b}} & F A_{1} × F A_{2} \ar[r]^{φ} \ar[d]^{F a×F b} & F (A × B) \ar[dd]^{F (a×b)} \\ F 1 × F 1 \ar[r]^{F i_{1}×F i_{1}} \ar[d]_{φ} & F (1 + 1) × F (1 + 1) \ar[dr]^{φ} \\ F (1 × 1) \ar[rr]^{F (i_{1}×i_{1})} \ar[d]_{F!} &  & F ((1 + 1) × (1 + 1)) \ar[d]^{F &} \\ F 1 \ar[rr]_{F i_{1}} &  & F (1 + 1)}

where the maps labelled φ are the canonical isomorphisms expressing the fact that F preserves products. The top left square is a pullback by definition of F (A, a) and F (B, b), and by the fact that products commute with pullbacks. The two squares involving φ’s commute, and the φ’s are invertible. The bottom square is a pullback because

\xymatrix{1 × 1 \ar[r]^{i_{1}×i_{1}} \ar[d]_{!} & (1 + 1) × (1 + 1) \ar[d]^{&} \\ 1 \ar[r]_{i_{1}} & 1 + 1}

is a pullback in 𝒟, and F preserves pullbacks along injections. It follows that the exterior square is a pullback; but this just says that \overline{F} preserves the product of (A, a) and (B, b).

In light of this theorem, we shall now use the notation 𝒟_{ex} in place of Bool(𝒟).

3.4. Proposition. If 𝒟 is itself extensive, then I : 𝒟 → 𝒟_{ex} is an equivalence of categories.

Proof. We have seen that Ext_{pr} is a full sub-2-category of Dist, and that the inclusion has a left biadjoint taking 𝒟 to 𝒟_{ex}, with I the unit of the biadjunction. It follows from general 2-categorical considerations that I must be an equivalence.

An object P of an arbitrary category is said to be preinitial if for each object A, there is at most one arrow from P to A. This is clearly equivalent to the unique arrow from the initial object being epimorphic, which is in turn equivalent to the diagram

\xymatrix{P \ar[r]^{1} & P & P \ar[l]_{1}}

exhibiting P as the coproduct P + P. This last characterization shows that any finitecoproduct-preserving functor preserves preinitial objects. In an extensive category sums are disjoint, whence it follows that the only preinitial object in an extensive category is the initial object. Putting these facts together we deduce:

3.5. Proposition. If 𝒟 is distributive and P is a preinitial object in 𝒟, then the image of P under I : 𝒟 → 𝒟_{ex} is initial.

In the special case that 𝒟 is a preorder, every object is preinitial. This gives:

3.6. Corollary. If 𝒟 is a distributive preorder, then 𝒟_{ex} is equivalent to the terminal category.

4. An embedding theorem

Recall [3] that a category is said to be locally distributive if it is distributive and every slice category is distributive, and lextensive if it is extensive and has finite limits. The first author proved [5] that a locally distributive category 𝒟 can be “subdirectly decomposed” into a distributive preorder and a lextensive category; that is, there is a distributive preorder 𝒫 and a lextensive category ℰ and a fully faithful functor 𝒟 → 𝒫×ℰ preserving finite coproducts and finite limits. Explicitly, write \overline{0} for the pullback of the injections 1 → 1 + 1. Then 𝒟/\overline{0} is a distributive preorder, \overline{0}/𝒟 is lextensive, and the functor I : 𝒟 → 𝒟/\overline{0} × \overline{0}/𝒟 sending A to (p_{2} : A × \overline{0} → \overline{0}, i_{2} : \overline{0} → A + \overline{0}) is fully faithful and preserves finite coproducts and finite limits.

These constructions fail if 𝒟 is only assumed to be distributive, for we cannot even guarantee the existence of \overline{0}. However we can subdirectly decompose a distributive category into a distributive preorder and an extensive category with products. The extensive category with products is the extensive completion 𝒟_{ex}, while the distributive preorder is the preorder reflection 𝒟_{pr}, which has the same objects as 𝒟, and A ≤ B if and only if there is an arrow in 𝒟 from A to B. Then 𝒟_{pr} is clearly distributive, and the canonical map Q : 𝒟 → 𝒟_{pr} is clearly a distributive functor. Write J : 𝒟 → 𝒟_{pr} × 𝒟_{ex} for the functor induced by Q and I.

4.1. Theorem. For a distributive category 𝒟, the functor J : 𝒟 → 𝒟_{pr} × 𝒟_{ex} is fully faithful, and so gives a subdirect decomposition of 𝒟 into a distributive preorder and an extensive category with products.

Proof. It remains only to prove that J is fully faithful. Certainly J is faithful, since I is so. Suppose then that A and B are objects of 𝒟, that f : A → B + 1 is a map IA → IB in 𝒟_{ex}, and that QA ≤ QB. We shall exhibit a map h : A → B so that Ih = f, whence it follows that J is full.

The fact that f : IA → IB is a map in 𝒟_{ex} amounts to the fact that (!+!)f : A → 1+1 factorizes through the first injection. Since QA ≤ QB, there is some map g : A → B in 𝒟. We take h : A → B be the composite

[figure: A; ^{\binom{g}{f}}; B × (B + 1); δ^{−1}; B × B + B; (p_{2} B); B.]

To say that Ih = f is just to say that f is the composite of h and i_{1} : B → B + 1. In the commutative diagram

[figure: A; _{\binom{g}{f}}; ^{( \begin{matrix}g \\ f \\ i_{1}! \end{matrix} )}; B × (B + 1); B×Δ; δ^{−1}; B × (B + 1) × (B + 1); B×(B+1)×(!+!); B × (B + 1) × (1 + 1); δ^{−1}×(1+1); (B × B + B) × (1 + 1); δ^{−1}; B × B + B; i_{1,4}; B × B + B + B × B + B]

write k for the value of the composite. The codomain is the coproduct of four components, and k factorizes through the injection of the first and fourth, but is also easily seen to factorize through the injection of the first two. It follows that arrows u, v : B × B + B + B ×B +B → C are equal if and only if their composites with the first injection are equal. Finally

i_{1}h = (i_{1}p_{2} i_{1} i_{1}p_{2} i_{1})k = (i_{1}p_{2} i_{2}! i_{1}p_{2} i_{2}!)k = f

whence the result.

A couple of remarks are appropriate here. First of all, if 𝒟 is of the form 𝒫 × ℰ to start with, where 𝒫 is a distributive preorder and ℰ is an extensive category with products, then 𝒟_{ex} may be taken to be ℰ itself, and I the projection. On the other hand, the preorder reflection of 𝒫 × ℰ is not in general 𝒫— for example consider the case where 𝒫 is the one-point preorder and ℰ is Set.

Secondly, while our result involves less structure than that of [5], there is another result involving more structure [10]. If 𝒟 is not just locally distributive but a quasitopos, then we can capture 𝒟 more precisely in terms of \overline{0}/𝒟 and 𝒟/\overline{0}. In that case, 𝒟 is (equivalent to) the comma category (\overline{0}/𝒟)/F where F : 𝒟/\overline{0} → \overline{0}/𝒟 is the the cartesian closed functor from the Heyting algebra 𝒟/\overline{0} to the topos \overline{0}/𝒟 taking an object u : A → \overline{0} of 𝒟/\overline{0} to A\overline{0} + \overline{0}. Conversely, if 𝒫 is a Heyting algebra, ℰ is a topos, and F : 𝒫 → ℰ is a cartesian closed functor, then ℰ /F is a quasitopos.

References

[1] A. Carboni, Some free constructions in realizability and proof theory, J. Pure Appl. Algebra 103:117–148, 1995.

[2] A. Carboni and G. Janelidze, Decidable (=separable) objects and morphisms in lextensive categories, J. Pure Appl. Algebra 110:219–240, 1996.

[3] A. Carboni, S. Lack, and R.F.C. Walters, Introduction to extensive and distributive categories, J. Pure Appl. Algebra 84:145–158, 1993.

[4] A. Carboni and E.M. Vitale, Regular and exact completions, J. Pure Appl. Alg., 125:79–116, 1998.

[5] J.R.B. Cockett, Categories with finite limits and stable binary coproducts can be subdirectly decomposed, J. Pure Appl. Alg. 78:131–138, 1992.

[6] J.R.B. Cockett, Introduction to distributive categories, Math. Structures Comput. Sci. 3:277–307, 1993.

[7] J.R.B. Cockett and Stephen Lack, Restriction categories I: Categories of partial maps, Theoretical Computer Science, 270:223–259, 2002.

[8] J.R.B. Cockett and Stephen Lack, Restriction categories II: Partial map classification, Theoretical Computer Science, to appear. Available electronically from

http://www.maths.usyd.edu.au/u/stevel/papers/restii.html.

[9] J.R.B. Cockett and Stephen Lack, Restriction categories III: Partial structures, in preparation.

[10] P.T. Johnstone, I. Moerdijk, and A. Pitts, Sketches of an Elephant: A topos theory compendium, manuscript in preparation, to appear with Oxford University Press.

[11] Stephen Lack, The algebra of distributive and extensive categories, Ph.D. thesis, Cambridge University, 1995.

[12] Stephen Lack, A note on the exact completion of a regular category, and its infinitary generalizations, Theory Appl. Categ., 5:70–80, 1999.

[13] F.W. Lawvere, Some thoughts on the future of category theory, in Category Theory (Lecture Notes in Mathematics 1488), Springer, Berlin, 1990.

[14] I. Le Creurer, Descent of internal categories, Ph.D. thesis, Louvain-la-Neuve, 1999.

[15] S.H. Schanuel, Negative sets have Euler characteristic and dimension, in: Category Theory (Lecture Notes in Mathematics 1488), Springer, Berlin, 1990.

[16] R.F.C. Walters, Categories and Computer Science, Cambridge University Press, Cambridge, 1991.

Department of Computer Science, University of Calgary, Calgary, Alberta, T2N 1N4, Canada

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

Email: robin@cpsc.ucalgary.ca and stevel@maths.usyd.edu.au

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/8/n22/n22.{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, Postscript and PDF. Details will be e-mailed to new subscribers. 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 http://www.tac.mta.ca/tac/. 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@barrs.org, Associate Managing Editor Lawrence Breen, Université 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: aurelio.carboni@uninsubria.it P. T. Johnstone, University of Cambridge: ptj@dpmms.cam.ac.uk G. Max Kelly, University of Sydney: maxk@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.uu.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mathstat.dal.ca Andrew Pitts, University of Cambridge: Andrew.Pitts@cl.cam.ac.uk Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca, Managing Editor Jiri Rosicky, Masaryk University: rosicky@math.muni.cz James Stasheff, University of North Carolina: jds@math.unc.edu Ross Street, Macquarie University: street@math.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 Insubria: walters@fis.unico.it R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca