This section sums up the ``good behaviour'' of coequalisers, and of finite
colimits in general, like that of coproducts in Section 5.5.
Categories of algebras inherit this good behaviour for quotients of congruences,
but not for coproducts or general coequalisers. The following definitions
progressively capture the ** exactness** properties of

DEFINITION 5.8.1
Let *S* be a category.

**(a)**- If
*S*has finite limits it is called a.*lex category* **(b)**- If further the image factorisation exists (Lemma
5.7.4) and is stable under pullback then
*S*is called a.*regular category* **(c)**- If further every congruence is the kernel pair of its coequaliser
then
*S*is said to beor*effective regular*.*Barr- exact* **(d)**- An
**AbGp**-enriched category (Definition 5.4.3ff) which is also effective regular is known as an. Equivalent definitions are discussed in [FS90, Section 1.59].*Abelian category* **(e)**- A
is a regular category with finite unions of subobjects which are stable under pullback (inverse image).*prelogos* **(f)**- A prelogos in which the inverse image operation between subobject
lattices has a right adjoint is called a
.*logos* **(g)**- By Theorem 3.6.9 any prelogos
which has
*arbitrary*stable unions of subobjects is a logos; we call it.*locally complete* **(h)**- A
is an effective regular extensive category (Definition 5.5.3); in particular it is a prelogos, but not necessarily a logos.*pretopos*

The original example of a regular category was **AbGp**, and
in general **Mod**(*L*) for any finitary algebraic theory
*L*, by Theorem 5.6.9. From Section
5.6, these categories have *all* coequalisers,
so there is some ambiguity in the literature as to whether all coequalisers
are required in the definition: after [FS90, §1.52],
we say they are not. Indeed in regular categories coequalisers *of
their kernel pairs* are stable under pullback, but even when they exist general
coequalisers need not be stable.

**(a)**-
**Set**is a pretopos by Example 5.5.6(a) and Proposition 5.6.8. **(b)**- A poset is lex iff it is a semilattice, and then it is trivially
effective regular. It is a prelogos iff it is a distributive lattice,
and a logos iff it is a Heyting lattice (Definition
3.6.15). Conversely, in any prelogos or
logos, every \Sub
_{S}(*X*) is a distributive or Heyting lattice respectively. Posets can never be pretoposes, except degenerately. **(c)**-
**Mod**(*L*), where*L*is a finitary algebraic theory, is effective regular by Theorem 5.6.9. It also has arbitrary colimits;*filtered*colimits (Example 7.3.2(j), in particular*directed*unions of subobjects) are stable, but finite ones are usually not. **(d)**- In particular
**Gp**is effective regular. It also has all coequalisers, but the following one is not stable under pullback. omitted diagram environment The parallel pairs consist of the inclusion of the normal subgroup and the map which interchanges (13)(24) with (14)(23). (Freyd){ *id*, (12)(34), (13)(24), (14)(23)} Ì*A*_{4} **(e)**-
, those satisfying "*Von Neumann regular rings**x*.$*y*.*x**y**x*=*x*, form a non-effective regular category. **(f)**- Abelian groups, vector spaces and modules form Abelian categories.
**(g)**- The category of compact Hausdorff spaces and continuous
functions is a pretopos, in which directed unions and general coequalisers
also exist but are not stable.
**(h)**- Equivalence relations in
**Pos**are not effective: all three points in the quotient of {0 < 1 < 2} by 0 ~ 0 ~ 2 ~ 2, 1 ~ 1 are identified. The kernel pairs of monotone functions are convex (Example 3.7.5(c)).

**Stable image factorisation **
To make Lemma 5.7.4 work as intended, we have
to show that the class of regular epis is closed under composition.

PROPOSITION 5.8.3
In a regular category the class of regular epis is closed under pullback
and so is the *E* class of the image factorisation.

PROOF: Suppose e:*X*® *Y* and **f**:*Y*® *Z* coequalise
their kernel pairs, *K*\rightrightarrows *X* and *L*\rightrightarrows *Y*
respectively. Let *M*\rightrightarrows *X* be the kernel pair of
*X*® *Y*® *Z*; comparing commutative squares with these kernels ( *cf* Lemma
5.6.6(a)), there are mediators *K*® *M*® *L*.

Let *X*® Q be a map having equal composites with
*M*\rightrightarrows *X*. Then the composites *K*® *M*\rightrightarrows *X*® Q are
equal and give *Y*® Q. The required mediator *Z*® Q exists
iff the composites *L*\rightrightarrows *Y*® Q are equal.

omitted diagram environment

We can achieve this by showing that the maps *M*® *P*® *L* are epi. Indeed,
both parts are pullbacks of the regular epi
e:*X*\twoheadrightarrow *Y* (against split epis). []

The last part is sufficient but not necessary. The literature on this subject is confusing, because in certain categories, one may show by slightly different arguments that regular epis compose, without being stable under pullback. There is apparently no convenient necessary and sufficient condition for composability of regular epis.

REMARK 5.8.4
There are four useful notions of surjectivity
e:*X*\twoheadrightarrow *Y* in lex categories ( *cf* Definition
5.2.1 for monos):

**(a)**-
: there is a map*split epi***m**:*Y*\hookrightarrow*X*with**m**;e = \id_{Y}; **(b)**-
: e is the coequaliser of some (its kernel) pair;*regular epi* **(c)**-
or*cover*: e^*surjective***m**for all monos**m**; **(d)**-
: for any*epi***f**,**g**:*Y*\rightrightarrows*Z*, if e;**f**= e;**g**then**f**=**g**.

By Proposition 5.8.3, the middle two coincide
in a regular category. Furthermore, every epi is regular in **Set**,
and indeed in any pretopos, but to say that every epi splits would be an internal
form of the axiom of choice (Exercise 1.38).

omitted diagram environment

**(e)**- An object
*P*with the lifting property on the left for every cover*A*\twoheadrightarrow*B*is called. In a regular category, the right hand diagram shows that*projective**P*is projective iff every cover*A*¢\twoheadrightarrow*P*splits.

**Relations **
Logically, stability of image factorisation corresponds to the Frobenius
law (Lemma 1.6.3). It is also vital for relational
calculus.

REMARK 5.8.5 The stable image interprets existential quantification, removing the uniqueness requirement from Remark 5.2.9.

omitted diagram environment

Stable unions of subobjects similarly express disjunction, where once again we have dropped uniqueness from Remark 5.5.10 . The right adjoint in a logos gives the universal quantifier. In this way, existential, coherent (Ù, Ú, $) and first order logic may be interpreted in regular categories, prelogoses and logoses respectively. We study these type-theoretically in Chapter IX, and just treat relational algebra here.

LEMMA 5.8.6
Let *S* be a lex category, in which relations
*R*:*X*\leftharpoondown\rightharpoonup *Y* are interpreted as subobjects
*R*\hookrightarrow *Xx* *Y*. Then composition of *general* relations, defined by image
factorisation, is associative iff *S* is regular.

PROOF: Let
*W* *Q*\leftharpoondown \rightharpoonup *X* *R*\leftharpoondown \rightharpoonup *Y* *S*\leftharpoondown \rightharpoonup *Z*.

**(a)**- As in Proposition 5.3.5, the pullback
below gives a subobject, abbreviated as
*x**Ry**Sz*Ì*XxYxZ*, of the three-fold product, but not necessarily a mono into*Xx**Z*. We use image factorisation to get one, as in the bottom row. omitted diagram environment **(b)**- To say that the factorisation is stable means that the mono in
the middle of the top row is invertible; this was one of the two crucial
steps in the proof of Lemma 4.1.3, the other
being similar.
**(c)**- Interchanging existential quantifiers does not cause any
problem, because surjections compose (but
*cf*Lemma 5.7.4). **(d)**- Composition of three particular relations may be associative
without stability, as the two subobjects
may coincide whilst still being proper.= 0 *pt**omitted**array**environment* **(e)**- However, if
*R*is functional then the lower epi is invertible, so one subobject is total without hypothesis. Thus associativity in the case where*R*^{op}is functional and*Z*= 1 implies stability. []

PROPOSITION 5.8.7 Relations in a regular category

**(a)**- form another category under relational composition (
*id*,*R*;*S*); **(b)**- with the same source and target admit binary intersection (
*R*Ç*S*), which is associative, commutative and idempotent; we also define*R*Ì*S*Û*R*=*R*Ç*S*; **(c)**- have monotone composition:
*R*;(*S*Ç*T*) Ì (*R*;*S*)Ç(*R*;*T*) ; **(d)**- have opposites, where
*R*^{op}has the source and target interchanged, and satisfies*omitted**array**environment* **(e)**- and also obey
: (*modularity**R*;*S*)Ç*T*Ì (*R*Ç(*T*;*S*^{op}));*S*. []

Freyd and Scedrov [FS90] call such a structure
an ** allegory**. They show how the logical connectives described
above may be reformulated in terms of relations rather than functions. For
example

Using this we can try to recover the category composed of functions from its
allegory composed of relations. Any *R* Ì *id* is the
support of a partial function (Remark 5.3.6)
and must be introduced as a virtual object. Every allegory is thereby embedded
in the category of relations of a regular category. The utility of the technique,
as we shall see in Theorem 6.4.19, is that allegories
can sometimes be constructed from one another more simply than the corresponding
categories, and results deduced without the extraneous objects.

**Stable unions **
To make full use of relational algebra we need unions of possibly overlapping
subsets. In a pretopos (effective regular extensive category), unions
of subobjects may be defined as quotients of sums and are stable. First we
consider the stable unions alone.

**(a)**- Image factorisation provides the left adjoint to the inverse
image map
**f**^{*}:*Sub*(*X*)®*Sub*(*Y*) , so preserves unions by Proposition 3.6.8. **(b)**- Relational composition distributes over stable unions.
**(c)**- In a logos there are adjoints (-);
*R*\dashv (-)/*R*and*R*;(-)\dashv*R*\(-), which both reduce to*Heyting implication**R*Þ (-) if*R*Ì D. These satisfy*R*;(*R*\*S*) Ì*S*and (*S*/*R*);*R*Ì*S*. The analogous structure for relations is called a.*division allegory*

The slash notation, suggesting division, is due to Joachim Lambek, who used it first in linguistics [Lam58] and later for modules for rings [Lam89]. (Don't confuse division with \ for subset difference, Example 2.1.6(e).) We shall use it to study transitive closures in the proof of Lemma 6.4.9.

PROOF: *R* Ì **f**^{*}*U*Þ *I* Ì *U* since
(*R*\twoheadrightarrow *I*)^(*U*\hookrightarrow *X*),

omitted diagram environment

and conversely since **f**^{*}*U* is a pullback. Composition is given by
the image of a pullback, and both operations preserve unions or have adjoints
as appropriate. []

The elementary properties of **Set** are already beginning
to emerge in a prelogos. The next result is known as the Pasting Lemma as
it is needed to combine partial functions, for example in Lemma
6.3.12.

LEMMA 5.8.9
Let *U*,*V* Ì *X* and suppose that product distributes over union. Then
the diagram on the left, which is a pullback by construction, is also a pushout.

omitted diagram environment

PROOF: Recall that a relation *R*\hookrightarrow *XxY* is the
graph of a function iff *R*\hookrightarrow *XxY*p_{0}® *X*
is an isomorphism. Applying this to **f**, **g** and **h**
in the diagram on the right, the graph of **f** is isomorphic to *U*,
*etc* . Then the union of the graphs of **f** and of **g**,
formed as a subobject of *XxY*, is isomorphic to *U*È*V* Ì *X* by
distributivity. Hence it is the graph of a function *U*È*V*® *Y*. []

Pretoposes enjoy even better properties.

PROPOSITION 5.8.10
Let *Y*\hookleftarrow ^{m}*X*\hookrightarrow ^{\} *Z* be
monos in a pretopos.

**(a)**- Then