Recall that there is a 2-category of homwise-discrete categories in any finitely complete 2-category . We write for its full sub-2-category spanned by the -congruences (always we take 2, (2,1), (1,2), or 1). Recall that there is a functor sending each object to its kernel; if is an -category then the image of is contained in .
Suppose that has finite limits. Then: 1. has finite limits. 1. is closed under finite limits in . 1. is 2-fully-faithful (that is, an equivalence on hom-categories) and preserves finite limits.
It suffices to deal with finite products, inserters, and equifiers. Evidently is a terminal object. If and are homwise-discrete categories, define and ; it is easy to check that then is a homwise-discrete category that is the product in . Since , and products preserve ffs, we see that is an -congruence if and are and that preserves products.
For inserters, let be functors in , define by the pullback
and define by the pullback
where is the “object of commutative squares in .” Then is a homwise-discrete category and is an inserter of . Also, is an -congruence if is, and preserves inserters.
Finally, for equifiers, suppose we have functors and 2-cells in , represented by morphisms such that . Let be the universal morphism equipped with an isomorphism such that is the given isomorphism (this is a finite limit in .) Note that since is discrete, is ff. Now let ; then is a homwise-discrete category and is an equifier of and in . Also is an -congruence if is, and preserves equifiers.
For any morphism in , is the functor that consists of and . A transformation between and is a morphism whose composites are and ; but this is just a transformation in . Thus, is homwise fully faithful. And homwise essential-surjectivity follows from the essential uniqueness of thin structures, or equivalently a version of Prop 6.4 in FBMF.
Moreover, we have:
If is an -category with finite limits, then is regular.
It is easy to see that a functor between -congruences is ff in iff the square
is a pullback in .
We claim that if is a functor such that is split (that is, for some ), then is eso in . For if for some ff as above, then we have with , and so the fact that is a pullback induces a functor with and . But this implies is an equivalence; thus is eso.
Moreover, if is split, then the same is true for any pullback of . For the pullback of along some is given by a where ; here is the “object of isomorphisms” in . What matters is that the projection has a splitting given by combining the splitting of with the “identities” morphism .
Now suppose that is any functor in . It is easy to see that if we define and let be the pullback
then where and are the obvious functors. Moreover, clearly is ff, and satisfies the condition above, so any pullback of it is eso. It follows that if itself were eso, then it would be equivalent to , and thus any pullback of it would also be eso; hence esos are stable under pullback.
Since is ff, the kernel of is the same as the kernel of , so to prove regular it remains only to show that is a quotient of that kernel. If denotes , then is the comma object and thus we can calculate
Therefore, if is equipped with an action by , then the action 2-cell is given by a morphism , and the action axioms evidently make this into a functor . Thus, is a quotient of , as desired.
However, there are three problems with the 2-category .
The solution to the first problem is straightforward. If is a 2-category with finite limits, define to be the sub-2-category of spanned by the 2-congruences which occur as kernels of morphisms in . If is an -category then any such kernel is an -congruence, so in this case is contained in and is an -category. Also, clearly factors through .
For any finitely complete 2-category , the 2-category is regular, and the functor induces an equivalence
for any regular 2-category .
Here denotes the 2-category of regular functors, transformations, and modifications between two regular 2-categories, and likewise denotes the 2-category of finite-limit-preserving functors, transformations, and modifications between two finitely complete 2-categories.
It is easy to verify that is closed under finite limits in , and also under the eso-ff factorization constructed in Theorem 1; thus it is regular. If is a lex functor where is regular, we extend it to by sending to the quotient in of , which exists since is regular. It is easy to verify that this is regular and is the unique regular extension of .
To solve the second and third problems with , we need to modify its morphisms.
Recall that 2-congruences in can be identified with certain double categories. As noted in PAPDC, edge-symmetric double categories with a thin structure are essentially the same as 2-categories, and homwise-discreteness makes them the same as 1-categories. Our lack of edge-symmetry means that we really have a 1-category with distinguished subclass of morphisms (the vertical ones), which must be preserved by functors between congruences. (Note that the transformations are “horizontal” and need not have distinguished components. Since every vertical arrow has a horizontal companion, any vertical transformation is represented by a horizontal one.) In order to eliminate the effect of the distinguished vertical morphisms, we can replace functors between congruences by anafunctors.
Suppose that is a finitely complete 2-site and that , , and are 2-congruences in . A functor is a weak equivalence if 1. the square
is a pullback, and 1. is a cover (a one-element covering family). An anafunctor is a span of functors such that is a weak equivalence.
The primary example we have in mind is when is a regular 2-category with its regular coverage, but it is useful to consider the general case.
If and are anafunctors between 2-congruences, then a transformation is a transformation between the two induced functors .
(Here denotes the pullback in .)
For any subcanonical and finitely complete 2-site (such as a regular -category with its regular coverage), there is a finitely complete 2-category of 2-congruences, anafunctors, and transformations in . It contains as a homwise-full sub-2-category (that is, is ff) closed under finite limits.
Composition is, of course, by pullback. Since covers are stable under pullback and composition, the composite of anafunctors is again an anafunctor. The coverage must be subcanonical in order to define the vertical composite of natural transformations. We regard a functor as an anafunctor by taking to be the identity; it is then clear that a transformation between functors is the same as a transformation between their corresponding anafunctors.
It is easy to see that products in remain products in . Before dealing with inserters and equifiers, we observe that if is an anafunctor in and is any eso, then pulling back to defines a new congruence and an anafunctor which is isomorphic to the original in . Thus, if and are parallel anafunctors in , by pulling them both back to we may assume that they are defined by spans with the same first leg, i.e. we have .
Now, for the inserter of and as above, let be the inserter of in . It is easy to check that the composite is an inserter of in . Likewise, given with and as above, we have transformations between the two functors in , and it is again easy to check that their equifier in is again the equifier in of the original 2-cells . Thus, has finite limits. Finally, by construction clearly the inclusion of preserves finite limits.
We write for the full sub-2-category of on the -congruences, which is a finitely complete -category. Of course, it contains as a homwise-full sub--category closed under finite limits, and when is an -category we have .
If is a subcanonical finitely complete -site, then the functor is 2-fully-faithful. If is an -exact -category equipped with its regular coverage, then is an equivalence of 2-categories.
Since is 2-fully-faithful and is homwise fully faithful, is homwise fully faithful. For homwise essential-surjectivity, suppose that is an anafunctor. Then is a cover and is the pullback of along it; but this just says that . The functor consists of morphisms and , and functoriality says precisely that the resulting 2-cell equips with an action by the congruence . But since is precisely the kernel of , which is a cover in a subcanonical 2-site and hence the quotient of this kernel, we have an induced morphism in . It is then easy to check that is isomorphic, as an anafunctor, to . Thus, is homwise an equivalence.
Now suppose that is an -exact -category and that is an -congruence. Since is -exact, has a quotient , and since is the kernel of , we have a functor which is a weak equivalence. Thus, we can regard it either as an anafunctor or , and it is easy to see that these are inverse equivalences in . Thus, is essentially surjective, and hence an equivalence.
Note that by working in the generality of 2-sites, this construction includes the previous one. Specifically, if is a finitely complete 2-category equipped with its minimal coverage, in which the covering families are those that contain a split epic, then . This is immediate from the proof of Theorem 1, which implies that the first leg of any anafunctor relative to this coverage is both eso and ff in , and hence an equivalence.
We also remark in passing that this allows us to reconstruct 2-exact 2-categories with enough groupoids or discretes from their subcategories of such.
If is a 2-exact 2-category with enough groupoids, then . Likewise, if is 2-exact and has enough discretes, then .
Define a functor by taking each object to the kernel of where is eso and is groupoidal (for example, it might be the core of ). Note that this kernel lives in since is discrete, hence is also groupoidal. The same argument as in Theorem 4 shows that this functor is 2-fully-faithful for any regular 2-category with enough groupoids, and essentially-surjective when is 2-exact; thus it is an equivalence. The same argument works for discrete objects.
In particular, the 2-exact 2-categories having enough discretes are precisely the 2-categories of internal categories and anafunctors in 1-exact 1-categories.
Our final goal is to construct the -exact completion of a regular -category, and a first step towards that is the following.
If is a regular -category, so is . The functor is regular, and moreover for any -exact 2-category it induces an equivalence
We already know that has finite limits and preserves finite limits. The rest is very similar to Theorem 1. We first observe that an anafunctor is an equivalence as soon as is also a weak equivalence (its reverse span then provides an inverse.) Also, is ff if and only if
is a pullback.
Now we claim that if is an anafunctor such that is eso, then is eso. For if we have a composition
such that is ff, then being eso implies that is also eso; thus is a weak equivalence and so is an equivalence. Moreover, by the construction of pullbacks in , anafunctors with this property are stable under pullback.
Now suppose that is any anafunctor, and define and let be the pullback of to along . Then is an -congruence, is ff in and thus also in , and factors through . (In fact, is the image of in .) The kernel of can equally well be calculated as the kernel of , which is the same as the kernel of .
Finally, given any with an action by this kernel, we may as well assume (by pullbacks) that (which leaves unchanged up to equivalence). Then since the kernel acting is the same as the kernel of , regularity of gives a descended functor . Thus, is the quotient of its kernel; so is regular.
Finally, if is -exact, then any functor induces one , but , so we have our extension, which it can be shown is unique up to equivalence.
When is a regular 1-category, it is well-known that (which, in that case, is the category of internal equivalence relations and functional relations) is the 1-exact completion of (the reflection of from regular 1-categories into 1-exact 1-categories). Theorem 6 shows that in general, will be the -exact completion of whenver it is -exact. However, in general for we need to “build up exactness” in stages by iterating this construction.
It is possible that the iteration will converge at some finite stage, but for now, define and let .
For any regular -category , is an -exact -category and there is a 2-fully-faithful regular functor that induces an equivalence
for any -exact 2-category .
Sequential colimits preserve 2-fully-faithful functors as well as functors that preserve finite limits and quotients, and the final statement follows easily from Theorem 6. Thus it remains only to show that is -exact. But for any -congruence in , there is some such that and both live in , and thus so does the congruence since sits 2-fully-faithfully in preserving finite limits. This congruence in is then an object of which supplies a quotient there, and thus also in .