Theory and Applications of Categories, Vol. 8, No. 21, 2001, pp. 522–540.

CLOSURE OPERATORS IN EXACT COMPLETIONS

MATÍAS MENNI

ABSTRACT. In analogy with the relation between closure operators in presheaf toposes and Grothendieck topologies, we identify the structure in a category with finite limits that corresponds to universal closure operators in its regular and exact completions. The study of separated objects in exact completions will then allow us to give conceptual proofs of local cartesian closure of different categories of pseudo equivalence relations. Finally, we characterize when certain categories of sheaves are toposes.

1. Introduction

It is well known that many interesting locally cartesian closed categories (even toposes) arise as solutions to universal problems of adding quotients of equivalence relations to categories with finite limits and to regular categories [6, 17, 12, 2]. Moreover, using the characterization of the categories with finite limits whose exact completions is locally cartesian closed given in [5] it was shown in [2] that if an exact completion E is locally cartesian closed then so are many interesting subcategories of E.

In the context of these results and studying the reasons why some exact completions are toposes we were led to investigate universal closure operators in exact completions in analogy with the situation for presheaf toposes, where for a small category C, universal closure operators in Set^{C^{op}} are in correspondence with Grothendieck topologies on C. We will present the results of this investigation and a couple of applications that show that it is both conceptually and practically useful to understand closure operators in exact completions in this way.

We will assume that the reader is familiar with the notions of regular and exact categories, with regular and exact completions of categories with finite limits [3] and with exact completions of regular categories [3, 6, 12]. We nevertheless quickly review these constructions in Section 2. For a category with finite limits C we denote the regular and exact completions respectively by C_{reg} and C_{ex}. For a regular category D we denote its reflection into the 2-category of exact categories by D_{ex/reg} and call it the “ex/reg completion”. We also assume familiarity with universal closure operators and related notions such as separated objects and sheaves [1, 4].

In Section 3 we introduce a notion of topology on locally small categories C with finite limits and show, in Proposition 3.5, that they are in bijective correspondence with the universal closure operators in C_{ex}.

PhD research supported by Consejo Nacional de Investigaciones Científicas y Técnicas (Conicet, Argentina), Fundación Antorchas/British Council, a CVCP Overseas Research Scholarship and EPSRC Research Grant GR/K06109.

Received by the editors July 31, 2001 and, in revised form, October 30, 2001.

Transmitted by I. Moerdijk. Published on November 16, 2001.

2000 Mathematics Subject Classification: 18A35, 18F10, 18B25.

Key words and phrases: Exact completions, closure operators, toposes.

\begin{matrix}c \\ ◯ \end{matrix} Matías Menni, 2001. Permission to copy for private use granted.

In Section 4 we start to study separated objects and sheaves for universal closure operators in exact completions.

Under mild conditions on a category C with finite limits it is possible to define a largest topology on C that makes every object of C separated in C_{ex}. We show that in this case, the category of separated objects for the induced universal closure operator in C_{ex} is equivalent to C_{reg}. The fact that for certain C, C_{reg} is a category of separated objects for a universal closure operator in C_{ex} has been observed in concrete cases. For example, in the context of realizability toposes [3] and in the context of equilogical spaces [19]. Our result provides a simple conceptual explanation for this phenomenon.

We then observe that regular categories D have a largest topology that makes every object of D a sheaf in D_{ex}. We call this topology the canonical topology. The main result of Section 4 is the characterization of the sheaves for the induced universal closure operator in D_{ex} as the equivalence relations in D with a strong “completeness” property. It turns out that these equivalence relations have already been used in other contexts. Most notably, in Higgs’ construction of localic toposes as categories of sets valued on a locale [7] and also, more abstractly, in Tripos theory [9].

The last two sections discuss applications of our results.

In Section 5 we give a conceptual proof of a result related to the one in [2] mentioned in the beginning about the local cartesian closure of certain subcategories of exact completions.

In Section 6 we give a characterization of the locally cartesian closed regular categories D whose associated category of sheaves for the canonical topology (identified in Section 4) is a topos. In this case, the category of sheaves is equivalent to D_{ex/reg}. So we are able to provide a novel perspective on how realizability toposes and toposes of sheaves on a locale arise ex/reg completions [6, 12].

All the results of the paper are part of the author’s thesis [13] and we will usually reference this work for details.

2. Completions

In this section we quickly review the constructions of regular and exact completions of categories with finite limits and of ex/reg completions of regular categories (see [3] for an expository presentation).

A relation from Y to X is a subobject of Y × X. We usually work with a pair of maps r_{Y} : R ^{}Y and r_{X} : R ^{}X such that ⟨r_{Y} , r_{X}⟩ : R ^{}Y × X is mono and induces the given relation.

Given relations S and R from Y to X we write S ≤ R if S and R are so related as subobjects of Y × X. Also, we write S^{∘} for the relation from X to Y which is the given S from Y to X seen as a subobject of X × Y.

Let ⟨e_{0}, e_{1}⟩ : E^{}^{}X × X be a relation from X to X. We say that E is reflexive if there exists a map r : X ^{}E satisfying e_{0}.r = e_{1}.r and we say that E is symmetric if there exists a map s : E ^{}E such that e_{0}.s = e_{1} and e_{1}.s = e_{0}.

Now let E ×_{X} E the pullback of e_{0} along e_{1}. We say that E is transitive if there exists a map t : E ×_{X} E ^{}E such that e_{0}.t = e_{0}.π_{0} and e_{1}.t = e_{1}.π_{1} (here π_{0} and π_{1} are the projections of the pullback E ×_{X} E).

An equivalence relation on X is a relation from X to X that is reflexive, symmetric and transitive. Notice that this definition makes sense in any category with finite limits. For example, kernel pairs are equivalence relations.

In order to define the exact completion of a category with finite limits we need a slightly more relaxed notion. A pseudo equivalence relation E on X is a (not necessarily jointly monic) pair of maps e_{0}, e_{1} : E ^{}X satisfying reflexivity, symmetry and transitivity as in the definition of equivalence relation above.

We say that an object P is projective if for every regular epi q : X [figure] Q and map f : P ^{}Q there exists a map g : P ^{}X such that q.g = f. We say that a category has enough projectives if for every object X there exists a projective object P and a regular epi P [figure] X.

Let C be a category with finite limits, the exact completion C_{ex} of C has objects the pseudo equivalence relations in C.

Let us denote a pseudo equivalence relation e_{0}, e_{1} : E ^{}X by X/E. For any other pseudo equivalence relation d_{0}, d_{1} : D ^{}Y, a map [f] : Y/D ^{}X/E in C_{ex} is an equivalence class of maps f : Y → X such that there exists an f′ : D → E and such that the two squares e_{0}.f′ = f.d_{0} and e_{1}.f′ = f.d_{1} commute. Two such maps f and g are equivalent if there exits an h : X_{0} → Y_{1} such that e_{0}.h = f and e_{1}.h = g.

The category C_{ex} is exact, it has enough projectives and C embeds into C_{ex} as the full subcategory of projectives. For any exact category E this embedding C ^{}C_{ex} induces an equivalence between the category of functors C ^{}E preserving finite limits and the category of exact functors C_{ex} ^{}E.

The regular completion C_{reg} of C can be defined to be the full subcategory of C_{ex} given by the equivalence relations in C that arise as a kernel pair. The category C_{reg} is regular and the embedding C ^{}C_{ex} factors through C_{reg}. For any regular category D this factorization induces an equivalence between the category of functors C ^{}D that preserve finite limits and the category of exact functors C_{reg} ^{}D.

In order to explain the construction of the exact completion D_{ex/reg} of a regular category D, we need to review some more results and definitions concerning relations.

In a regular category, relations can be composed as follows, if ⟨f_{Y} , f_{X}⟩ : R^{}^{}Y ×X and ⟨g_{Z}, g_{Y} ⟩ : S^{}^{}Z × Y are relations from Y to X and Z to Y respectively then their composition ⟨h_{Z}, h_{X}⟩ : SR^{}^{}Z × X from Z to X is defined as the mono part of the regular-epi/mono factorization of the rightmost map below.

S ×_{Y} R \overline{π_{R} ^{}}R  S ×_{Y} R  S ×_{Y} R

[figure: S; π_{S}; g_{Y}; Y; f_{Y}; SR; reg]

[figure: Z × X; ⟨h_{Z}, h_{X}⟩; Z × X; ⟨g_{Z}.π_{S}, f_{X}.π_{R}⟩]

Given equivalence relations D on Y and E on X we say that a relation F from Y to X is defined from D to E if DF E = F.

A relation F defined from D to E is total if D ≤ F F^{∘} and it is single valued if F^{∘}F ≤ E. A functional relation from D to E is a relation F defined from D to E that is total an single valued.

For example, for any D and E as above and a map [f] : Y/D ^{}X/E in D_{ex}, the relation DfE is a functional relation from D to E. Actually, DfE can be characterized as the unique functional relation F from D to E such that f ≤ F.

The category D_{ex/reg} has the equivalence relations in D as objects and the functional relations between them as maps. D_{ex/reg} is exact and there is an exact full and faithful functor D ^{}D_{ex/reg} such that, for every exact category E, it induces an equivalence between the category of exact functors from D to E and that of exact functors from D_{ex/reg} to E.

So the assignment of maps to functional relations mentioned above is an injective function D_{ex}(Y/D, X/E) ^{}D_{ex/reg}(Y/D, X/E).

Finally, the embedding of D into D_{ex/reg} preserves subobjects in the following sense. A functor F : D ^{}D′ preserves subobjects if it preserves monos and moreover, for

every X, the induced map Sub(X) ^{}Sub(F X) is an isomorphism.

3. Topologies in categories with finite limits

In this section we introduce the notion of topology on a category with finite limits C (all categories are assumed to be locally small) and then show that it corresponds to universal closure operators in the exact completion of C. (Recall the a universal closure operator on a category with finite limits is a natural (in X) transformation Sub(X) ^{}Sub(X) such that it is idempotent, monotone and inflationary with respect to the usual partial order of subobjects.)

3.1. Definition. Let C be a category with finite limits. A quasi-topology is a function J such that for every X in C, JX is a class of morphisms with codomain X subject to the following axioms:

Theory and Applications of Categories, Vol. 8, No. 21 526

(T1) every split epi with codomain X is in JX (T2) for f : Y ^{}X, if g ∈ JX then the pullback f^{∗}g of g along f is in JY (T3) let f : Y ^{}X in JX and g : Z ^{}X. If f^{∗}g ∈ JY then g ∈ JX

Equivalently, a quasi-topology can be described by the set of axioms below. (T1’) every identity id_{X} ∈ JX (T2) for f : Y → X, if g ∈ JX then f^{∗}g ∈ JY (T3’) if the composite g.h is in JX then g ∈ JX (T4’) if f : Y ^{}X ∈ JX and g ∈ JY then f.g ∈ JX

In order to characterize universal closure operators, we need an extra axiom which requires the following definition. 3.2. Definition. A map h : Z → X is closed with respect to a quasi-topology J if the following holds: for every f : Y → X, f^{∗}h ∈ JY implies that f factors through h.

Closed maps are closed under pullback and the following is also worth noting. 3.3. Lemma. Let J be a quasi-topology. Then the following are equivalent.

1. h is closed for J

2. for every commutative square as below,

[figure: g; f; h]

g in J implies that f factors through h

3. f^{∗}h in J implies that f^{∗}h is a split epi Proof. Routine.

The definition of closed map allows us to formulate the notion of topology.

3.4. Definition. A quasi-topology J is a topology if it holds that

(T) for every arrow f : Y → X there exists an g : V → W ∈ JW and a closed h : W → X such that f factors through h.g and h.g factors through f.

The main fact about topologies is the following.

3.5. Proposition. Let D be a regular category with enough projectives, such that the full subcategory P of projectives is closed under finite limits. Then there is a bijective correspondence between topologies on P and universal closure operators in D.

Proof. Assume first that we have a topology J on P. Any subobject U^{}^{}X in D of an object X in P appears as the image of some map f : Y ^{}X in P. Axiom (T) gives a closed map h : W ^{}X and we can define the closure of U to be the image of h. It is not difficult to show that this is well defined. As J-closed maps are closed under pullback we obtain a universal closure operator “on subobjects of objects from D”. We can then extend this restricted closure operator to an honest one using Barr-Kock’s Theorem as stated for example in Lemma 25.24 of [12].

In this way we obtain a universal closure operator in D such that for every projective X and U^{}^{}X, U is dense if and only if for some/any projective cover Y [figure] D, the composite Y ^{}X is a map in J. And also, U is closed if and only if Y ^{}X is J-closed.

Conversely, given a universal closure operator in D, we let J be the collection of maps in P whose image (in D) is dense. It is not difficult to show that a map in P is J-closed if and only if its image (in D) is closed for the given closure operator and that J is a quasi-topology.

To prove axiom (T), let f : X → Y and consider the following diagram in D where every square is a pullback.

[figure: V; reg; A; dense; W]

[figure: X; reg; reg; Im(f); reg; dense; \overline{Im(f)}; reg]

[figure: X; id; reg; Im(f); id; Y; closed]

Having in mind that the bottom line is the regular-epi/mono factorization of f, one should look at this diagram from the bottom right corner where we have the familiar facts that the closure of an object is closed and that the embedding of an object in its closure is dense.

The regular epi W [figure] \overline{Im(f)} is a chosen projective cover. The remaining squares are explained by the facts that, in D, regular epis and dense monos are closed under pullback.

Now, V is a pullback of arrows between projectives so it is projective because the embedding P ^{}D preserves finite limits.

Let g : V → W be the top composition and let h : W → Y be the right hand composition. So we have the needed arrows and the fact that h.g factors through f. As the map V [figure] X is a regular epi between projectives in D, it splits. So f factors through h.g.

To show that the constructions are one the inverse of the other one uses the fact that in the result of both cases the universal closure operator and the topology are related by the facts that a map is in the topology (resp. is J-closed) if and only if its image is dense (resp. is closed).

See Chapter 9 in [13] for details of the proof.

Let us instantiate this result to our main examples of regular categories with enough projectives.

3.6. Corollary. For any category with finite limits C there is a bijective correspondence between topologies on C and universal closure operators in C_{ex} and in C_{reg}.

The most immediate examples of topologies are the ones induced by stable factorization systems (E, M) satisfying T3’. For example, stable epi/regular-mono and stable regular-epi/mono factorizations induce topologies that we will study in more detail in Section 4. On the other hand, the axiom for a topology is weaker than the usual factorization property. We now present a class of examples that, in general, do not arise from factorization systems.

3.7. Oracle topologies. In [8] (section 17) it is attributed to Powell the observation that there is a connection between notions of degree and the forcing of decidability in recursive realizability. This observation finds a nice expression in the fact that the ∨-semilattice of Turing degrees embeds into the Heyting algebra of Lawvere-Tierney topologies in the effective topos Eff.

As Eff is the exact completion of the category PAss(K_{1}) of partitioned assemblies [17], it follows by Corollary 3.6 that the Lawvere-Tierney topologies in Eff can be presented in terms of topologies in our sense on the category PAss(K_{1}). We now show some examples of this. These examples also show non-trivial cases of the axiom (T) of Definition 3.4. First, let us quickly recall the definition of the category of partitioned assemblies.

3.8. Definition. For a partial combinatory algebra A, the category PAss(A) of partitioned assemblies is defined as follows.

Objects are pairs X = (|X|, ∥ ∥_{X}) such that |X| is a set and ∥ ∥_{X} : |X| → A is a function valued in the underlying set of the partial combinatory algebra. We usually omit subscripts.

Morphisms f : Y → X of partitioned assemblies are functions f : |Y | → |X| for which there exists an a ∈ A such that, for every y ∈ |Y |, a∥y∥ is defined and a∥y∥ = ∥fy∥. (Here juxtaposition of elements of the partial combinatory algebra denotes the corresponding application in the algebra.)

For any subset A ⊆ ℕ of the natural numbers we can consider the class of partial A-recursive functions [18], intuitively, those that in their process of computation can “ask an oracle whether a number is or not in A”.

For each X, let J_{A}(X) be the class of maps with codomain X that have an A-recursive section. That is, g : Z ^{}X is in J_{A}(X) if and only if there exists a function s : |X| ^{}|Z| that can be realized by a partial A-recursive function and such that |g|.s = id.

For every subset A ⊆ ℕ, J_{A} is a topology on PAss(K_{1}). The proof that it is a quasitopology is easy. On the other hand, one can prove axiom (T) using the ideas present in [8, 15, 14] where the associated closure operators are also discussed using different mechanisms to present them.

4. Separated objects and sheaves

Recall [1] that and object A is separated with respect to a universal closure operator if for every dense u : U^{}^{}X and map t : U ^{}A there exists at most one map k : X ^{}A such that k.u = t. We say that A is a sheaf if for every u and t as above, there exists a unique k such that k.u = t. Of course, every sheaf is separated.

We now explain how to identify separated objects and sheaves in C_{ex} using just the information in the topology.

4.1. Lemma. Let J be a topology on C and consider the universal closure operator induced in D where D is either C_{reg} or C_{ex}.

1. A is separated if and only if for every map f : Y ^{}X in J and every pair of maps g, h : X ^{}A, g.f = h.f implies that g = h (that is, A believes that maps in J are epi in D).

2. A is a sheaf if and only if for every map f : Y ^{}X in J with kernel pair f_{0}, f_{1} : K ^{}Y and map g : Y ^{}A such that g.f_{0} = g.f_{1} there exists a unique map g′ : X ^{}A such that g′.f = g (that is, A believes that maps in J are regular epis in D).

Proof. First one proves that an object is separated if and only if the condition holds for dense subobjects of projectives (i.e. of objects from C). Then it is easy to show that separatedness “with respect to projectives” is equivalent to the condition in the statement. The case for sheaves is analogous.

Universal closure operators are sometimes denoted by the letter j. For any category D equipped with such a j, we denote by Sep_{j}(D) and Sh_{j}(D) the full categories of D given by separated objects and sheaves respectively.

Let us now give a concrete description of the categories of separated objects. Given a topology J on a category C, we say that a pseudo equivalence relation p_{0}, p_{1} : X_{1} ^{}X_{0} is J-closed if the map ⟨p_{0}, p_{1}⟩ : X_{1} ^{}X_{0}×X_{0} is closed with respect to J (Definition 3.2).

For any topology J we say that a subclass S of the class of J-closed maps is sufficient if for every J-closed h : Y ^{}X there exists a map h′ : Y′ ^{}X in S such that h factors through h′ and h′ factors through h. Moreover, we say that a pseudo equivalence relation p_{0}, p_{1} : X_{1} ^{}X_{0} is S-closed if the map ⟨p_{0}, p_{1}⟩ : X_{1} ^{}X_{0} × X_{0} is in S.

We can now state a convenient way to describe categories of separated objects.

4.2. Lemma. Let J be a topology on a category C and let j be the induced universal closure operator in C_{ex}. Moreover, let S be a sufficient class of J-closed maps. Then Sep_{j}(C_{ex}) is equivalent to the full subcategory of C_{ex} given by the S-closed pseudo equivalence relations.

Proof. Use Lemma 4.1 plus the observation that every J-closed pseudo equivalence relation is isomorphic (as an object of C_{ex}) to an S-closed one.

We say that a topology on C is sep-subcanonical if every object of C is separated in C_{ex} (or equivalently in C_{reg}) with respect to the induced universal closure operator. We say that the topology is subcanonical if every object of C is a sheaf in C_{ex} (or C_{reg}).

4.3. Sep-canonical topologies. Let us here characterize sep-subcanonical topologies and relate them to regular completions.

4.4. Corollary. A topology J on C is sep-subcanonical if and only if every map in J is epi in C. Moreover, if C has stable epi/regular-mono factorizations then it has a largest sep-subcanonical topology.

Proof. Use Lemma 4.1 for the first part of the statement. For the second let JX be the class of all epi maps with codomain X. The stable factorizations imply axiom (T).

In the latter case, we call this topology the sep-canonical topology.

We say that an equivalence relation e_{0}, e_{1} : E ^{}X is regular if the induced mono ⟨e_{0}, e_{1}⟩ : E^{}^{}X × X is regular.

4.5. Corollary. If C has stable epi/regular-mono factorizations then the category of separated objects in C_{ex} for the sep-canonical topology is equivalent to the full subcategory of C_{ex} given by the regular equivalence relations.

Proof. It is not difficult to show that, in this case, the regular monos form a sufficient class of closed maps. Then the result follows by Lemma 4.2.

In [3] the category of separated objects for the ¬¬-topology in the Effective topos [8] is shown to be the regular completion of the category of partitioned assemblies. Similarly, in [19] it is shown that the category Equ of equilogical spaces is equivalent to (T_{0})_{reg}, the regular completion of the category of T_{0} topological spaces, and that it is also a category of separated objects of (T_{0})_{ex}. The fact that in these cases the regular completion appears as a category of separated objects of the exact completion is well explained by the following corollary.

4.6. Corollary. Let C have stable epi/regular-mono factorizations and be such that every regular equivalence relation is a kernel pair. Then C_{reg} is the category of separated objects in C_{ex} for the sep-canonical topology.

Proof. This follows from the characterization of the category of separated objects for the sep-canonical topology given in Corollary 4.5 and the description of C_{reg} as the category of kernel pairs in C (see [3]).

This may also be suggesting that, in general, it may be useful to consider the category of separated objects in C_{ex} for the sep-canonical topology rather than C_{reg} because, as a category of separated objects of an exact completion it will inherit better properties.

4.7. Canonical topologies. Regular epis on any locally small regular category induce a topology in our sense. In this section we study this topology and also characterize the sheaves in D_{ex} for it.

4.8. Corollary. A topology J on C is subcanonical if and only if every map in J is a regular epi in C. So, if D is a regular category then it has a largest subcanonical topology.

Proof. Use Lemma 4.1.

In the latter case, we call this topology the canonical topology and we denote it by can. It is easy to show that monos are closed and that the class of monos is sufficient. Then, by Lemma 4.2, Sep_{can}(D_{ex}) is equivalent to the full subcategory of D_{ex} given by the equivalence relations. But let us concentrate on the characterization of sheaves for this topology.

We will now introduce two definitions that characterize sheaves for the canonical topology on a regular category (see Section 6 for an explanation of the terminology).

4.9. Definition. An equivalence relation ⟨e_{0}, e_{1}⟩ : E^{}^{}X × X is Higgs-complete if for every equivalence relation ⟨d_{0}, d_{1}⟩ : D^{}^{}Y × Y and every functional relation ⟨f_{Y} , f_{X}⟩ : F^{}^{}Y × X from D to E there exists a map f : Y ^{}X such that f ≤ F (i.e. f induces F).

In other words, for F and f as above, there exists f′ : D ^{}E such that the following diagrams commute and such that DfE = F (here juxtaposition means composition of relations).

[figure: D; f′; E; Y; d_{0}; d_{1}; f; X; e_{0}; e_{1}]

Also, E on X is Higgs-complete if for every equivalence relation D, the inclusion D_{ex}(Y/D, X/E) ^{}D_{ex/reg}(Y/D, X/E) is actually an isomorphism.

(I believe the notion of Higgs-completeness is related to that of Cauchy-completeness as discussed in [10] and [20] but we will not pursue this here.)

4.10. Definition. An equivalence relation ⟨e_{0}, e_{1}⟩ : E^{}^{}X × X is complete if for every exact sequence d.d_{0} = d.d_{1} and maps f, \overline{f} such that f.d_{0} = e_{0}.\overline{f} and f.d_{1} = e_{1}.\overline{f} as in the left diagram below

[figure: D; \overline{f}; E; Y; k; E]

[figure: Y; d_{0}; d_{1}; f; X; e_{0}; e_{1}; Y × Z; ⟨id, d⟩; f × f′; X × X; ⟨e_{0}, e_{1}⟩]

Z [figure: d]

there exist maps f′ : Z ^{}X and k : Y ^{}E such that e_{0}.k = f and e_{1}.k = f′.d as in the right diagram above. In other words, f and f′.d induce the same morphism from D to E in the exact completion of the underlying category.

Notice that there are no functional relations involved in this definition. In order to motivate it let us say that an object Q is a quasi-sheaf if for every dense mono m : U^{}^{}Y and map f : U ^{}Q there exists a (not necessarily unique) f′ : Y ^{}Q such f′.m = f.

By the descriptions of exact completions and of canonical topologies, a map from a dense subobject of an object in D is given by a diagram as in Definition 4.10. It is easy to check that an equivalence relation E on X in D is a quasi-sheaf as an object in D_{ex} if and only if it is complete.

4.11. Lemma. Let D be a regular category. Then an equivalence relation in D (seen as an object Q in D_{ex}) is a sheaf for the canonical topology on D if and only if Q is a quasi-sheaf.

Proof. One direction is trivial. To show that Q a quasi-sheaf implies that Q is a sheaf we need only show that Q is separated. This is equivalent (see [1]) to the fact that Δ : Q^{}^{}Q × Q is closed. We now show that this is the case.

Let E^{}^{}X × X be the equivalence relation (in D) whose effective quotient is X [figure] Q. We then have the following pullback diagram in D_{ex}.

[figure: E; Q; X × X; q × q; Q × Q; Δ]

As D is regular, monos form a sufficient class of closed maps for the canonical topology, so E^{}^{}X × X is closed. As the square is a pullback and q × q is a regular epi, Δ is also closed.

One of the key results in the paper is the following.

4.12. Proposition. Let D be a regular category. Then the following categories are equivalent.

1. Sh_{can}(D_{ex})

2. the full subcategory of D_{ex} given by the complete equivalence relations

3. the full subcategory of D_{ex} given by the Higgs-complete equivalence relations

Proof. As sheaves are separated, every sheaf for the canonical topology is iso in D_{ex} to an equivalence relation (see remark below Corollary 4.8).

Lemma 4.11 is the equivalence between 1 and 2.

Now suppose that the equivalence relation E on X is complete and suppose that F = ⟨f_{Y} , f_{X}⟩ : F ^{}Y × X is a functional relation as in Definition 4.9. It is easy to show that f_{X} induces a map in D_{ex} from the object induced by the kernel pair of f_{Y} to that given by E. Completeness then provides a map f ≤ F.

Conversely, assume that E on X is Higgs-complete and suppose that the exact sequence d.d_{0} = d.d_{1} and maps f and \overline{f} are as in Definition 4.10. The objects induced by Z and by D on Y are iso in D_{ex/reg} so the map f induces a functional relation from Z to E on X. By Higgs-completeness there exists a map f′ : Z ^{}X inducing the functional relation. It follows that f and f′.d induce the same map from D to E.

See Corollary 10.4.8 in [13] for the details of the proof.

The definition of Higgs-completeness (Definition 4.9) implies that the full subcategories of D_{ex} and of D_{ex/reg} induced by the Higgs-complete equivalence relations are equivalent. Let us denote any of these equivalent categories by Ceq(D). So that we have embeddings Ceq(D) ^{}D_{ex/reg} and Ceq(D) ≃ Sh_{can}(D_{ex}) ^{}D_{ex}.

We now briefly discuss the category Ceq(D) from the perspective of its embedding into D_{ex/reg}.

4.13. Definition. Let D be a subcategory of D′. A map q : Y ^{}Q in D′ is Dprojecting if for every X in D and map g : X ^{}Q there exists a map f : X ^{}Y such that q.f = g.

The following lemma relates this notion with the sheaves for the canonical topology.

4.14. Lemma. An object Q in D_{ex/reg} is in Ceq(D) if and only if there exists an X in D and a D-projecting quotient X [figure] Q.

Proof. Let q : X [figure] Q be a regular epi and let e_{0}, e_{1} : E ^{}X be its kernel pair (an equivalence relation in D). So Q is the equivalence relation E seen as an object of D_{ex/reg}. It is not difficult to show that if E is Higgs-complete then q is D-projecting.

On the other hand, it is also not difficult to show that if q is D-projecting then E is complete. See Lemmas 10.5.2 and 10.5.3 in [13].

The following sums up some good properties of the category Ceq(D).

4.15. Proposition. If D is a regular category then Ceq(D) is regular and the embedding Ceq(D)^{}^{}D_{ex/reg} is exact and preserves subobjects.

Proof. Using Lemma 4.14 and the fact that D^{}^{}D_{ex/reg} preserves subobjects one proves that Ceq(D)^{}^{}D_{ex/reg} preserves subobjects. Using this and the facts that D^{}^{}D_{ex/reg} preserves finite limits and that projecting quotients are closed under pullback one shows that Ceq(D)^{}^{}D_{ex/reg} preserves finite limits. Again, using exactness of D^{}^{}D_{ex/reg} and preservation of subobjects of both D^{}^{}D_{ex/reg} and Ceq(D)^{}^{}D_{ex/reg}, one shows that Ceq(D) has stable regular-epi/mono factorizations and that the embedding into D_{ex/reg} preserves them. See Section 10.5 in [13].

Notice that as the embedding D ^{}D_{ex/reg} also preserves subobjects we obtain that the embedding D ^{}Ceq(D) does too.

The strong properties of the embedding Ceq(D) ^{}D_{ex/reg} have the following consequence.

4.16. Corollary. Ceq(D) is exact if and only if it is equivalent to D_{ex/reg}.

5. Local cartesian closure

We show how to derive local cartesian closure of certain subcategories of exact completions and relate this result to that in [2]. We recall very briefly here the fundamental result in the area.

5.1. Definition. Given maps f : X → J and α : J → I, a weak dependent product of f along α consists of a map ζ : Z ^{}I and a natural epi C/I( , ζ) [figure] C/J(α^{∗}( ), f). (See also Remark 3.2 in [5].)

The result in [5], specialized as in [2] to the setting where strong finite limits are assumed, is the following.

5.2. Proposition. C_{ex} is locally cartesian closed if and only if C has weak dependent products.

In [2], the authors were interested to apply this result to get local cartesian closure of many subcategories of C_{ex}. In particular, of the regular completion of the category of T_{0} topological spaces.

We will now show how to obtain a related result using the machinery described in this paper. The idea is to use Lemma 4.2 and obtain local cartesian closure as a general property of categories of separated objects.

Let j be a universal closure operator in a category with finite limits C. Then, for any X in C, j induces a universal closure operator j/X in the slice category C/X such that the following holds.

5.3. Lemma. If X is separated for j in C then Sep_{(j/X)}(C/X) ≅ (Sep_{j}C)/X. Moreover, if X is a sheaf then Sh_{(j/X)}(C/X) ≅ (Sh_{j}C)/X.

Proof. This is well known but we give a sketch of the proof (see Lemma 10.6.1 in [13] for details). For any map f : Y ^{}X in C, we denote the corresponding object of C/X by (Y, f). It is easy to see that m : (Y′, g) ^{}(Y, f) is mono in C/X if and only if m : Y′ ^{}Y is mono in C. Then we can define (j/X)m = jm ∈ Sub_{C/X}(Y, f). It is not difficult to show that (j/X) is a universal closure operator in C/X.

To show that Sep_{(j/X)}(C/X) is embedded in (Sep_{j}C)/X one shows that if a : A ^{}X is separated for (j/X) in (C/X) then A is separated in C for j. On the other hand, to show that (Sep_{j}C)/X embeds into Sep_{(j/X)}(C/X) one shows that for any separated A in C and any a : A ^{}X, a is separated for (j/X) in C/X. It is easy to show that the induced embeddings are inverse to each other so one obtains that Sep_{(j/X)}(C/X) ≅ (Sep_{j}C)/X. The case for sheaves is analogous.

It is well known (see for example the proof of Lemma V.2.1 in [11]) that if a category is cartesian closed then the categories of sheaves and of separated objects for any universal closure operator are also cartesian closed. In the case of separated objects for a universal closure operator this also follows from the preservation of products of the reflection functor [1] (this reflection functor does not exist in general for categories of sheaves).

5.4. Corollary. Let C have weak dependent products. Then for any topology J on C, the category of J-closed pseudo equivalence relations is locally cartesian closed.

Proof. By Proposition 5.2, C_{ex} is locally cartesian closed and by Lemma 4.2 the Jclosed pseudo equivalence relations form a subcategory of separated objects of C_{ex}.

This, in turn can be used to prove the local cartesian closure of regular completions. Indeed, if C has weak dependent products and satisfies the hypothesis of Corollary 4.6, it follows that C_{reg} is locally cartesian closed.

Let us compare these results with the approach in [2] to prove local cartesian closure of certain categories of pseudo equivalence relations. In their work, topologies in the sense of Definition 3.4 are not considered and results on categories of separated objects are not exploited. For any stable factorization system (E, M) in C they introduce the full subcategory PER(C, M) of C_{ex} given by the pseudo equivalence relations r_{1}, r_{2} : X_{1} ^{}X_{0} such that ⟨r_{1}, r_{2}⟩ : X_{1} ^{}X_{0} × X_{0} is in M. Then they show that the embedding of PER(C, M) into C_{ex} has a left adjoint which preserves products and commutes with pullbacks along maps in the subcategory. From this, it follows that if C_{ex} is locally cartesian closed then PER(C, M) also is.

Notice that when (E, M) satisfies T3’ then the factorization system is an example of our topologies and PER(C, M) is the associated category of separated objects by Lemma 4.2. Then the existence of the left adjoint satisfying the properties mentioned above follows from general facts about categories of separated objects (see [1]) and Lemma 5.3.

On the other hand, left adjoints to embeddings of categories of sheaves are not as easy to construct as in the case of separated objects. Indeed, enough injectives are usually required [1]. But we can still use our argument to prove the following.

5.5. Corollary. If D is a regular category with weak dependent products then Ceq(D) is locally cartesian closed.

Proof. Recall from Section 4.7 that Ceq(D) is equivalent to Sh_{can}(D_{ex}). So the result follows by the remark below Lemma 5.3.

This result will let us show the local cartesian closure of certain ex/reg completions in Section 6.

6. Complete equivalence relations and toposes

We will give, after some motivation and history, a characterization of when is Ceq(D) a topos.

It is well known that toposes of sheaves on a locale and realizability toposes arise non-trivially as ex/reg completions [6, 3, 12]. The topos of sheaves on a locale H is the ex/reg completion of the category H_{+} of H-valued sets which is, in turn, the coproduct completion of H (see 2.3.1 in [13] for a more concrete presentation). Realizability toposes are the ex/reg completions of the categories Ass of assemblies [3].

The strategy for the proofs of these facts given in [6] is simple: build the ex/reg completion and prove that it is a topos by showing that it has finite limits and power objects. No attempt is made to give conditions on a regular category for its ex/reg completion to be a topos.

In [12] there is an attempt to simplify the presentation. McLarty shows that in order to prove that the ex/reg completion of a regular category D is a topos it is enough to show that every object in D has a power object in D_{ex/reg} (actually, something slightly weaker). That is, in order to prove that D_{ex/reg} is a topos, one does not need to build all power objects, just a good class of them. This is a good simplification, yet, to use this fact, one still has to build the ex/reg completion and construct objects in it.

We will present a result that allows one to show that D_{ex/reg} is a topos merely by looking at the category D itself.

In order to motivate our proof, let us first briefly review Higgs’ construction of the category of sheaves on a locale [7].

Let H be a frame and consider the category 𝒮(H) defined as follows. Its objects are pairs X = (|X|, δ_{X}) with |X| a set and δ_{X} a function from |X| × |X| to H such that δ_{X}(x, x′) = δ_{X}(x′, x) and δ_{X}(x_{0}, x_{1}) ∧ δ_{X}(x_{1}, x_{2}) ≤ δ_{X}(x_{0}, x_{2}).

A map Y ^{}X between two such objects is a function f : |Y | × |X| ^{}H such that the following hold.

1. f(y, x) ∧ δ_{Y} (y, y′) ≤ f(y′, x) and f(y, x) ∧ δ_{X}(x, x′) ≤ f(y, x′)

2. f(y, x) ∧ f(y, x′) ≤ δ_{X}(x, x′)

3. ⋁_{x∈X} f(y, x) = δ_{Y} (y, y)

It turns out that this category is equivalent to the category of sheaves on the frame H. Let us outline a sketch of the proof. We use the terminology of [7]. We say that a map f : Y ^{}X is represented by a function f_{0} : |Y | ^{}|X| if f(y, x) ≤ δ_{X}(f_{0}y, x) for all y ∈ Y and x ∈ X.

Now define an object X to be ample if every map to X is represented by a function. There is functor from the category of sheaves on H to the category 𝒮(H) that assigns

to each sheaf an ample object. This property is used to prove that the functor is full and faithful. Then it is proved that every object in 𝒮(H) is isomorphic to one in the image of the embedding of sheaves.

In [9], this presentation of sheaves is used to motivate the definition of a tripos. In their treatment of geometric morphisms they introduce the notion of a weakly complete object which is very similar to the notion of an ample object. They prove is that every object in the topos induced by a tripos is isomorphic to a weakly complete one.

The resemblance of Higgs-completeness with ampleness (and also with weak completeness [9]) is evident.

We are going to borrow this idea from Higgs in order to prove our result. But first we need the following definition.

6.1. Definition. A generic mono in a category D is a mono τ : Υ^{}^{}Λ such that every mono u : U^{}^{}A in D arises as a pullback of τ (along a not necessarily unique map).

The following is a generalization of Higgs’ main idea about ampleness.

6.2. Lemma. If D is regular, locally cartesian closed and has a generic mono then every equivalence relation in D is isomorphic (as an object in D_{ex/reg}) to a complete one. That is, D_{ex/reg} ≃ Ceq(D).

Proof. The proof is essentially that of Proposition 3.3 in [9]. There is a more external version proved in the context of this paper in [13].

As the canonical embedding D ^{}D_{ex/reg} preserves finite limits, then the universal property of D_{ex} induces an exact functor a : D_{ex} ^{}D_{ex/reg} ≃ Sh_{can}(D_{ex}). This functor is easily seen to be left adjoint to the embedding Sh_{can}(D_{ex}) ^{}D_{ex}. So we have easily obtained an associated sheaf functor. Notice that as this functor preserves finite limits, we have another proof of local cartesian closure of D_{ex/reg} ≃ Sh_{can}(D_{ex}) ≃ Ceq(D).

6.3. Proposition. Let D be a locally cartesian closed regular category. Then Ceq(D) is a topos if and only if D has a generic mono. Moreover, in this case, Ceq(D) is equivalent to D_{ex/reg}.

Proof. Consider first the if direction. Our characterization of complete equivalence relations as a category of sheaves gives a cheap proof that Ceq(D) is locally cartesian closed (Corollary 5.5). So we need only prove that Ceq(D) has a subobject classifier. Given a generic mono τ : Υ ^{}Λ we think of Λ as a space of “propositions”. By Lemma 6.2, Ceq(D) is equivalent to D_{ex/reg} and so Ceq(D) is exact. We can then quotient Λ by the equivalence relation that relates two propositions if and only if they are equivalent. Denote this quotient by Ω. Using that Ω can be covered by a D-projecting quotient (Lemma 4.14) one proves that Ω is a subobject classifier.

For the only if direction let ⊤ : 1 ^{}Ω be the subobject classifier in Ceq(D). By Lemma 4.14 there exists a D-projecting quotient ρ : Λ [figure] Ω with Λ in D. Let τ = ρ^{∗}⊤ : Υ^{}^{}Λ. As D ^{}Ceq(D) preserves subobjects, Υ is in D. As ρ is D-projecting it is easy to see that τ is a generic mono in D.

By Corollary 4.16, Ceq(D) is equivalent to D_{ex/reg}.

It is very easy to check that the categories Ass of assemblies for a partial combinatory algebra and H_{+} of H-valued sets satisfy the premises of Proposition 6.3. This gives very simple presentations of realizability and localic toposes.

Realizability toposes can also be presented using exact completions [17, 13]. It is worth mentioning that those presentations require the axiom of choice in Set while the presentation using ex/reg completions does not.

It may be interesting to notice that, in general, it can be the case that Ceq(D) ≃ D_{ex/reg} is a topos while D_{ex} is not.

The reader should compare Proposition 6.3 with Theorem 4.2 in [16] which gives a characterization of the first order hyperdoctrines (over categories with finite products) whose associated category of partial equivalence relations is a topos. Using this result it is not difficult to prove the if direction of our Proposition 6.3 in the form: if D is a locally cartesian closed regular category with a generic mono then D_{ex/reg} is a topos.

7. Acknowledgements

I would like to thank Alex Simpson and Jaap van Oosten for helpful discussions. Paul Taylor’s diagrams package was used.

References

[1] M. Barr. On categories with effective unions. In Categorical algebra and its applications, Louvain-La-Neuve,1987, volume 1348 of Lecture notes in mathematics, pages 19–35. Springer, 1988.

[2] L. Birkedal, A. Carboni, G. Rosolini, and D. S. Scott. Type theory via exact categories. In Proceedings of 13th Annual Symposium on Logic in Computer Science, pages 188–198, 1998.

[3] A. Carboni. Some free constructions in realizability and proof theory. Journal of pure and applied algebra, 103:117–148, 1995.

[4] A. Carboni and S. Mantovani. An elementary characterization of categories of separated objects. Journal of pure and applied algebra, 89:63–92, 1993.

[5] A. Carboni and G. Rosolini. Locally cartesian closed exact completions. Journal of Pure and Applied Algebra, 154:103–116, 2000.

[6] P. J. Freyd and A. Scedrov. Categories, Allegories. North-Holland, 1990.

[7] D. Higgs. Injectivity in the topos of complete Heyting algebra valued sets. Canadian journal of mathematics, 3:550–568, 1984.

[8] J. M. E. Hyland. The effective topos. In The L. E. J. Brouwer Centenary Symposium, pages 165–216. North-Holland, 1982.

[9] J. M. E. Hyland, P.T. Johnstone, and A.M. Pitts. Tripos theory. Mathematical Proceedings of the Cambridge philosophical society, 88:205–232, 1980.

[10] F. W. Lawvere. Metric spaces, generalized logic and closed categories. Rendiconti del Seminario Matematico e Fisico di Milano, 43:135–166, 1973.

[11] S. Mac Lane and I. Moerdijk. Sheaves in Geometry and Logic: a First Introduction to Topos Theory. Universitext. Springer Verlag, 1992.

[12] C. McLarty. Elementary categories, elementary toposes. Oxford Science Publications, 1995.

[13] M. Menni. Exact completions and toposes. PhD thesis, University of Edinburgh,

2000. Available from http://www.dcs.ed.ac.uk/~matias/.

[14] J. van Oosten. Fibrations and calculi of fractions. Journal of pure and applied algebra, 146:77–102, 2000.

[15] W. K. S. Phoa. Relative computability in the effective topos. Mathematical Proceedings of the Cambridge philosophical society, 106:419–422, 1989.

[16] A. M. Pitts. Tripos theory in retrospect. To appear in Mathematical structures in computer science.

[17] E. Robinson and G. Rosolini. Colimit completions and the effective topos. The Journal of Symbolic Logic, 55(2):678–699, June 1990.

[18] H. Rogers Jr. Theory of recursive functions and effective computability. McGraw-Hill, 1967. Reissued by MIT Press, 1987.

[19] G. Rosolini. Equilogical spaces and filter spaces. Rendiconti del Circolo Matematico di Palermo (Serie II), 64, 2000.

[20] R. F. C. Walters. Sheaves on sites as cauchy-complete categories. Journal of pure and applied algebra, 24:95–102, 1982.

LFCS, Division of Informatics, University of Edinburgh,

JCMB, King’s Buildings, Edinburgh, EH9 3JZ

Email: matias@dcs.ed.ac.uk

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/n21/n21.{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