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.
There are several constructions of the ex/lex completion. Perhaps the quickest one to state (Hu-Tholen 1996) is that if is small, then is the full subcategory of its presheaf category spanned by those presheaves such that
A more explicit construction is as follows. Let us think, informally, of the objects of as presets and the morphisms of as “proofs”. An object of will then be a “set” or setoid constructed from . Precisely, we take the objects of to be the pseudo-equivalence relations in : a pseudo-equivalence relation consists of:
If is a monomorphism, then these conditions make it precisely a congruence or internal equivalence relation in . In general, we can think of the fiber of over as giving a collection of “reasons” or “proofs” that . Then supplies a uniform proof that for every , while supplies a uniform proof that implies , and supplies a uniform proof thath and imply .
If and are two pseudo-equivalence relations, a morphism between them in is defined to be a morphism in , such that there exists a morphism with and . That is, supplies a uniform proof that if then . Moreover, we declare two such morphisms to be equal if there exists a morphism such that and (that is, a uniform proof that ). Because is a pseudo-equivalence relation, this defines an actual equivalence relation on the morphisms , which is compatible with composition; thus we have a well-defined category .
We have a full and faithful functor sending an object to the pseudo-equivalence relation . One can then verify directly that is exact, that this embedding preserves finite limits, and that it is universal with respect to lex functors from 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 of a lex category is perhaps most succinctly described as the subcategory of consisting of those objects which admit monomorphisms into objects of . That is, instead of adding all quotients of pseudo-equivalence relations in , we only add those quotients which are necessary in order to be able to construct images of morphisms in . For many construction of , this idea can then be made more explicit and sometimes simplified.
For instance, if we regard as a full subcategory of as above, then we can likewise regard as the full subcategory of determined by those presheaves such that
If we construct using pseudo-equivalence relations, as above, then we can characterize the pseudo-equivalence relations which we need to form as precisely the kernel pairs of morphisms of (or finite families of such). Therefore, we obtain an equivalent definition of as follows. Its objects are morphisms of (regarded as stand-ins for their formally added images). A morphism from to should be a morphism for which there exists an relating the kernel of to the kernel of , modulo an equivalence relation generated by maps from to the kernel of . 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 , so it makes sense to define the morphisms of from to to be certain morphisms which factor through (non-uniquely). We still have to impose the condition that should preserve the kernel pairs, but in terms of this is simply the statement that , where is the kernel pair of . This is the definition of given in the Elephant.
We can then verify that is regular, that we have a full and faithful functor , which preserves finite limits, and is universal among lex functors from to regular categories. Again, there are also other constructions.
Also, just as for the free exact completion, the construction works essentially the same if has only weak finite limits. In this case, instead of the objects of admitting a monomorphism to a single object of , we have to consider those admitting a jointly-monic finite family of morphisms into objects of , with similar modifications for the other descriptions.
A more explicit description can be obtained by first passing from to its allegory of internal relations, then splitting the idempotents which are equivalence relations in , and finally reconstructing a regular category from the resulting allegory. Yet more explicitly, this means that the objects of are congruences in , and the morphisms are relations which are entire and functional relative to the given congruences.
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:
In the absence of choice, this is still true as long as the morphisms between 0-trivial n-groupoids are -anafunctors. If instead we consider only actual functors, however, in the absence of choice what we obtain are various completions of . Specifically:
This idea can be generalized to provide alternate constructions of the completions for an arbitrary with finite limits. The notions of internal -category and internal -functor in such a make perfect sense for any . The same is true of the notion of -groupoid, as long as we interpret this to mean the structure of “inverse-assigning” morphisms in . The statement “any two parallel -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 -cells are equivalent” algebraically by specifying a particular equivalence between any such pair. (Note that for , since parallel -cells are equal there is a unique way to do this.) We thereby obtain a notion of internal 0-trivial -groupoid in any lex category, and we write for the category of such things and internal -natural equivalence classes of functors. We then have:
It is fairly clear from the above explicit description that is the full subcategory of determined by the kernel pairs (which are congruences, i.e. internal 0-trivial 1-groupoids). If, like , is already exact, so that every congruence is a kernel pair, then .
is always equivalent to . To see this, note that a pseudo-equivalence relation (together with chosen maps , , and ) can be regarded as the 1-skeleton of an internal bicategory in 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 -groupoids fit into this picture for , 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 is already regular, then we can define a notion of internal anafunctor between internal -categories. It is then easily seen that
Again, it is not entirely clear how the 0-trivial -groupoids and anafunctors behave for , although it seems fairly likely (to me) that in this case the process will stabilize at , i.e. 0-trivial -groupoids with equivalence classes of ana--functors will give for all .
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 be a unary site, so that it has a notion of “covering morphism” and admits “finite local unary prelimits”. In particular, any cospan has a local unary pre-pullback, which is a commutative square
such that for any other commutative square
there is a cover and a map such that the induced composites and are equal.
Now we can define a unary congruence in to consist of:
A parallel pair , such that
There exists a cover and a map with ,
There exists a cover and a map with and , and
There exists a local unary pre-pullback of the cospan and an arrow such that and , where and are the projections of to .
If 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 is regular with its regular topology, then these conditions ensure exactly that the image of is an internal equivalence relation on .
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 . 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.
More generally, any κ-ary site has a -ary exact completion, which is a κ-ary exact category. This exhibits the 2-category of -ary exact categories as a reflective sub-2-category of that of -ary sites. See (Shulman) for details. In particular:
Many categorical properties of interest are preserved by one or more of the regular and exact completions. That is, if 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 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, need only have weak finite limits.
is lextensive if and only if is, and if and only if is, and in this case the embeddings preserve coproducts (Menni 2000). It follows that if is a pretopos, then so is , although the inclusion is not a “pretopos functor” as it does not preserve regular epis.
If is lextensive and has coequalizers (and hence has finite colimits), then so do and (Menni 2000). However, the inclusion functors do not preserve coequalizers. In fact, it suffices for to be lextensive with quasi-coequalizers, meaning that for every there exists with , such that for any with , coequalizes the kernel pair of .
The categories and always have enough (regular) projectives. In fact, the objects of are precisely the projective objects of these categories. Moreover, an exact category is of the form for some (with weak finite limits) if and only if it has enough projectives, in which case of course can be taken to be the subcategory of projectives (Carboni–Vitale 1998). Note that if has enough projectives, then its subcategory of projectives always has weak finite limits. Similarly, a regular category is of the form for some (with weak finite limits) if and only if it has enough projectives and every object can be embedded in a projective one.
If is a regular category satisfying the “regular” axiom of choice (i.e. every regular epi splits), then it is equivalent to , and hence the latter also satisfies the axiom of choice. Similarly, if is exact and satisfies choice, then it is equivalent to . Conversely, if the inclusion or is an equivalence, then since the objects of are projective in these completions, must satisfy the axiom of choice.
In fact, if we assume merely that is a equivalence, then since the objects of are projective in , they must also all be projective in , and therefore is also an equivalence. It follows by induction that if the sequence of iterations of stabilizes at any finite stage, it must in fact stabilize at the very beginning and 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, is cartesian closed if and only if 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, is locally cartesian closed if and only if is weakly locally cartesian closed, meaning that each slice category has weak dependent products. It follows in particular that if is a Π-pretopos, then so is . For each -pretopos we thus obtain a sequence , , , … of -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 is the full subcategory of consisting of the kernel pairs, suppose that has pullback-stable (epi,regular mono) factorizations and that every regular congruence is a kernel pair. Then is reflective in (BCRS 1998, Menni 2000): the reflection of a pseudo-equivalence relation is its (epi,regular mono) factorization. Moreover, the reflection preserves products, and also pullbacks along maps in , from which it follows that if is cartesian closed or locally cartesian closed, so is .
Thus, if 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 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 is called the category of equilogical spaces.
If is lextensive with coequalizers (or “quasi-coequalizers”) and a strong-subobject classifier, then so is (Menni 2000). It follows that if is a lextensive quasitopos, then so is . For each lextensive quasitopos we thus obtain a sequence , , , … of lextensive quasitopoi, which in general does not stabilize.
is an elementary topos iff has weak dependent products and a generic proof (Menni 2000). Note that if is a topos satisfying the axiom of choice, then its subobject classifier is a generic proof. It follows that in this case is a topos—but we already knew that, because is equivalent to for such a .
If is regular, locally cartesian closed, and has a generic mono, i.e. a monomorphism such that every monomorphism is a pullback of (not necessarily uniquely), then is a topos (Menni 2000).
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 is a topos, then of course so is , since it is equivalent to ).
Similarly, if is well-powered, it does not follow that or are. In particular, for , the subobject preorders and are equivalent to the preorder reflection of the slice category , and it is easy to construct examples in which this is not essentially small1.
If is a coherent category, it does not follow that or is. However, if 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 is a Heyting category, it does not follow that or is. However, if 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 is a Boolean category, it does not follow that or is, even if is lextensive and LCC so that its completions are Heyting.
In fact, a stronger statement is true: if is lextensive and regular, then and are Boolean if and only if satisfies the axiom of choice (in which case they are of course equivalent to ). More precisely, if is such that every subobject of in is complemented, then is projective in . (The same argument applies to .) For suppose that is a regular epi in . Recall that is the preorder reflection of . Thus , considered as an object of , defines a monomorphism in . By assumption, this monic is complemented; let its complement be represented by . Since complements are disjoint, and meets in are given by pullbacks in , the pullback of and admits a morphism to the initial object , and hence is itself initial since is extensive. Now is regular epi, hence so is its pullback . But in a lextensive regular category, disjointness of the coproduct implies that is the equalizer of of the coprojections , and therefore any epimorphism with domain is an isomorphism; thus is also initial. Now since joins in are given by coproducts in , the induced map must become an isomorphism in , which means that it must admit a section; but since is initial this means that itself has a section.
If is well-pointed, it does not follow that or are (in the stronger sense appropriate for non-toposes). It is of course always true that is projective in the completions. And if is lextensive, so that its completions are coherent, then is indecomposable in them as soon as it is so in . However, it does not follow that is a strong generator in the completions even if it is so in , since the completions have (in general) many more monomorphisms than does.
If is a well-pointed topos such that is also a topos, then the latter cannot be well-pointed unless satisfies AC, because the completion would then be Boolean, and hence AC holds by the proof above.
(to be written…)
Realizability toposes arise as ex/lex completions of categories of partitioned assemblies based on a partial combinatory algebra . In fact the reg/ex completion gives, as an interesting intermediate step, the category of assemblies based on (which turns out to be the quasitopos of -separated objects inside the realizability topos). This is discussed in Menni.
The category of torsion-free abelian groups is regular, but not exact. For instance, the congruence is not a kernel in . Unsurprisingly, the ex/reg completion of is equivalent to the category of all abelian groups.
Note that although is not exact, its inclusion into does have a left adjoint (quotient by torsion), and thus 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 is in fact a (pseudo) algebra structure; but since the monad is actually idempotent, any algebra structure is an equivalence. Of course, the reflection 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 lives. In fact, it is not hard to check that has a left adjoint in if and only if has coequalizers of congruences (while if it has a left adjoint in then it must be an equivalence).
Carboni and Celia Magno, “The free exact category on a left exact one”, J. Austral. Math. Soc. (Ser. A), 1982.
Hu and Tholen, “A note on free regular and exact completions and their infinitary generalizations”, TAC 1996.
Carboni and Vitale, “Regular and exact completions”, JPAA 1998.
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)
For example, let be the topos of directed graphs. For each ordinal , let be the directed graph whose nodes are elements of and with a directed edge from to if in . Then in the poset reflection , we have a class of proper monomorphisms, e.g., whenever . Thus is a large poset. This example also shows that need not be a total category even if is. ↩