nLab regular and exact completions


The forgetful 2-functors

have left adjoints, and in fact are (2-)monadic. Their left adjoints are called (free) regular or exact completions.

In the third case the 2-monad is idempotent, so the left adjoint can properly be called a completion, while in the first two cases, the 2-monad is only lax-idempotent, so the left adjoint should technically be called a free completion. However, the phrases regular completion and exact completion are also commonly used for the first two cases. To disambiguate the second and third cases the phrases ex/lex completion and ex/reg completion are also used, and so by analogy the first case is called reg/lex completion.

In fact, the reg/lex and ex/lex completion can be applied to a category that merely has weak finite limits, although in this case they are not left adjoint to the obvious forgetful functor. A general context which includes all of these types of these completions is the 2-category of unary sites, in which the categories of regular and exact categories form reflective sub-2-categories.


The ex/lex completion

There are several constructions of the ex/lex completion. Perhaps the quickest one to state (Hu-Tholen 1996) is that if CC is small, then C ex/lexC_{ex/lex} is the full subcategory of its presheaf category Set C opSet^{C^{op}} spanned by those presheaves FF such that

  • FF admits a regular epimorphism y(X)Fy(X)\twoheadrightarrow F from a representable presheaf,
  • with the additional property that if Ky(X)K\rightrightarrows y(X) is the kernel pair of y(X)Fy(X)\twoheadrightarrow F, then KK also admits a regular epi y(Z)Ky(Z)\to K from a representable presheaf.

A more explicit construction is as follows. Let us think, informally, of the objects of CC as presets and the morphisms of CC as “proofs”. An object of C ex=C ex/lexC_{ex} = C_{ex/lex} will then be a “set” or setoid constructed from CC. Precisely, we take the objects of C exC_{ex} to be the pseudo-equivalence relations in CC: a pseudo-equivalence relation consists of:

  • an object XCX\in C and
  • a parallel pair s,t:RXs,t\colon R\rightrightarrows X, such that
  • there exists an arrow i:XRi\colon X\to R with si=ti=1 Xs i = t i = 1_X,
  • there exists an arrow v:RRv\colon R\to R with sv=ts v = t and tv=st v = s, and
  • there exists an arrow c:R× XRRc\colon R\times_X R \to R with sc=sπ 1s c = s \pi_1 and tc=tπ 2t c = t \pi_2. (If CC has merely weak finite limits, we assert this for some, and hence every, weak pullback R× X wRR\times^w_X R.)

If (s,t):RX×X(s,t)\colon R\to X\times X is a monomorphism, then these conditions make it precisely a congruence or internal equivalence relation in CC. In general, we can think of the fiber of RR over (x 1,x 2)(x_1,x_2) as giving a collection of “reasons” or “proofs” that x 1Rx 2x_1 \mathrel{R} x_2. Then ii supplies a uniform proof that xRxx \mathrel{R} x for every xx, while vv supplies a uniform proof that xRyx \mathrel{R} y implies yRxy \mathrel{R} x, and cc supplies a uniform proof that xRyx \mathrel{R} y and yRzy \mathrel{R} z imply xRzx \mathrel{R} z.

If RXR\rightrightarrows X and SYS\rightrightarrows Y are two pseudo-equivalence relations, a morphism between them in C exC_{ex} is defined to be a morphism f:XYf\colon X\to Y in CC, such that there exists a morphism f 1:RSf_1\colon R\to S with sf 1=fss f_1 = f s and tf 1=ftt f_1 = f t. That is, f 1f_1 supplies a uniform proof that if xRyx \mathrel{R} y then f(x)Sf(y)f(x) \mathrel{S} f(y). Moreover, we declare two such morphisms f,g:XYf,g\colon X\to Y to be equal if there exists a morphism h:XSh\colon X\to S such that sh=fs h = f and th=gt h = g (that is, a uniform proof that f(x)Sg(x)f(x) \mathrel{S} g(x)). Because SYS\rightrightarrows Y is a pseudo-equivalence relation, this defines an actual equivalence relation on the morphisms f:XYf\colon X\to Y, which is compatible with composition; thus we have a well-defined category C exC_{ex}.

We have a full and faithful functor CC exC\to C_{ex} sending an object XX to the pseudo-equivalence relation XXX\rightrightarrows X. One can then verify directly that C exC_{ex} is exact, that this embedding preserves finite limits, and that it is universal with respect to lex functors from CC into exact categories.

There are also other constructions. Of course, the ex/lex completion can also be obtained by composing (any construction of) the reg/lex completion with (any construction of) the ex/reg completion.

The reg/lex completion

The reg/lex completion C reg=C reg/lexC_{reg}= C_{reg/lex} of a lex category CC is perhaps most succinctly described as the subcategory of C exC_{ex} consisting of those objects which admit monomorphisms into objects of CC. That is, instead of adding all quotients of pseudo-equivalence relations in CC, we only add those quotients which are necessary in order to be able to construct images of morphisms in CC. For many construction of C exC_{ex}, this idea can then be made more explicit and sometimes simplified.

For instance, if we regard C exC_{ex} as a full subcategory of Set C opSet^{C^{op}} as above, then we can likewise regard C regC_{reg} as the full subcategory of Set C opSet^{C^{op}} determined by those presheaves FF such that

  • FF admits a regular epimorphism y(X)Fy(X) \twoheadrightarrow F from a representable presheaf, and
  • FF admits a monomorphism Fy(Z)F\rightarrowtail y(Z) into a representable presheaf.

If we construct C exC_{ex} using pseudo-equivalence relations, as above, then we can characterize the pseudo-equivalence relations which we need to form C regC_{reg} as precisely the kernel pairs of morphisms of CC (or finite families of such). Therefore, we obtain an equivalent definition of C regC_{reg} as follows. Its objects are morphisms of CC (regarded as stand-ins for their formally added images). A morphism from p:XYp\colon X\to Y to q:ZWq\colon Z\to W should be a morphism f:XZf\colon X\to Z for which there exists an f 1f_1 relating the kernel of pp to the kernel of qq, modulo an equivalence relation generated by maps from XX to the kernel of qq. But by definition of kernel pairs, two morphisms will be identified under this latter equivalence relation if and only if they have the same composite with qq, so it makes sense to define the morphisms of C regC_{reg} from p:XYp\colon X\to Y to q:ZWq\colon Z\to W to be certain morphisms f¯:XW\overline{f}\colon X\to W which factor through qq (non-uniquely). We still have to impose the condition that ff should preserve the kernel pairs, but in terms of f¯\overline{f} this is simply the statement that f¯r=f¯s\overline{f} r = \overline{f} s, where (r,s)(r,s) is the kernel pair of pp. This is the definition of C regC_{reg} given in the Elephant.

We can then verify that C regC_{reg} is regular, that we have a full and faithful functor CC regC\to C_{reg}, which preserves finite limits, and is universal among lex functors from CC to regular categories. Again, there are also other constructions.

Also, just as for the free exact completion, the construction works essentially the same if CC has only weak finite limits. In this case, instead of the objects of C exC_{ex} admitting a monomorphism to a single object of CC, we have to consider those admitting a jointly-monic finite family of morphisms into objects of CC, with similar modifications for the other descriptions.

The ex/reg completion

If CC is regular, a quick definition of C ex/regC_{ex/reg} is as the full subcategory of the category Sh(C)Sh(C) of sheaves for the regular coverage on CC spanned by those sheaves which are quotients of congruences in CC. (Lack 1999)

A more explicit description can be obtained by first passing from CC to its allegory of internal relations, then splitting the idempotents which are equivalence relations in CC, and finally reconstructing a regular category from the resulting allegory. Yet more explicitly, this means that the objects of C ex/regC_{ex/reg} are congruences in CC, and the morphisms are relations which are entire and functional relative to the given congruences.

The higher categorical approach

A somewhat more unified approach to all these completions can be obtained as follows. Observe that in the classical situation (that is, in the presence of choice), sets can be identified with all of the following:

  • 0-trivial groupoids, i.e. groupoids in which any two parallel morphisms are equal, i.e. equivalence relations.
  • 0-trivial 2-groupoids, i.e. 2-groupoids in which any two parallel 2-morphisms are equal and any two parallel 1-morphisms are isomorphic.
  • and so on…
  • 0-trivial n-groupoids for any 0n0\le n \le \infty.

In the absence of choice, this is still true as long as the morphisms between 0-trivial n-groupoids are nn-anafunctors. If instead we consider only actual functors, however, in the absence of choice what we obtain are various completions of SetSet. Specifically:

  • Set reg/lexSet_{reg/lex} can be identified with the category whose objects are 0-trivial groupoids, and whose morphisms are natural isomorphism classes of functors.
  • Set ex/lexSet_{ex/lex} can be identified with the category whose objects are 0-trivial 2-groupoids, and whose morphisms are pseudonatural equivalence classes of 2-functors. In the notion of 2-groupoid here we also demand that each 1-cell be equipped with a specified inverse equivalence.

This idea can be generalized to provide alternate constructions of the completions for an arbitrary CC with finite limits. The notions of internal nn-category and internal nn-functor in such a CC make perfect sense for any nn. The same is true of the notion of nn-groupoid, as long as we interpret this to mean the structure of “inverse-assigning” morphisms in CC. The statement “any two parallel nn-cells are equal” also makes sense in any lex category, since it demands that a certain specified morphism is monic. Finally, we can also interpret “any two parallel kk-cells are equivalent” algebraically by specifying a particular equivalence between any such pair. (Note that for k=(n1)k=(n-1), since parallel nn-cells are equal there is a unique way to do this.) We thereby obtain a notion of internal 0-trivial nn-groupoid in any lex category, and we write 0trivnGpd(C)0 triv n Gpd(C) for the category of such things and internal nn-natural equivalence classes of functors. We then have:

  • It is fairly clear from the above explicit description that C reg/lexC_{reg/lex} is the full subcategory of 0triv1Gpd(C)0 triv 1 Gpd(C) determined by the kernel pairs (which are congruences, i.e. internal 0-trivial 1-groupoids). If, like SetSet, CC is already exact, so that every congruence is a kernel pair, then C reg/lex0triv1Gpd(C)C_{reg/lex}\simeq 0 triv 1 Gpd(C).

  • C ex/lexC_{ex/lex} is always equivalent to 0triv2Gpd(C)0 triv 2 Gpd(C). To see this, note that a pseudo-equivalence relation (together with chosen maps ii, cc, and vv) can be regarded as the 1-skeleton of an internal bicategory in CC with specified inverse equivalences for every 1-cell. There is then a unique way to add 2-cells to make it a 0-trivial bigroupoid.

It is not clear how 0-trivial nn-groupoids fit into this picture for n>2n\gt 2, although it seems likely that the objects of iterated reg/lex and ex/lex completions can be identified with some type of internal n-fold category.

Now if CC is already regular, then we can define a notion of internal anafunctor between internal nn-categories. It is then easily seen that

  • C ex/regC_{ex/reg} is equivalent to the category of 0-trivial 1-groupoids, and natural isomorphism classes of internal anafunctors between them.

Again, it is not entirely clear how the 0-trivial nn-groupoids and anafunctors behave for n>1n\gt 1, although it seems fairly likely (to me) that in this case the process will stabilize at n=1n=1, i.e. 0-trivial nn-groupoids with equivalence classes of ana-nn-functors will give C ex/regC_{ex/reg} for all n1n\ge 1.

Completions of unary sites

The descriptions of the ex/lex and ex/reg completions in terms of pseudo-equivalence relations and equivalence relations, respectively, have a common generalization. Let CC be a unary site, so that it has a notion of “covering morphism” and admits “finite local unary prelimits”. In particular, any cospan XZYX\to Z\leftarrow Y has a local unary pre-pullback, which is a commutative square

P Y X Z \array{ P & \to & Y \\ \downarrow && \downarrow\\ X & \to & Z }

such that for any other commutative square

V Y X Z \array{ V & \to & Y \\ \downarrow && \downarrow\\ X & \to & Z }

there is a cover UVU\to V and a map UPU\to P such that the induced composites UXU\to X and UYU\to Y are equal.

Now we can define a unary congruence in CC to consist of:

  • An object XCX\in C

  • A parallel pair s,t:RXs,t:R\rightrightarrows X, such that

  • There exists a cover p:YXp:Y\to X and a map i:YRi:Y\to R with si=ti=ps i = t i = p,

  • There exists a cover q:SRq:S\to R and a map v:SRv:S\to R with sv=tqs v = t q and tv=sqt v = s q, and

  • There exists a local unary pre-pullback TT of the cospan RtXsRR \xrightarrow{t} X \xleftarrow{s} R and an arrow c:TRc:T\to R such that sc=sπ 1s c = s \pi_1 and tc=tπ 2t c = t \pi_2, where π 1\pi_1 and π 2\pi_2 are the projections of TT to RR.

If CC has a trivial topology, then local unary prelimits are simply weak limits, and this reduces to the definition of pseudo-equivalence relation. On the other hand, if CC is regular with its regular topology, then these conditions ensure exactly that the image of RX×XR\to X\times X is an internal equivalence relation on XX.

Now we can define morphisms between unary congruences using a suitable kind of either entire and functional relations or anafunctors, and obtain the exact completion of the unary site CC. This construction exhibits the 2-category of exact categories as a reflective sub-2-category of the 2-category of unary sites, and restricts to the ex/wlex and ex/reg completions on the sub-2-categories of categories with weak finite limits and trivial topologies and of regular categories with regular topologies, respectively. It can also be modified to construct regular completions. See (Shulman) for details.

Generalizations to higher arity

More generally, any ∞-ary site has a κ\kappa-ary exact completion, which is a ∞-ary exact category. This exhibits the 2-category of κ\kappa-ary exact categories as a reflective sub-2-category of that of κ\kappa-ary sites. See (Shulman) for details. In particular:

Properties of regular and exact completions

Many categorical properties of interest are preserved by one or more of the regular and exact completions. That is, if CC has these properties, then so does the completion, and the inclusion functor preserves them. Note that frequently, for a completion to have some structure, it suffices for CC to have a “weak” version of that structure.

  • Of course, finite limits are preserved by all three completions. In fact, as we have remarked, for the ex/lex and reg/lex completions, CC need only have weak finite limits.

  • CC is lextensive if and only if C ex/lexC_{ex/lex} is, and if and only if C reg/lexC_{reg/lex} is, and in this case the embeddings preserve coproducts (Menni 2000). It follows that if CC is a pretopos, then so is C ex/lexC_{ex/lex}, although the inclusion CC ex/lexC\to C_{ex/lex} is not a “pretopos functor” as it does not preserve regular epis.

  • If CC is lextensive and has coequalizers (and hence has finite colimits), then so do C ex/lexC_{ex/lex} and C reg/lexC_{reg/lex} (Menni 2000). However, the inclusion functors do not preserve coequalizers. In fact, it suffices for CC to be lextensive with quasi-coequalizers, meaning that for every f,g:YXf,g\colon Y\rightrightarrows X there exists q:XQq\colon X\to Q with qf=qgq f = q g, such that for any h:XZh\colon X\to Z with hf=hgh f = h g, hh coequalizes the kernel pair of qq.

  • The categories C reg/lexC_{reg/lex} and C ex/lexC_{ex/lex} always have enough (regular) projectives. In fact, the objects of CC are precisely the projective objects of these categories. Moreover, an exact category DD is of the form C ex/lexC_{ex/lex} for some CC (with weak finite limits) if and only if it has enough projectives, in which case of course CC can be taken to be the subcategory of projectives (Carboni–Vitale 1998). Note that if DD has enough projectives, then its subcategory of projectives always has weak finite limits. Similarly, a regular category DD is of the form C reg/lexC_{reg/lex} for some CC (with weak finite limits) if and only if it has enough projectives and every object can be embedded in a projective one.

  • If CC is a regular category satisfying the “regular” axiom of choice (i.e. every regular epi splits), then it is equivalent to C reg/lexC_{reg/lex}, and hence the latter also satisfies the axiom of choice. Similarly, if CC is exact and satisfies choice, then it is equivalent to C ex/lexC_{ex/lex}. Conversely, if the inclusion CC reg/lexC\to C_{reg/lex} or CC ex/lexC\to C_{ex/lex} is an equivalence, then since the objects of CC are projective in these completions, CC must satisfy the axiom of choice.

    In fact, if we assume merely that C ex/lex(C ex/lex) ex/lexC_{ex/lex} \to (C_{ex/lex})_{ex/lex} is a equivalence, then since the objects of C ex/lexC_{ex/lex} are projective in (C ex/lex) ex/lex(C_{ex/lex})_{ex/lex}, they must also all be projective in C ex/lexC_{ex/lex}, and therefore CC ex/lexC\to C_{ex/lex} is also an equivalence. It follows by induction that if the sequence of iterations of () ex/lex(-)_{ex/lex} stabilizes at any finite stage, it must in fact stabilize at the very beginning and CC must satisfy the axiom of choice. A similar argument applies to the reg/lex completion. (The ex/reg completion, of course, always stabilizes after one application.)

  • Cartesian closure is preserved by the ex/lex completion (Carboni–Rosolini 2000). In fact, C ex/lexC_{ex/lex} is cartesian closed if and only if CC has weak simple products, meaning weak dependent product?s along product projections.

  • Local cartesian closure is also preserved by the ex/lex completion (Carboni–Rosolini 2000). In fact, C ex/lexC_{ex/lex} is locally cartesian closed if and only if CC is weakly locally cartesian closed, meaning that each slice category has weak dependent products. It follows in particular that if CC is a Π-pretopos, then so is C ex/lexC_{ex/lex}. For each Π\Pi-pretopos CC we thus obtain a sequence CC, C exC_{ex}, (C ex) ex(C_{ex})_{ex}, … of Π\Pi-pretopoi, which in general does not stabilize.

  • (Local) cartesian closure is seemingly not always preserved by the reg/lex completion, but it is under certain hypotheses. Recalling that C reg/lexC_{reg/lex} is the full subcategory of C ex/lexC_{ex/lex} consisting of the kernel pairs, suppose that CC has pullback-stable (epi,regular mono) factorizations and that every regular congruence is a kernel pair. Then C reg/lexC_{reg/lex} is reflective in C ex/lexC_{ex/lex} (BCRS 1998, Menni 2000): the reflection of a pseudo-equivalence relation RXR\rightrightarrows X is its (epi,regular mono) factorization. Moreover, the reflection preserves products, and also pullbacks along maps in C reg/lexC_{reg/lex}, from which it follows that if C ex/lexC_{ex/lex} is cartesian closed or locally cartesian closed, so is C reg/lexC_{reg/lex}.

    Thus, if CC is weakly cartesian closed (resp. weakly locally cartesian closed), has pullback-stable (epi,regular mono) factorizations, and every regular congruence is a kernel pair, then C reg/lexC_{reg/lex} is cartesian closed (resp. locally cartesian closed). In particular, the local versions of these hypotheses apply in particular to Top and to any quasitopos. Note that Top reg/lexTop_{reg/lex} is called the category of equilogical spaces.

  • If CC is lextensive with coequalizers (or “quasi-coequalizers”) and a strong-subobject classifier, then so is C reg/lexC_{reg/lex} (Menni 2000). It follows that if CC is a lextensive quasitopos, then so is C reg/lexC_{reg/lex}. For each lextensive quasitopos CC we thus obtain a sequence CC, C regC_{reg}, (C reg) reg(C_{reg})_{reg}, … of lextensive quasitopoi, which in general does not stabilize.

  • If CC has a natural numbers object, then so do C reg/lexC_{reg/lex} and C ex/lexC_{ex/lex}. (Does C ex/regC_{ex/reg}? What about more general W-types?)

  • If CC is a ΠW-pretopos, then so is C ex/lexC_{ex/lex} (see vandenBerg, Theorem 1.1).

  • C ex/lexC_{ex/lex} is an elementary topos iff CC has weak dependent products and a generic proof (Menni2000). Note that if CC is a topos satisfying the axiom of choice, then its subobject classifier is a generic proof. It follows that in this case C ex/lexC_{ex/lex} is a topos—but we already knew that, because C ex/lexC_{ex/lex} is equivalent to CC for such a CC.

  • Expanding on the last point, for a presheaf topos C=Set D opC = Set^{D^{op}}, the category C ex/lexC_{ex/lex} is a topos iff DD is a groupoid (Menni2000).

  • If CC is regular, locally cartesian closed, and has a generic mono, i.e. a monomorphism τ:ϒΛ\tau\colon \Upsilon\to \Lambda such that every monomorphism is a pullback of τ\tau (not necessarily uniquely), then C ex/regC_{ex/reg} is a topos (Menni2000).

  • If CC is an additive category, then C ex/lexC_{ex/lex} is an abelian category.

On the other hand, some properties are not preserved by the completions.

  • Of course, all the completions are regular categories, but the inclusions are not regular functors, since they do not preserve regular epis.

  • We have seen that the existence of a subobject classifier or power objects is not, in general, preserved by the completions (although if CC is a topos, then of course so is C ex/regC_{ex/reg}, since it is equivalent to CC).

  • Similarly, if CC is well-powered, it does not follow that C reg/lexC_{reg/lex} or C ex/lexC_{ex/lex} are. In particular, for XCX\in C, the subobject preorders Sub C reg/lex(X)Sub_{C_{reg/lex}}(X) and Sub C ex/lex(X)Sub_{C_{ex/lex}}(X) are equivalent to the preorder reflection of the slice category C/XC/X, and it is easy to construct examples in which this is not essentially small1.

  • If CC is a coherent category, it does not follow that C ex/lexC_{ex/lex} or C reg/lexC_{reg/lex} is. However, if CC is additionally lextensive, we have seen above that so are these completions, and hence in particular also coherent (any extensive regular category is coherent). One can also write down the “free coherent completion” and the “free pretopos completion” of a lex category, and the “pretopos completion” of a coherent category; see familial regularity and exactness for some clues on how to proceed.

  • If CC is a Heyting category, it does not follow that C ex/lexC_{ex/lex} or C reg/lexC_{reg/lex} is. However, if CC is additionally lextensive and locally cartesian closed, we have seen above that so are these completions, and hence Heyting (any lextensive locally cartesian closed regular category is Heyting).

  • Unsurprisingly, if CC is a Boolean category, it does not follow that C ex/lexC_{ex/lex} or C reg/lexC_{reg/lex} is, even if CC is lextensive and LCC so that its completions are Heyting.

    In fact, a stronger statement is true: if CC is lextensive and regular, then C reg/lexC_{reg/lex} and C ex/lexC_{ex/lex} are Boolean if and only if CC satisfies the axiom of choice (in which case they are of course equivalent to CC). More precisely, if XCX\in C is such that every subobject of XX in C reg/lexC_{reg/lex} is complemented, then XX is projective in CC. (The same argument applies to C ex/lexC_{ex/lex}.) For suppose that p:YXp\colon Y\to X is a regular epi in CC. Recall that Sub C reg/lex(X)Sub_{C_{reg/lex}}(X) is the preorder reflection of C/XC/X. Thus pp, considered as an object of C/XC/X, defines a monomorphism in C reg/lexC_{reg/lex}. By assumption, this monic is complemented; let its complement be represented by q:ZXq\colon Z\to X. Since complements are disjoint, and meets in Sub C reg/lex(X)Sub_{C_{reg/lex}}(X) are given by pullbacks in C/XC/X, the pullback of pp and qq admits a morphism to the initial object 00, and hence is itself initial since CC is extensive. Now pp is regular epi, hence so is its pullback 0Z0\to Z. But in a lextensive regular category, disjointness of the coproduct 1+11+1 implies that 010\to 1 is the equalizer of of the coprojections 11+11\rightrightarrows 1+1, and therefore any epimorphism with domain 00 is an isomorphism; thus ZZ is also initial. Now since joins in Sub C reg/lex(X)Sub_{C_{reg/lex}}(X) are given by coproducts in C/XC/X, the induced map Y+ZXY+Z \to X must become an isomorphism in Sub C reg/lex(X)Sub_{C_{reg/lex}}(X), which means that it must admit a section; but since ZZ is initial this means that pp itself has a section.

  • If CC is well-pointed, it does not follow that C ex/lexC_{ex/lex} or C reg/lexC_{reg/lex} are (in the stronger sense appropriate for non-toposes). It is of course always true that 11 is projective in the completions. And if CC is lextensive, so that its completions are coherent, then 11 is indecomposable in them as soon as it is so in CC. However, it does not follow that 11 is a strong generator in the completions even if it is so in CC, since the completions have (in general) many more monomorphisms than CC does.

    If CC is a well-pointed topos such that C ex/lexC_{ex/lex} is also a topos, then the latter cannot be well-pointed unless CC satisfies AC, because the completion would then be Boolean, and hence AC holds by the proof above.


(to be written…)

  • The category Set of Bishop sets is the ex/lex completion of the category of hSets in a theory without quotients.

  • Realizability toposes arise as ex/lex completions of categories of partitioned assemblies based on a partial combinatory algebra AA. In fact the reg/lex completion gives, as an interesting intermediate step, the category of assemblies based on AA (which turns out to be the quasitopos of ¬¬\neg\neg-separated objects inside the realizability topos). This is discussed in Menni.

  • The category TFTF of torsion-free abelian groups is regular, but not exact. For instance, the congruence {(a,b)|abmod2}×\{ (a,b) | a \equiv b \mod 2 \} \subseteq \mathbb{Z}\times\mathbb{Z} is not a kernel in TFTF. Unsurprisingly, the ex/reg completion of TFTF is equivalent to the category AbAb of all abelian groups.

    Note that although TFTF is not exact, its inclusion into AbAb does have a left adjoint (quotient by torsion), and thus TFTF is cocomplete. Herein lies a subtle trap for the unwary: since the ex/reg completion monad is idempotent, it is in particular lax-idempotent, which means that any left adjoint to the unit CC ex/regC \hookrightarrow C_{ex/reg} is in fact a (pseudo) algebra structure; but since the monad is actually idempotent, any algebra structure is an equivalence. Of course, the reflection AbTFAb \to TF is not an equivalence, which doesn’t contract the general facts because this left adjoint is not a regular functor, and hence not an adjunction in the 2-category on which the monad () ex/reg(-)_{ex/reg} lives. In fact, it is not hard to check that CC ex/regC \hookrightarrow C_{ex/reg} has a left adjoint in CatCat if and only if CC has coequalizers of congruences (while if it has a left adjoint in RegReg then it must be an equivalence).

  • A free cocompletion of a (possibly large) finitely complete category, i.e., the category of small presheaves on CC, is the ex/lex completion of the free coproduct completion of CC. This appears as Lemma 3 here.


  • Carboni and Celia Magno, “The free exact category on a left exact one”, J. Austral. Math. Soc. (Ser. A), 1982.

  • Jiří Rosický, Cartesian closed exact completions, JPAA 142 no. 3 (October 1999), 261-270. (doi00146-7))

  • Hu and Tholen, “A note on free regular and exact completions and their infinitary generalizations”, TAC 1996.

  • Aurelio Carboni, Enrico Vitale, Regular and exact completions, Journal of Pure and Applied Algebra 125 1–3 (1998) 79-116 (doi:10.1016/S0022-4049(96)00115-6)

  • Birkedal and Carboni and Rosolini and Scott, “Type Theory via Exact Categories,” 1998

  • Stephen Lack, “A note on the exact completion of a regular category, and its infinitary generalizations” TAC 1999.

  • The Elephant, Sections A1.3 and A3.

  • Carboni and Rosolini, “Locally cartesian closed exact completions”, JPAA 2000

  • Matías Menni, “Exact completions and toposes,” Ph.D. Thesis, University of Edinburgh, 2000. (web)

  • Michael Shulman, “Exact completions and small sheaves”. Theory and Applications of Categories, Vol. 27, 2012, No. 7, pp 97-173. Free online

  1. For example, let C=Set C = Set^{\bullet \rightrightarrows \bullet} be the topos of directed graphs. For each ordinal α\alpha, let G αG_\alpha be the directed graph whose nodes are elements of α\alpha and with a directed edge from β\beta to γ\gamma if β<γ\beta \lt \gamma in α\alpha. Then in the poset reflection Pos(C)Pos(C), we have a class of proper monomorphisms, e.g., [G α]<[G α][G_\alpha] \lt [G_{\alpha'}] whenever α<α\alpha \lt \alpha'. Thus Pos(C)Pos(C) is a large poset. This example also shows that Pos(C)Pos(C) need not be a total category even if CC is.

Last revised on January 11, 2024 at 19:48:46. See the history of this page for a list of all contributions to it.