<<

. 32
( 60 .)



>>

d

f »(h, k) k
 
 r
 
c  
© c
E S4
S3
h
for which r —¦ u = r —¦ v = f and s —¦ u = s —¦ v = g (which requires adding a certain
cone and some diagrams to the sketch) and an arrow ±: SS ’ A, along with

diagrams forcing ±(a) to equal both u and v.

Toposes

A topos is an LE-category with the property that for each object X there
is an object PX (the power object of X) and a subobject e: ∈X )’ X — PX

with the property that if u: U )’ X — B is any subobject of X — B for which

168 4 Theories
(i) this diagram
u E X —B
E
U

(1)
Ψ(u) idX — ¦U
c c
E E X — PX
∈X
is a pullback, and
(ii) if u : U )’ X — B determines the same subobject as u, then Ψ(u) =

Ψ(u ) and ¦(u) = ¦(u ). (This is equivalent to the de¬nition in Chapter 2: the
subobject ∈X is in fact a universal element for the functor Sub (X, —(’)), which
is therefore representable.)
Toposes with designated limits and designated power objects are also models
of an LE-theory. One obtains them by adding some data determining the power
object and ∈ to the sketch for LE-categories just given.
The ¬rst thing we need is an object M of the sketch which is to consist of all
the monic arrows in A. This can be constructed as an equalizer of two arrows
from A to CD, one which takes f : X ’ Y to the pullback of

X

f
c
EY
X
f
and another which takes f to
idX E
X X

idX
c
X
Both these arrows can be constructed by techniques used above.
We also need an arrow P : O ’ O which should take an object (element of

O) to its power object, adn an arrow E: O ’ M along with diagrams forcing

the domain of E(X) to be X and the codomain to be X — PX.
Another equalizer construction will produce an object S of monos along with
a speci¬c representation of the codomain of the mono as a product of two objects;
in other words,
S = {(u, X, B) | u is monic, codomain of u is X — B}
4.4 Left Exact Theories 169
The universal property of ∈ then requires an arrow φ: S ’ A along with diagrams

forcing the domain of φ(u, X, B) to be B and the codomain to be PX. Further
constructions will give an arrow from A to A taking f : B ’ PX to (idX , f ).

From these ingredients it is straightforward to construct an arrow β: S ’ CD

that takes u: U ’ X — B to

X —B

idX — φ(u)
c
E X — PB
∈X
The appropriate diagram then forces the pullback of this to be (1). The
uniqueness of φ(u) can be obtained by a construction similar to that which gave
the uniqueness of the arrow to a pullback.
Perhaps the most e¬cient way to make φ and ψ be invariant on subobjects is
to construct an object T consisting of all diagrams of the form
V
Td
dv
d
c ‚
d
E X —B
Uu

with all four arrows monic. (In a model the arrows between U and V must
become inverse to each other). Then add to the sketch arrows φ : T ’ A and

ψ : T ’ A and diagrams forcing φ (u, v) = φ(u) = φ(v) and similarly for ψ.


Exercises 4.4

1. Suppose D: I ’ Set is a ¬ltered diagram. On the set U = DI de¬ne a

relation R by letting xRy for x ∈ DI and y ∈ DJ if and only if there is an object
K and maps f : I ’ K and g: J ’ K such that Df (x) = Dg(y).
’ ’
(i) Show that R is an equivalence relation.
(ii) Show that the set of equivalence classes together with the evident maps
DI ’ U ’ U/R is the colimit of D.
’ ’
(iii) Show that if J is a ¬nite graph and E: J ’ Hom(I , Set) is a diagram,

then colim: Hom(I , Set) ’ Set preserves the limit of E.


2. One can construct an LE-theory for graphs by omitting some of the arrows,
cones and diagrams in the theory for categories, as suggested in the text, or by
170 4 Theories
constructing an FP-theory along the lines suggested in Exercise 10 of section
3.4 and then constructing the LE-completion of that theory. Are the resulting
theories equivalent (or even isomorphic) as categories?

3. Show that the category of right-exact small categories and right-exact functors
is the category of models of an LE-theory.

4. Show that neither of these subcategories of Set is the category of models of
an LE-theory:
(a) The full subcategory of ¬nite sets;
(b) The full subcategory of in¬nite sets.
(See Exercise 3 of Section 8.3.)

5. Prove Lemma 6. (Hint: Use representable functors to reduce it to the dual
theorem for equalizers in Set. It is still a fairly delicate diagram chase.)


4.5 Notes on Theories
The motivating principle in our study of theories is: turn the mathematician™s
informal description of a type of structure into a mathematical object which can
then be studied with mathematical techniques. The fruitfulness of the subject
comes from the interplay between properties of the description (the theory, or
syntax) and properties of the objects described (the models, or semantics). That
LE theories are closed under ¬ltered colimits is an example of this (Theorem 4
of Section 4.4). Many other properties are given in Theorem 1 of Section 8.4.
In classical model theory, of which a very good presentation is found in [Chang
and Keisler, 1973], the theory consists of a language, rules of inference and axioms;
thus the theory is an object of formal logic. The models are sets with structure.
The natural notion of morphism is that of elementary embedding. The reason
for this is that inequality is always a stateable predicate.
In our treatment, the theory is a category with certain properties (FP, LE, etc.
as in Chapter 4) and extra structure (a topology, as in Chapter 8), the models
are functors to other categories with appropriate structure, and morphisms of
models are natural transformations of these functors. This almost always gives
the correct class of morphisms.
Categorical theories were devmloped in two contexts and from two di¬erent
directions. One was by Grothendieck and his school in the context of classifying
toposes (Grothendieck [1964]). These are, essentially, our geometric theories as
in Chapter 8. The other source was the notion of (¬nitary) equational theories
4.5 Notes on Theories 171
due to Lawvere [1963]; they are our single-sorted FP theories. Thus these two
sources provided the top and bottom of our hierarchy.
The Grothendieck school developed the idea of the classifying topos for a type
of structure in the late 1950™s. Because of the name, we assume that they were
developed by analogy with the concept of classifying space in topology.
In the 1960™s, Lawvere invented algebraic theories (our single-sorted FP the-
ories) quite explicitly as a way of describing algebraic structures using categories
for theories and functors for models. His work is based on the concept of G.
Birkhoªs equational classes. Of course, Birkho did not describe these in terms
of categories, nor was his concept of lattice useful in this connection. The latter
was primarily useful for describing the classes of subobjects and quotient objects.
Models were described in semantic terms and it seems never to have occurred to
anyone before Lawvere that the theory of groups could be thought of as a generic
group. Lawvere™s seminal observation that the theory of groups, for example, is a
category with a group object, that a group in Set is a product preserving functor
and that a morphism of groups is a natural transformation of functors is an idea
of a di¬erent sort, rather than just an extension of existing ones.
Lawvere™s work was limited to ¬nitary equational theories, and it was Linton
[1966], [1969a] who extended it to in¬nitary theories (not covered in this book)
and made precise the relation with triples. It became clear very early that the
study of in¬nitary theories becomes much more tractable via the Lawvere-Linton
approach.
Lawvere alluded to multisorted FP theories in his thesis and even asserted
“ incorrectly “ that the category of algebras for a multisorted theory could be
realized as algebras for a single-sorted theory. Multisorted algebraic theories have
recently found use in theoretical computer science; see Barr and Wells [1999].
An early attempt at extending theories beyond FP was Freyd™s “essentially
algebraic theories” [1972], which are subsumed by our LE theories. The idea of
de¬ning algebraic structures in arbitrary categories predates Lawvere™s work; for
example Eckmann-Hilton [1962]. See also B´nabou [1968], [1972].
e
Somewhere along the line it became clear that algebraic theories had clas-
sifying toposes and that Lawvere™s program of replacing theories by categories,
models by functors and morphisms by natural transformations of those functors
could be extended well beyond the domain of equational theories.
Ehresmann introduced sketches in the late 1960™s as a way of bringing the
formal system closer to the mathematician™s naive description. (Our notion of
sketch is even more naive than his. However, the kinship is clear and we are only
too happy to acknowledge the debt.) The development of the categorical approach
to general theories constituted the major work of the last part of his career.
The presentation in Bastiani-Ehresmann [1973] (which contains references to his
172 4 Theories
earlier work) is probably the best starting place for the interested reader. Our
description of sketches and induced theories is very di¬erent from Ehresmann™s.
In particular, he constructs the theory generated by a sketch by a direct trans¬nite
induction rather than embedding in models and using Kennison™s Theorem. (See
Kelly [1982] for a general report on the use of trans¬nite induction in this area.)
Ehresmann™s sketches are based on graphs with partial composition rather
than simply graphs, but as is clear from our treatment in Section 4.1, the tran-
sition is straightforward.
The connection between logical theories and categorical theories was explored
systematically by Makkai and Reyes (two logicians!) [1977] who showed that
when restricted to geometric theories the two were entirely interchangeable. See
also Lambek and Scott [1986] and Bunge [1983].
With the advent of toposes and geometric morphisms from Lawvere-Tierney,
the theory of geometric theories reached its full fruition. What was left was only
to ¬ll in the holes “ special cases such as regular and ¬nite sum theories. This
was more or less clear to everyone (see Lawvere [1975]) but we have the ¬rst
systematic treatment of it.
5
Properties of Toposes
In this chapter we will develop various fundamental properties of toposes. Some
of these properties are familiar from Set; thus, every topos has ¬nite colimits
and has internal homsets (is Cartesian closed). Others are less familiar, but are
technically important; an outstanding example of this sort of property is the fact
that if E is a topos then so is the category E /A of objects over an object A of E .
Our treatment makes substantial use of triple theory as developed in Chapter 3.


5.1 Tripleability of P
[Par´] P: E op ’ E is tripleable.
Theorem 1. e ’
Proof. We will use the Crude Tripleability Theorem (Section 3.5). P has a left
adjoint, namely Pop (Proposition 3 of Section 2.3). E op has coequalizers of re-
¬‚exive pairs, indeed all coequalizers, because E has all ¬nite limits. The other
properties, that P re¬‚ects isomorphisms and preserves coequalizers of re¬‚exive
pairs, follow from Lemmas 4 and 5 below.
Before proving these lemmas, we illustrate the power of this theorem with:
Corollary 2. Any topos has ¬nite colimits.
Proof. By Theorem 1 of 3.4, a category of algebras E T for a triple T on a category
E has ¬nite limits if E does, but E op having limits is equivalent to E having
colimits.
The same argument implies that a topos has colimits of any class of diagrams
that it has limits of. The converse of this is also true (Exercise 1).
Observe that for any topos E , the functor T = P —¦ P is a covariant endofunctor
of E . Since T is the composite of a functor and its right adjoint, it is the functor
part of a triple (T, ·: 1 ’ T, µ: T 2 ’ T ).
’ ’
For any object A of E , ·A: A ’ PPA is monic.
Lemma 3. ’
Proof. The singleton map {}: A ’ PA is monic by Proposition 1 of Section 2.3,

so {} —¦ {}: A ’ T A is also monic. The Lemma then follows from Exercise 7 of

section 3.1.

173
174 5 Properties of Toposes
Lemma 4. P re¬‚ects isomorphisms.
Proof. Suppose f : B ’ A in E and suppose Pf is an isomorphism. Then so is

PPf . In the commutative diagram
f
A' B

<<

. 32
( 60 .)



>>