nLab
regular and exact completions

Regular and exact completions

Idea

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.

Constructions

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 C is small, then C ex/lex is the full subcategory of its presheaf category Set C op spanned by those presheaves F such that

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

  • an object XC and
  • a parallel pair s,t:RX, such that
  • there exists an arrow i:XR with si=ti=1 X,
  • there exists an arrow v:RR with sv=t and tv=s, and
  • there exists an arrow c:R× XRR with sc=sπ 1 and tc=tπ 2. (If C has merely weak finite limits, we assert this for some, and hence every, weak pullback R× X wR.)

If (s,t):RX×X is a monomorphism, then these conditions make it precisely a congruence or internal equivalence relation in C. In general, we can think of the fiber of R over (x 1,x 2) as giving a collection of “reasons” or “proofs” that x 1Rx 2. Then i supplies a uniform proof that xRx for every x, while v supplies a uniform proof that xRy implies yRx, and c supplies a uniform proof thath xRy and yRz imply xRz.

If RX and SY are two pseudo-equivalence relations, a morphism between them in C ex is defined to be a morphism f:XY in C, such that there exists a morphism f 1:RS with sf 1=fs and tf 1=ft. That is, f 1 supplies a uniform proof that if xRy then f(x)Sf(y). Moreover, we declare two such morphisms f,g:XY to be equal if there exists a morphism h:XS such that sh=f and th=g (that is, a uniform proof that f(x)Sg(x)). Because SY is a pseudo-equivalence relation, this defines an actual equivalence relation on the morphisms f:XY, which is compatible with composition; thus we have a well-defined category C ex.

We have a full and faithful functor CC ex sending an object X to the pseudo-equivalence relation XX. One can then verify directly that C ex is exact, that this embedding preserves finite limits, and that it is universal with respect to lex functors from C 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/lex of a lex category C is perhaps most succinctly described as the subcategory of C ex consisting of those objects which admit monomorphisms into objects of C. That is, instead of adding all quotients of pseudo-equivalence relations in C, we only add those quotients which are necessary in order to be able to construct images of morphisms in C. For many construction of C ex, this idea can then be made more explicit and sometimes simplified.

For instance, if we regard C ex as a full subcategory of Set C op as above, then we can likewise regard C reg as the full subcategory of Set C op determined by those presheaves F such that

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

If we construct C ex using pseudo-equivalence relations, as above, then we can characterize the pseudo-equivalence relations which we need to form C reg as precisely the kernel pairs of morphisms of C (or finite families of such). Therefore, we obtain an equivalent definition of C reg as follows. Its objects are morphisms of C (regarded as stand-ins for their formally added images). A morphism from p:XY to q:ZW should be a morphism f:XZ for which there exists an f 1 relating the kernel of p to the kernel of q, modulo an equivalence relation generated by maps from X to the kernel of q. 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 q, so it makes sense to define the morphisms of C reg from p:XY to q:ZW to be certain morphisms f¯:XW which factor through q (non-uniquely). We still have to impose the condition that f should preserve the kernel pairs, but in terms of f¯ this is simply the statement that f¯r=f¯s, where (r,s) is the kernel pair of p. This is the definition of C reg given in the Elephant.

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

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

The ex/reg completion

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

A more explicit description can be obtained by first passing from C to its allegory of internal relations, then splitting the idempotents which are equivalence relations in C, and finally reconstructing a regular category from the resulting allegory. Yet more explicitly, this means that the objects of C are congruences in C, 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 0n.

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

  • Set 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/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 C with finite limits. The notions of internal n-category and internal n-functor in such a C make perfect sense for any n. The same is true of the notion of n-groupoid, as long as we interpret this to mean the structure of “inverse-assigning” morphisms in C. The statement “any two parallel n-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 k-cells are equivalent” algebraically by specifying a particular equivalence between any such pair. (Note that for k=(n1), since parallel n-cells are equal there is a unique way to do this.) We thereby obtain a notion of internal 0-trivial n-groupoid in any lex category, and we write 0trivnGpd(C) for the category of such things and internal n-natural equivalence classes of functors. We then have:

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

  • C ex/lex is always equivalent to 0triv2Gpd(C). To see this, note that a pseudo-equivalence relation (together with chosen maps i, c, and v) can be regarded as the 1-skeleton of an internal bicategory in C 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 n-groupoids fit into this picture for n>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 C is already regular, then we can define a notion of internal anafunctor between internal n-categories. It is then easily seen that

  • C 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 n-groupoids and anafunctors behave for n>1, although it seems fairly likely (to me) that in this case the process will stabilize at n=1, i.e. 0-trivial n-groupoids with equivalence classes of ana-n-functors will give C ex/reg for all n1.

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 C be a unary site, so that it has a notion of “covering morphism” and admits “finite local unary prelimits”. In particular, any cospan XZY 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 UV and a map UP such that the induced composites UX and UY are equal.

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

  • An object XC

  • A parallel pair s,t:RtotoX, such that

  • There exists a cover p:YX and a map i:YR with si=ti=p,

  • There exists a cover q:SR and a map v:SR with sv=tq and tv=sq, and

  • There exists a local unary pre-pullback T of the cospan RtXsR and an arrow c:TR such that sc=sπ 1 and tc=tπ 2, where π 1 and π 2 are the projections of T to R.

If C 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 C is regular with its regular topology, then these conditions ensure exactly that the image of RX×X is an internal equivalence relation on X.

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 C. 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 κ-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:

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 C 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 C 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, C need only have weak finite limits.

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

  • If C is lextensive and has coequalizers (and hence has finite colimits), then so do C ex/lex and C reg/lex (Menni 2000). However, the inclusion functors do not preserve coequalizers. In fact, it suffices for C to be lextensive with quasi-coequalizers, meaning that for every f,g:YX there exists q:XQ with qf=qg, such that for any h:XZ with hf=hg, h coequalizes the kernel pair of q.

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

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

    In fact, if we assume merely that C ex/lex(C ex/lex) ex/lex is a equivalence, then since the objects of C ex/lex are projective in (C ex/lex) ex/lex, they must also all be projective in C ex/lex, and therefore CC ex/lex is also an equivalence. It follows by induction that if the sequence of iterations of () ex/lex stabilizes at any finite stage, it must in fact stabilize at the very beginning and C 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/lex is cartesian closed if and only if C 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/lex is locally cartesian closed if and only if C is weakly locally cartesian closed, meaning that each slice category has weak dependent products. It follows in particular that if C is a Π-pretopos, then so is C ex/lex. For each Π-pretopos C we thus obtain a sequence C, C ex, (C ex) ex, … 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 C reg/lex is the full subcategory of C ex/lex consisting of the kernel pairs, suppose that C has pullback-stable (epi,regular mono) factorizations and that every regular congruence is a kernel pair. Then C reg/lex is reflective in C ex/lex (BCRS 1998, Menni 2000): the reflection of a pseudo-equivalence relation RX is its (epi,regular mono) factorization. Moreover, the reflection preserves products, and also pullbacks along maps in C reg/lex, from which it follows that if C ex/lex is cartesian closed or locally cartesian closed, so is C reg/lex.

    Thus, if C 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/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/lex is called the category of equilogical spaces.

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

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

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

  • If C 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 C ex/reg 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 C is a topos, then of course so is C ex/reg, since it is equivalent to C).

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

  • If C is a coherent category, it does not follow that C ex/lex or C reg/lex is. However, if C 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 C is a Heyting category, it does not follow that C ex/lex or C reg/lex is. However, if C 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 C is a Boolean category, it does not follow that C ex/lex or C reg/lex is, even if C is lextensive and LCC so that its completions are Heyting.

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

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

    Of course, if C is a well-pointed topos such that C ex/lex is also a topos, then the latter is also well-pointed, since any generator in a topos is a strong generator.

Examples

(to be written…)

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

  • The category TF of torsion-free abelian groups is regular, but not exact. For instance, the congruence {(a,b)abmod2}× is not a kernel in TF. Unsurprisingly, the ex/reg completion of TF is equivalent to the category Ab of all abelian groups.

    Note that although TF is not exact, its inclusion into Ab does have a left adjoint (quotient by torsion), and thus TF 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/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 AbTF 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 lives. In fact, it is not hard to check that CC ex/reg has a left adjoint in Cat if and only if C has coequalizers of congruences (while if it has a left adjoint in Reg then it must be an equivalence).

References

  • 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)

  • 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 be the topos of directed graphs. For each ordinal α, let G α be the directed graph whose nodes are elements of α and with a directed edge from β to γ if β<γ in α. Then in the poset reflection Pos(C), we have a class of proper monomorphisms, e.g., [G α]<[G α] whenever α<α. Thus Pos(C) is a large poset. This example also shows that Pos(C) need not be a total category even if C is.

Revised on March 12, 2013 17:13:27 by Todd Trimble (67.81.93.26)