‚

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