The correct notions of regularity and exactness for 2-categories is one of the subtler parts of the theory of first-order structure. In particular, we need a suitable replacement for the 1-categorical notion of equivalence relation. The (almost) correct definition was probably first written down in StreetCBS.
One way to express the idea is that in an -category, every object is internally a -category; exactness says that conversely every “internal -category” is represented by an object. When , an “internal 0-category” means an internal equivalence relation; thus exactness for 1-categories says that every equivalence relation is a kernel (i.e. is represented by some object). Thus, we need to find a good notion of “internal 1-category” in a 2-category.
Of course, there is an obvious notion of an internal category in a 2-category, as a straightforward generalization of internal categories in a 1-category. But internal categories in Cat are double categories, so we need to somehow cut down the double categories to those that really represent honest 1-categories. These are the 2-congruences.
If is a finitely complete 2-category, a homwise-discrete category in consists of a discrete morphism , together with composition and identity maps and in , which satisfy the usual axioms of an internal category up to isomorphism. (Since is discrete, these isomorphisms will automatically satisfy any coherence axioms one might care to impose.)
The notions of functor and transformation between such categories are evident. The first point worth noting is that the transformations between functors are a version of the notion for internal categories, thus given by a morphism in . The 2-cells in play no explicit role, but we will recapture them below. The second point worth noting is that by homwise-discreteness, any “modification” between transformations is necessarily a unique isomorphism, so (after performing some quotienting, if we want to be pedantic) we really have a 2-category rather than a 3-category.
If is any morphism in , there is a canonical homwise-discrete category , where is the comma object of with itself. We call this the kernel of . In particular, if then , so we have a canonical homwise-discrete category called the kernel of . It is easy to check that taking kernels of objects defines a functor ; this might first have been noticed by Street.
If is a homwise-discrete category in , the following are equivalent. 1. is a two-sided fibration in . 1. There is a functor whose object-map is the identity.
Actually, homwise-discreteness is not necessary for this result, but we include it to avoid worrying about coherence isomorphisms, and since that is the case we are most interested in here.
We consider the case ; the general case follows because all the notions are defined representably. A homwise-discrete category in is, essentially, a double category whose horizontal 2-category is homwise-discrete (hence equivalent to a 1-category). We say “essentially” because the pullbacks and diagrams only commute up to isomorphism, but up to equivalence we may replace by an isofibration, obtaining a (pseudo) double category in the usual sense. Now the key is to compare both properties to a third: the existence of a companion for any vertical arrow.
Suppose first that is a two-sided fibration. Then for any (vertical) arrow in we have cartesian and opcartesian morphisms (squares) in :
The vertical arrows marked as isomorphisms are so by one of the axioms for a two-sided fibration. Moreover, the final compatibility axiom for a 2-sided fibration says that the square
induced by factoring the horizontal identity square of through these cartesian and opcartesian squares, must be an isomorphism. We can then show that (or equivalently ) is a companion for just as in Theorem 4.1 here. Conversely, from a companion pair we can show that is a two-sided fibration just as as in loc cit.
The equivalence between the existence of companions and the existence of a functor from the kernel of is essentially found in this paper, although stated only for the “edge-symmetric” case. In their language, a kernel is the double category of commutative squares in , and a functor which is the identity on is a thin structure on . In one direction, clearly has companions, and this property is preserved by any functor . In the other direction, sending any vertical arrow to its horizontal companion is easily checked to define a functor .
In particular, we conclude that up to isomorphism, there can be at most one functor which is the identity on objects.
A 2-congruence in a finitely complete 2-category is a homwise-discrete category in satisfying the equivalent conditions of Theorem 1.
Of course, the kernel of any object is a 2-congruence. More generally it is easy to see that the kernel of any morphism is also a 2-congruence.
The idea of a 2-fork is to characterize the structure that relates a morphism to its kernel . The kernel then becomes the universal 2-fork on , while the quotient of a 2-congruence is the couniversal 2-fork constructed from it.
A 2-fork in a 2-category consists of a 2-congruence , , , and a morphism , together with a 2-cell such that and such that
The comma square in the definition of the kernel of a morphism gives a canonical 2-fork
It is easy to see that any other 2-fork
factors through the kernel by an essentially unique functor that is the identity on .
If is a 2-fork, we say that it equips with an action by the 2-congruence . If also has an action by , say , a 2-cell is called an action 2-cell if . There is an evident category of morphisms equipped with actions.
A quotient for a 2-congruence in a 2-category is a 2-fork such that for any object , composition with defines an equivalence of categories
A quotient can also, of course, be defined as a suitable 2-categorical limit.
The quotient in any 2-congruence is eso.
If is ff, then the square we must show to be a pullback is
But this just says that an action of on is the same as an action of on which happens to factor through , and this follows directly from the assumption that is ff.
A 2-fork is called exact if is a quotient of and is a kernel of .
The opposite of a homwise-discrete category is again a homwise-discrete category. However, the opposite of a 2-congruence in is a 2-congruence in , since 2-cell duals interchange fibrations and opfibrations. Likewise, passage to opposites takes 2-forks in to 2-forks in , and preserves and reflects kernels, quotients, and exactness.