Practical Foundations of Mathematics
Paul Taylor
7.3 General Limits and Colimits
Limits and colimits are perhaps the most important cases of universal properties,
so we devote the next three sections to them and to how they relate to adjunctions
in general. Even if you learn no other theorem in category theory, the most
important result is that left adjoints preserve colimits and right adjoints
limits: the next section consists entirely of applications of this fact.
For the converse, which (unlike the version for posets) needs an extra hypothesis,
we make use of a simple example of a 2-limit, but this will repay ample dividends
in Section 7.7.
The original case for which a definition like the one which follows was needed
was that of a chain or w-sequence, where
obÁ = N and there is an arrow (n+1)® n in the limit case ( projective
or inverse limits) and n® (n+1) in the colimit case (
inductive or direct limits). When it was realised that products,
pullbacks, equalisers and their duals fit the same pattern, it became customary
to define a diagram-shape as a category. More recently, since the identities
and composition play no role in the definition of (co)cones and (co)limits
- and often get in the way - authors' habits have reverted to regarding
them as graphs. Each convention has its uses, and the notion of elementary
sketch covers both.
DEFINITION 7.3.1
A diagram-shape is an elementary sketch by yet another name (
Definition 4.2.5ff), usually with only a set
of nodes. (See Definition 3.2.9 for the poset
analogues.)
- (a)
- A diagram (of shape Á) in a category C
is an interpretation of the sketch, ie an assignment of an object
\typeXi Î obC to each node i Î Á
and a morphism \typeXu:\typeXi® \typeXj to each arrow
u:i® j in such a way that the given polygons (laws) commute.
So if Á is given as a category, a diagram is a functor
\typeX(-) :Á® C.
- (b)
- A cone with vertex G over this
diagram assigns a map \ai:G® \typeXi to each node
i Î Á such that for each (``base'') arrow u:i® j in Á,
the (``cross-section'') triangle \ai;\typeXu = \aj commutes.
- (c)
- A limit is a universal cone
(L,(pi)i Î Á ), so that for any other cone (G,(\ai)i Î Á)
there is a unique mediating map h:G® L with
h;pi = \ai for each i Î Á.
omitted diagram environment
- (d)
- A cocone with covertex Q
under the diagram is an assignment of a morphism
\Fredi:\typeXi® Q to each node i Î Á such that for each arrow
u:i® j in Á, the law \typeXu;\Fredj = \Fredi holds.
- (e)
- A colimit is a universal cocone
(C,(ni)i Î I), so that for any cocone (Q,(\Fredi)i Î Á)
there is a unique mediating map p:C® Q with
ni;p = \Fredi for each i Î Á.
- (f)
- A category which has all set-indexed limits or colimits is called
complete or cocomplete respectively, cf
Definition 3.6.12 for lattices.
- (g)
- See Definition 4.5.10 regarding
preservation and creation of limits and colimits. Some authors say that
a functor is ( co) continuous when it preserves
(co)limits, but we reserve this word for Scott-continuity,
ie preservation of filtered colimits.
As for all universal properties, limits and colimits, where they exist,
are unique up to unique isomorphism. They are written
limi Î Á\typeXi or
\limarrowÁ \typeXi and
\colimi Î Á \typeXi or Ú| limÁ \typeXi
respectively. The projections pi and inclusions ni are an essential
part of the definition.
EXAMPLES 7.3.2
- (a)
- If C is a preorder then a cone is a lower bound and
a cocone is an upper bound; the arrows of Á are redundant.
Limits and colimits are meets and joins respectively (Definition
3.2.4).
- (b)
- For Á = Æ, a (co)cone is simply an object,
the (co)vertex; then a limit is a terminal object and a colimit is an initial
object.
- (c)
- If Á is a discrete graph (with no arrows), or a discrete
category (with only identity maps), then a diagram is a family of objects,
a limit is its product and a colimit its coproduct.
- (d)
- For the graph on the left below, a limit is an equaliser and
a colimit is a coequaliser.
omitted diagram environment omitted diagram environment |
|
- (e)
- For the graph on the right, a limit is a pullback, but the colimit
is simply the value of the diagram at the corner. For the opposite of this
diagram-shape, a colimit is a pushout.
- (f)
- The equaliser of a parallel pair consisting of an endomap
i:X® X and the identity is the set of fixed points. If i
is idempotent then the coequaliser is the image, and these two objects
are isomorphic; the mono and epi split the idempotent i (Definition
1.3.12).
- (g)
- Section 6.4 used similar diagrams (without
the requirement that i be idempotent) to study while
loops.
- (h)
- If Á has a terminal object then we call it a wide
pullback; such diagrams arose in Exercise 3.34
and Lemma 5.7.8. The term is also applied
to a diagram of such a shape or its limit.
- (i)
- If the graph Á is connected (in an unoriented sense,
cf Lemma 1.2.4) then we similarly
refer to connected limits. The epithet refers to the shape
of the defining diagram, and does not mean that the object L is connected,
for example as a topological space. The empty diagram is not
connected; wide pullbacks are, as are equalisers, which are not wide
pullbacks. For simple connectedness, see Exercise
8.13.
- (j)
- A category in which every finite diagram has a cocone (which
need not be colimiting) is called filtered; this generalises
directedness for posets (Definition 3.4.1).
The forgetful functor U:Mod(L)® Set
for a finitary theory L creates filtered colimits ( ie
of diagrams whose shape is filtered), cf Theorem
3.9.4 and Definition
6.6.14.
- (k)
- (Freyd) Assuming excluded middle (so
W = 2),
if a small category has arbitrary limits then it is a preorder. Let
a, b:G\rightrightarrows X be distinct and
I = mor C be the set of all morphisms; then, by the definition of I-fold
product,
2I Ì C(G,X)I º C( G,XI) Ì I, contradicting Cantor's Theorem (Proposition
2.8.8). This result remains true in any sheaf
topos over the classical category of sets.
- (l)
- Martin Hyland, Edmund Robinson and Giuseppe Rosolini [
HRR90] showed that the effective topos
has a reflective, and so complete, subcategory (whose objects are known
as modest sets) which is weakly equivalent to the internal
(``small'') category of PERs (Exercise 5.10).
Because of the problem of Choosing amongst isomorphic objects, the latter
does not have limits of parametric diagrams.
LEMMA 7.3.3
Let \typeX(-):Á® C be a diagram in a category
with equalisers. If C has products indexed by
obÁ and morÁ then limi\typeXi exists. Moreover
if F:C® D preserves these equalisers and
products then it preserves the limit.
PROOF: The limit of \typeX(-):Á® C
is given by the equaliser
omitted diagram environment
EXAMPLES 7.3.4
- (a)
- The lemma was found by abstracting the construction of general
limits in Set, namely the subset consisting of those
(obÁ)-tuples (\argsi) which satisfy
\typeX u(s(i)) = s(j) for each u:i® j in Á.
- (b)
- Equalisers, binary products and a terminal object suffice
to construct all finite limits (see also Example
5.1.3(c)).
- (c)
- Similarly, the colimit C of any diagram
\typeX(-): Á® Set is the coequaliser
of a pair of functions into the coproduct \typeC0.
By Lemma 5.6.11, this coequaliser is the
quotient C = \typeC0/ ~ by an equivalence relation, namely
that generated by the relation i,x ~ j,y if there is an arrow
u:i ® j in Á such that y = \typeXu(x).
Although it is useful for showing that limits and colimits exist in certain
semantic categories, this decomposition into products and equalisers
is misleading for type theory, as we shall see in Section 8.3.
(See [ML71, p. 109] for a more detailed proof
of the lemma.)
Adjoints preserve (co)limits
The most important result.
THEOREM 7.3.5
Let F\dashv U. Then F preserves any colimits that exist and U any
limits, cf Proposition 3.6.8.
PROOF: Let \typeX(-):Á® S
be any diagram and let ni:X® C be a colimiting cocone under it in S
. Then
- (a)
- By functoriality, Fni:FX® FC is also a cocone under
F\typeX(-).
- (b)
- Let \Pollyi:F\typeXi® Q be a cocone under the
diagram F\typeX(-):Á® A. By the adjoint
correspondence there are maps \Fredi:\typeXi® UQ, which,
by naturality with respect to \typeXu, form a cocone under
the diagram \typeX(-):Á® S.
omitted diagram environment
Hence there is a unique mediator f:C® UQ in S.
- (c)
- Taking this back along the adjoint correspondence, there is
a map p:FC® Q, which is a mediator for the cocone \Pollyi
by naturality. It is unique because the argument is reversible.
The result for limits is the same with the arrows reversed. []
REMARK 7.3.6
Colimits are preserved by left adjoints because they are themselves left
adjoints, and a diagram of left adjoints commutes iff the right adjoints
do, cf Remark 3.6.11. However, to
state this precisely we have to formulate the analogue of Lemma
3.6.4ff (see Exercise
7.27ff).
omitted diagram environment
EXAMPLES 7.3.7
- (a)
- Let U:A Ì S be the (full and replete)
inclusion of a reflective subcategory, with F\dashv U, and let
\typeA(-):Á® A be a diagram. Then
FcolimSU\typeAI = colimA FU\typeAI º colimA\typeAI |
|
by Corollary 7.2.10(b), cf
Proposition 3.7.3 for posets. As an easy
special case of Proposition 7.5.6, the
inclusion U not only preserves but creates limits (Definition
4.5.10(c)).
- (b)
- In a cartesian closed category, where Xx(-)\dashv ( = )X
,
- Xx(-) preserves colimits;
- in particular, products distribute over sums (Definition
5.5.1);
- (-)X preserves limits;
- the contravariant functor S(-) sends colimits to
limits, because it is symmetrically self-adjoint on the right (Example
7.1.9(b)); in particular
SX+Y º SXxSY;
cf Proposition 3.6.14 for Heyting
lattices.
- (c)
- Since the forgetful functors
Set® Pfn and Set® Rel
have right adjoints (namely the lifting and covariant powerset functors),
the colimits with respect to total functions work for partial functions
and for relations too.
- (d)
- The forgetful functor
U:Mod(P)® Set from the category of algebras for the covariant powerset
functor creates (small) limits, but has no left adjoint, since the initial
P-algebra would be P(A) º A, contradicting
Cantor's theorem (Propositions 2.8.8 and
6.1.4(b)).
Because of Example 7.3.2(k) we cannot reasonably
ask for categories to have and functors to preserve class-indexed (co)limits.
Theorem 7.3.12 shows what alternative condition
suffices to obtain the right adjoint for a colimit-preserving functor.
The forgetful functor from the category of complete Boolean algebras to
Set is a more popular counterexample, but it takes rather
more work to show that FN doesn't exist [Joh82
, p. 57].
The next section gives some further applications of Theorem
7.3.5.
Comma categories
The next construction is a new kind of limit which arises in 2-categories,
just as equalisers appeared when we moved from posets to categories. Section
7.7 makes a powerful application of this simple idea
to the equivalence of syntax and semantics.
DEFINITION 7.3.8
Let CF® S U¬ A be functors.
Then the comma category F¯ U has
- (a)
- objects (X,A,a) where
X Î ob C, A Î obA and a:FX® UA
in S (we commonly abbreviate this to the map a:F(X)® U(A)
alone, bracketing the objects for emphasis if necessary; such an object
will be called tight if the map a is an isomorphism),
- (b)
- morphisms the pairs f:X® Y, u:A® B
making the square on the left commute:
omitted diagram environment omitted diagram environment |
|
The square of functors on the right doesn't commute; the little arrow is a
natural transformation a:F·p0® U·p1 that
has a categorical universal property:
PROPOSITION 7.3.9
Let G be another category with functors
P:G® C and Q:G® A and a natural transformation
f:F·P® U·Q. Then there is a functor
P,Q,f:G® F¯ U, unique up to equality, such that
P = p0·P,Q,f, Q = p1·P,Q,f and
f = a·P,Q,f.
In particular, if the square from G commutes up to isomorphism then
the mediator factors through the pseudo-pullback, ie
the full subcategory of F¯ U consisting of the tight objects.
[]
EXAMPLES 7.3.10
The notation can be specialised in several ways.
- (a)
- If A = {*} ,
U* = A, S = C,
F = \idC, we have the slice C¯ A
(5.1.8).
- (b)
- Dually, for C = {*} ,
F* = X,
S = A, U = \idA, the coslice X¯ A
.
- (c)
- If C, S and A are discrete categories
then F¯ U is the pullback in Set of their
sets of objects (Example 5.1.4(b)).
- (d)
- If they are preorders then
F¯ U = {x,a| x Î C,a Î A,Fx £ Ua} (see footnote
down-cl fn on page down-cl fn
).
- (e)
- An initial object of X¯ U (where
C = {*} and F(*) = X) is a universal map from the object X to
the functor U (Definition 7.1.1).
- (f)
- The functor U is called final if for every
X Î obS, X¯ U is a connected category.
See Exercise 7.19 for filtered final functors.
- (g)
- A terminal object of F¯ A (where
A = {*} and U(*) = A) is a co-universal map from the functor F
to the object A (Lemma 4.5.16 and Definition
7.1.7ff);
- (h)
- (Lawvere) F\dashv U iff there is an isomorphism of categories
omitted diagram environment
such that the triangle of functors commutes.
- (i)
- For S = C, F = \idC and
U:A ® S any functor, S¯ U is called
the gluing construction (Section 7.7).
Equivalent colimits
We now prove Proposition 3.2.10 for categories.
Let \typeX(-):Á® C be a diagram. Then
any functor U:J® Á between diagram-shapes
induces a ``restriction'' of cocones \GuyI:\typeXI® Q under
the diagram of shape Á to \FredJ = \GuyUJ under the composite
J® Á® C.
PROPOSITION 7.3.11
If U is final then this is a bijection: every cocone
\FredJ:\typeXUJ®Q for J extends uniquely to a cocone \GuyI for Á.
So whenever either of them exists,
\colimI Î Á\typeXI º \colimJ Î J\typeXUJ.
PROOF: Let \FredJ:\typeXUJ® Q be a cocone in
C under J. By finality, for
I Î obÁ the comma category I¯ U is connected. Let a:I® UJ
be any object of it and put \GuyI = \typeXa;\FredJ, as we must
for this to be a cocone under Á with respect to a, since
\FredJ = \GuyUJ.
omitted diagram environment
Any other object a¢:I® UJ¢ of I¯ U is linked to
this one by a zig-zag, of which (for induction on its length) we need only consider
one step j:J® J¢. Since this is a morphism of I¯ U
and \Fred(-) was a cocone, the triangles commute, so
\GuyI = \typeXa¢;\FredJ¢.
We may then take \GuyI as the value at I of a cocone over Á,
because for i:I¢® I,
I¯ U\hookrightarrow I¢¯ U as a subcategory, so \GuyI¢ = \typeXi;\GuyI.
[]
The general adjoint functor theorem
We would like to show that if S has and F:A® S
preserves colimits then F has a right adjoint.
By Example 7.3.10(g), it suffices to show
that, for each A Î obA, the category F¯ A
has a terminal object. Since the terminal object of any category X
is the colimit of the diagram \idX:Á® X
with Á º X,
UA = colim{X| (FXf® A) Î F¯ A }, |
|
as in the proof of Theorem 3.6.9. (This is an
example of a left Kan extension, the categorical analogue
Fid(A) of the modal operator < > in Section 3.8
.)
Unfortunately, F¯ A is a large category, so by Example
7.3.2(k) we cannot ask for its colimit directly.
There may, however, be a smaller diagram which has the same colimit, in the
sense of Proposition 7.3.11.
THEOREM 7.3.12
[Peter Freyd, 1963] Let S be a category which has and
F:S® A a functor which preserves all small colimits. Let
A Î obA and suppose that the solution-set
condition holds:
there are a small category \IA and a final functor
\IA® F ¯ A.
Then there is a co-universal map eA:FX® A from the functor
F to the object A. Making an assignment of these, there is a right
adjoint functor F\dashv U. []
If we are already in possession of the co-universal map, the singleton subdiagram
consisting of this alone suffices, so the solution-set condition is trivially
necessary.
Preservation of limits is normally excellent heuristic evidence justifying
the search for an adjunction: it is well worth making a habit of checking
whether functors preserve products, coproducts and a few other cases. Frequently
a few minutes' work will identify the essential features of any adjunction
which holds, and the quickest way of proving adjointness is the universal
property. We have also seen in the preceding sections that the effect of the
two functors on morphisms, the unit, h, co-unit, e,
transposition, l, and their naturality all shed light
on the phenomena under study. So, although this is technically ``redundant''
information, they should always be investigated and described.
The general adjoint functor theorem has been cited [ML88
] as the first theorem of category theory itself, but the solution-set
condition seriously limits its value. Which is more useful, an ah
doc construction verifying this condition, or a presentation of the adjoint,
which is an invariant? Clearly the latter, because subsequent researchers
will want to know as much as possible about what it does, and maybe study it
in its own right. Describing the adjoint is elementary (in the technical
sense) and usually simpler than testing preservation of all (co)limits
properly.
Although the theory of general limit diagrams is important to bringing together
products, equalisers, pullbacks and inverse chains, it begs a number of
questions, in particular where such (infinite) diagrams
come from. We shall discuss this and the existence of arbitrary
limits and colimits in Set in the final section of the book.