Practical Foundations of Mathematics

Paul Taylor

5.8 Regular Categories

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 AbGp and Set. It is these properties of the sum and quotient, and not the all-powerful operations of Zermelo type theory, which provide the foundation of twentieth century algebra.

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 be effective regular or Barr- exact.
(d): An AbGp-enriched category (Definition 5.4.3ff) which is also effective regular is known as an Abelian category. Equivalent definitions are discussed in [FS90, Section 1.59].
(e): A prelogos is a regular category with finite unions of subobjects which are stable under pullback (inverse image).
(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 pretopos is an effective regular extensive category (Definition 5.5.3); in particular it is a prelogos, but not necessarily a logos.

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.

EXAMPLES 5.8.2

(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

{id, (12)(34), (13)(24), (14)(23)} Ė A₄

and the map which interchanges (13)(24) with (14)(23). (Freyd)

(e)

Von Neumann regular rings, those satisfying "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): split epi: there is a map m:Y\hookrightarrow X with m;e = \id_Y;
(b): regular epi: e is the coequaliser of some (its kernel) pair;
(c): cover or surjective: e^ m for all monos m;
(d): epi: for any 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 projective . In a regular category, the right hand diagram shows that 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

= 0pt omitted array environment

may coincide whilst still being proper.

(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 R is functional iff R^op;R Ė id, total iff id Ė R;R^op and confluent iff R^op;R Ė R;R^op.

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.

LEMMA 5.8.8

(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 XxYp₀Ž 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 ^mX\hookrightarrow ^\ Z be monos in a pretopos.

(a): Then