Practical Foundations of Mathematics

Paul Taylor

5.1 Pullbacks and Equalisers

Pullbacks are everywhere, as Serge Lang observed in the 1950s. Indeed they occur spontaneously, as it were: commutative squares arising for other reasons often happen to satisfy the universal property.

DEFINITION 5.1.1

(a): Let f,g:X\rightrightarrows Y be a parallel pair of maps in a category S. Then an object E together with a morphism m:EŽ X is an equaliser of f and g if m;f = m;g, and whenever a:GŽ X is another morphism such that a;f = a;g there is a unique map h:GŽ E with a = h ;m.
(b): Let f:XŽ Z and g:YŽ Z be two maps in a category. Then an object P together with a pair of maps p₀:PŽ X and p₁:PŽ Y is a pullback if p₀;f = p₁;g and whenever a:GŽ X and b:GŽ Y also satisfy a;f = b;g there is a unique map h:GŽ P such that h;p₀ = a and h;p₁ = b.

displaymath omitted diagram environment omitted diagram environment

Pullbacks and equalisers are unique up to unique isomorphism where they exist, cf Theorem 4.5.6.

The pullback and mediator are written X×_ZY and a,b. However, one should remember that this notation hides not only the projection maps (which were already absent from the product and exponential notations we have used) but also the maps f and g which are part of the data. The object X×_ZY or the map p₁:X×_ZYŽ Y is also called the pullback of f along or against g. In Proposition 5.1.9, where we write p₀ = f^*g, we shall see that this asymmetrical language is more typical of the way pullbacks arise than the diagram above suggests.

Pullbacks are often indicated with the right angle symbol, which was suggested by William Butler in 1974 and popularised by Peter Freyd. In Section 9.4 we will no longer be able to afford the space for it, and will instead adopt the convention that the ubiquitous pullbacks are drawn as parallelograms. This emphasises how pullbacks do ``parallel translation'' of structure, in particular by substitution in syntax.

There is no widely used notation for an equaliser, but Freyd and Scedrov [ FS90] write \rightarrowtail ^\f_g or just \rightarrowtail ^ˇ_ˇ for the map m. The hook notation will be discussed in the next section.

The following easy result will turn out to be extremely useful:

LEMMA 5.1.2 Suppose that the two squares commute below, and that the one on the right is a pullback.

omitted diagram environment

Then the rectangle is a pullback iff the left hand square is. []

Applications

EXAMPLES 5.1.3

(a): Pullbacks in a poset are just meets, but of pairs with a common upper bound (Exercises 3.5, 3.20, 3.34 and 4.51). Since all squares commute, what the bound is doesn't matter, only that it exists. Again, since any two parallel maps are equal, they trivially have an equaliser: the identity.
(b): A parallel pair f,g:[[(x)\vec]:[(X)\vec]] \rightrightarrows [[(y)\vec]:[(Y)\vec]] in the category of contexts and substitutions is given by a list of pairs of terms \funf_j([(x)\vec]),\fung_j( [(x)\vec]):\typeY_j. A substitution a = [[(x)\vec]: = [(a)\vec]] has equal composites with them iff it is a unifier, ie \funf_j[[(x)\vec]: = [(a)\vec]] = \fung_j[[(x)\vec]: = [(a)\vec]], or, in the informal notation, \funf_j([(a)\vec]) = \fung_j([(a)\vec]). The equaliser, if any, is the most general unifier (Remark 1.7.8), since any other unifier is a substitute. Similarly pullbacks solve \funf_j([(x)\vec]) = \fung_j([(y)\vec]). In Section 6.5 we shall construct the most general unifier in the simplest case, a free algebraic theory.
(c): A pullback rooted at the terminal object Z = 1 is a product. In any category with binary products, pullbacks may be constructed from equalisers and vice versa ( cf Remark 5.2.3).

EXAMPLES 5.1.4 Pullbacks of sets and functions have several names.

(a): The equaliser of two parallel functions f,g:X\rightrightarrows Y is (the inclusion of) the subset E = {x|f(x) = g(x)}. If a: GŽ X with fo a = go a then the results of a at all elements of G lie in E Ě X, so a restricts to h:GŽ E Ě X.
(b): The pullback of any two functions f:XŽ Z and g:YŽ Z is the subset {x,y|f(x) = g(y)} with the usual projections. A pair of maps from G gives rise to a map a,b:GŽ Xx Y to the product, which restricts to the pullback in the same way as for the equaliser.
(c): If g:Y Ě Z is a subset inclusion then the pullback is the inverse image, f^-1[Y] Ě X.
(d): If f and g are both subset inclusions then the pullback, XÇY Ě Z, is their intersection (Example 2.1.6(d)).

EXAMPLES 5.1.5 Some other familiar semantic categories.

(a): The restriction of the order on the source gives the equaliser and on the product gives the pullback in Preord, Pos, CSLat, SLat, Lat, DLat, BA, Frm, HSL, Heyt and Dcpo. This fails, however, in many popular categories of domains.
(b): Equalisers and pullbacks in Set^{C^op} are constructed pointwise and the Yoneda embedding (Theorem 4.8.12(b)) \H_(-):C \hookrightarrow Set^{C^op} preserves whatever limits exist.
(c): The category Mod(L) of models of any algebraic theory L has pullbacks and equalisers. Indeed the forgetful functor Mod(L)Ž Set^S creates limits ( cf Definition 4.5.10(c)), S being the set of sorts.
(d): The category of trichotomous orders (Definition 3.1.3) and strictly monotone functions does not have products, but it has got pullbacks and equalisers, constructed in Set. This is because its maps are all injective, so pullbacks are intersections.
(e): A coherence space is a set X with two symmetric relations \coh (joined or coherent) and \icoh (un-joined or incoherent ) satisfying a trichotomy law: exactly one of x\coh y, x = y and x\icoh y holds. An embedding is a function which preserves all three relations, whence it also reflects them and is injective, so pullbacks are intersections.
(f): The category of fields also has pullbacks and equalisers but not binary products or a terminal object. We can say that two elements x,y Î K of a field are apart in a positive sense which is preserved by homomorphisms, if $z.(x-y)z = 1, which we write as x#y. This obeys the dichotomy law that exactly one of x = y and x#y holds, whence all homomorphisms are injective. The full subcategory consisting of those fields in which a particular polynomial has a root (say x²+1 = 0) has pullbacks but not equalisers.

EXAMPLES 5.1.6 Some squares which are ``spontaneous'' pullbacks.

(a): Exercise 4.34 showed that the Church- Rosser Theorem (Fact 2.3.3) may be expressed as a commutative square in a certain category. This square is in fact a pushout (a pullback in the opposite category) [ Bar81, Exercise 12.4.4].
(b): The effect of the product functor on morphisms (Proposition 4.5.13) gives rise to pullback squares. These also occurred in the diagrams Example 4.6.3(f) and Definition 4.7.9.
(c): Let f:X˘Ž X in C and g:E˘Ž E in G be maps in any two categories. Then this square (Proposition 4.8.3(c)) is a pullback: omitted diagram environment This means that the result of applying a pullback-preserving functor P:GxCŽ D to this square yields another pullback: cf Exercises 3.20 and 5.9.

Slices Pullbacks arise in three important ways in type theory:

(a): they generalise products (so are also called fibred products),
(b): they have something to do with equality, and
(c): in Chapter VIII their primary role is substitution, cf Exercise 5.6.

In the first two cases there is a symmetry between the two legs, but this is not true of substitution, where one is definitely acting on the other and not vice versa . Let's look at (b) and then (c).

REMARK 5.1.7 The pullbacks below are in a sense trivial, in that the pullback of an identity must be an isomorphism. But if we think of the pullback as a subset X×_ZY Ě XxY, on the left we obtain the graph of a function, cf Definition 1.3.1, Exercise 1.14 and Corollary 4.3.13(a).

omitted diagram environment

The even simpler case on the right gives the binary equality relation, ( = _X) Ě XxX, to which we return in Remark 8.3.5. []

To see pullbacks as products exactly, we need to formalise the idea used in Lemma 4.5.16. For the terminal object, see Exercise 5.4.

DEFINITION 5.1.8 Let X be any object of any category S. The slice category SŻ X has

(a): as objects the S-morphisms d:YŽ X,
(b): as morphisms the commuting triangles in S, omitted diagram environment
(c): and as identity and composition those for S .

PROPOSITION 5.1.9 If S has chosen pullbacks against u:X˘Ž X then u^*:SŻ XŽ SŻ X˘ is a functor. This is a contravariant action (Section 4.2), except that id^* need only be isomorphic to the identity and (u;|)^* to u^*·|^*.

omitted diagram environment

PROOF: The effect of u^* on the morphism f is the mediator between the pullback parallelograms. Identities and composites are preserved by the same argument by uniqueness of mediators as in Proposition 4.5.13. []

The analogue of the slice for posets is just the lower set generated by an element (Definition 3.1.7). In the next section we shall use the same construction, but with the ds restricted to be monos. It will appear in a more general form in Definition 8.3.8, where the ds belong to a specified class but u and f will be arbitrary. An important common generalisation of pullbacks and slices (comma categories) is given in Definition 7.3.8.