Todd Trimble An elementary approach to elementary topos theory

Contents

Introduction

There are many students and researchers outside of category theory who have heard about categorical approaches to “mathematical foundations”, and eager to learn more. Perhaps they heard for instance about “categorical set theory” such as Lawvere’s ETCS: the Elementary Theory of the Category of Sets. Or, they may have heard that topos theory can be seen as “generalized set theory”, and heard about some of its selling points. For example, how categorical set theory is structural, i.e., is set up so that the chief concepts are invariant with respect to isomorphism. From this point of view, the “stuff” that sets are made of (elements, elements of elements, …) is not important, but how sets are interconnected through functions and relations is important, as is the way sets are used by mathematicians which is through universal properties. Another selling point is that topos theory is said to be more flexible and general than ordinary set theory: all the familiar forms of set theory such as ultrapowers, forcing extensions, etc. form toposes, but there are many other toposes of quite different character, worlds of set-like objects tailored more directly to the intuitions and language native to particular problem environments: petit toposes like sheaves over a space, or classifying toposes in algebraic geometry for expressing things like etale cohomology, synthetic differential geometry for nilpotent infinitesimals and function spaces, realizability toposes for recursive function theory, linguistically constructed logical toposes, … This is exciting, and consequently there is a demand and market for introductory accounts.

However, such readers may be dismayed by the technical demands the standard introductory accounts make. A student who turns for example to the (deservedly) well regarded graduate text Sheaves in Geometry and Logic by Mac Lane and Moerdijk, to learn about “First properties of elementary topoi” (Chapter IV), may be surprised by how much categorical background is actually needed. Even to construct very basic things like finite coproducts and quotients, the reader is expected to become familiar with properties of monadic functors, the crude monadicity theorem, Beck-Chevalley conditions, and other technical methods and results – not the type of thing one usually associates with “set theory”. One could understandably walk away believing that topos theory is something only for specialists, nothing at all like set theory but some abstruse and intimidating categorical development. And to set theorists who were told that topos theory and various offshoots offer an alternative and viable categorical approach to set-theoretic foundations, this situation may seem totally out of hand, even ridiculous.¹

Even for professional category theorists, the connection between (to them) standard techniques and the naive set-theoretic principles we grew up may seem pretty remote. Coproducts are basically just disjoint unions, right? Do we really need recondite and non-direct arguments to prove their existence in an elementary topos? The standard approach (based on elegant but slightly tricky arguments first published by Paré) is to show that the contravariant power (i.e., power set, power object) functor on a topos is monadic. The monad itself is the double power functor, and the monadicity theorem requires consideration of two or three iterations of the monad, so prima facie up to five or six applications of the power functor are involved in the construction of finite colimits. Meanwhile, in ordinary mathematics, it’s somewhat rare to go beyond three iterations of power set: our brains are not that well equipped to visualize such higher-order constructions, and manipulations become more or less exercises in formal reasoning.

In other words, even after one is convinced that the constructions work, it doesn’t give a very “common sense” way to view coproducts or coequalizers. A likely result is that one treats colimits in elementary toposes as sitting in a black box: they’re there, but almost impossible to see directly.² To get beyond that point, one has still more work to do (and frequently the textbooks don’t go into this). Surely an uncomfortable situation, particularly in a classroom setting.

My PhD thesis adviser was Myles Tierney; he and Bill Lawvere founded elementary topos theory. Myles and I would sometimes talk about such things: he longed for a “naive topos theory” just as viable and available for use by working mathematicians as ordinary naive set theory. On one occasion – either in his office or during a short elevator ride to his office in Hill Center – he outlined for me a program for obtaining all the exactness properties of a topos (i.e., the finitary hypotheses in Giraud’s theorem characterizing Grothendieck toposes), in a manner more elementary and natively set-theoretic than the accounts I knew from graduate textbooks. This conversation, which occurred decades ago, has been at the back of my mind ever since.

In memory of this fine gentleman and scholar, my goal is to try to reproduce and fill in details of Myles’s brief outline to me. (It was, in my possibly faulty memory, very brief indeed – it took him perhaps as few as 90 seconds to get it across.) I don’t know if the approach I will take here is exactly what he had in mind, or whether it will have more appeal for many who have struggled with the standard treatments. But if nothing else, I hope to prove existence of colimits in a topos (as well as all the other basic properties) in a way closer to common sense reasoning, eschewing technical monadicity theorems and such, and using formulas and constructions that appeal directly to naive set theory intuitions.

These notes will nevertheless give a self-contained account of all of the standard categorical properties of an elementary topos, summarized by saying that a topos is a locally cartesian closed Heyting pretopos (in particular an effective regular extensive category with finite colimits, covering all those conditions of Giraud’s theorem that are “elementary”). To keep this account within a manageable number of pages, I simply must make robust use of the language of categorical algebra. Thus, I make no apology for bandying about properties of adjoint functors or cartesian closed categories or other core concepts of category theory.

A central result of elementary topos theory, and certainly of this account, is the slice theorem: if $\mathbf{E}$ is a topos, then so is the slice category $\mathbf{E}/X$ over any object $X$. (Freyd and Scedrov dub this “the fundamental theorem of topos theory”.) These notes have been arranged so that, save a few preliminary observations, almost everything flows out from this one result. The main constructions for the slice, particularly of power objects, can be justified intuitively without much pain, and for a teacher of an introductory course I think that would be reasonable to go into. The proof of the slice theorem, while not nightmarish, is somewhat technical and so I have relegated it to an appendix. It is not necessary to know the proof to understand and appreciate the consequences.

(Actually what I present is a more powerful but more technical-looking result: that the category of coalgebras of a pullback-preserving comonad on a topos is again a topos, with a weaker hypothesis than “lex” or finite-limit-preserving comonad. This neatly combines the slice theorem with the lex comonad theorem, with hardly more effort than either, and I am convinced this is a good way to go for future topos theory textbooks. However, for some reason a published account of the pullback-preserving comonad result is virtually nonexistent; the result is briefly mentioned in Johnstone’s “Elephant”) but not proven there. On a personal note: this result was something Myles and I worked out for fun when I was a grad student, around 1987 or so, before finding out it was already known to some people at least.)

The main mathematical consequence of the slice theorem is the local cartesian closure of toposes, and more particularly the stability of colimits under pullback, an enormously important fact. More philosophically, the moral of the slice theorem is it provides a theoretical basis and methodological bridge for crossing from naive set theory over to topos theory, and particularly for developing the internal logic of a topos.

Generally, the method starts with writing down set theory propositions in terms of ordinary elements (formulated categorically, as points $x: 1 \to X$). Now, the slice theorem guarantees that whatever is provable for a general topos $\mathbf{E} \simeq \mathbf{E}/1$ is also provable for a slice $\mathbf{E}/U$, and this allows us to relativize statements and constructions: statements formulated in terms of ordinary points $1 \to X$ may be restated and proven for more general “points” $U \to X$ over arbitrary domains $U$. Finally, by instantiating at the “generic point” $1_X: X \to X$, a maneuver reminiscent of the Yoneda lemma, one arrives at the “right” corresponding construction or proposition for topos theory, one that is stable and internally correct.

With these points in mind, we may begin our account proper, starting with the systematic construction of the internal logic.³ At first, the “logic” is quite parsimonious: it’s just equational logic, or logic expressible in terms of products and equalizers. Bit by bit one constructs internal logical operators in a topos, starting with the “negative” operators $\wedge$, $\Rightarrow$, and $\forall$. This gives us enough to write down a formula for internal intersection $\bigcap$, a crucial step. With this step, we see that lattices of subobjects are internally complete (closed under arbitrary internal meets), and therefore also internally cocomplete (closed under internal joins), and this puts us on the path to constructing logical operators on the “positive formula” side: $\vee$, $\exists$, $\bigcup$.

Finally we put the internal logic to use to construct finite colimits. The main problem is figuring out how to exploit “local colimits” (joins in subobject lattices) to create “global colimits”. For example, coproducts are obtained by figuring out how to create disjoint unions. (This approach, together with stability, makes automatic the fact that toposes are extensive categories.) For coequalizers, the key turns out to be constructing first the image factorization, whence we proceed essentially by a series of familiar set-theoretic maneuvers that guide us towards constructing coequalizers of equivalence relations. We’ll save the punch lines for later, but the fact that colimits are stable leads quickly to the conclusion that toposes are effective regular categories, as a natural by-product, and with this we may conclude our account.

In theory this account could be read by someone with only slight prior exposure to topos theory, or even just a decent course in basic category theory, but the readers I am most interested in reaching are those who already have some experience with topos theory as student and perhaps also as lecturer⁴, and who share my feeling that there is indeed something formidable about the standard developments, and that a different approach is worth a shot. I’m hoping this article could even serve as a detailed source of working notes for someone who is considering teaching elementary topos theory.

As intimated above, the development I have undertaken here owes a great deal to my PhD adviser Myles Tierney, to whom I dedicate this work. I also thank André Joyal, Tom Leinster, and David Roberts for expressing their interest in this approach, which in the end encouraged me to finish writing this up.

Definition

We adopt the power-set or power-object definition of elementary topos:

Intuitively, the power-set definition of topos concerns the interplay between categories of sets and relations and the category of sets and functions, which maps faithfully into sets and relations: it says that this faithful “inclusion” functor

has a right adjoint $P$. Here “relations” from $B$ to $A$, denoted $R: B \nrightarrow A$, are by definition subobjects of $B \times A$, i.e., isomorphism classes of monomorphisms into $B \times A$. The inclusion functor $i$ takes a function $f: X \to Y$ to its corresponding functional relation $i(f) = (X \stackrel{\langle 1_X, f \rangle}{\hookrightarrow} X \times Y$).

With the hindsight (foresight?) that toposes are indeed regular categories, with the consequence that relations may be decently composed and $Rel(\mathbf{E})$ forms a category, this observation becomes a precise definition: a topos is a regular category such that $i: \mathbf{E} \to Rel(\mathbf{E})$ has a right adjoint. The components of the counit of $i \dashv P$ are relations of the form

with the intent that any relation $R: i(B) \nrightarrow A$ factors uniquely through $\ni_A$ via the underlying relation of a function $\chi_R: B \to P A$:

Exploring this further, the unit of the adjunction $A \to P i A$, which is the classifying map of the identity relation $1_A: A \nrightarrow A = \delta_A: A \to A \times A$, is the singleton function $\sigma_A: A \to P A$. Looking further ahead, the multiplication of the monad $P$ (now suppressing $i$‘s) is the classifying map $P P A \to P A$ of the composite relation:

Set-theoretically, the composite relation is $\{(\mathcal{F}, a): \exists_{F: P A} \mathcal{F} \ni F \wedge F \ni a\}$; its classifying map is the union operation $\bigcup_A: P P A \to P A$.

The power $P 1$ of the terminal object $1$ plays a special role; it is familiarly known as the subobject classifier $\Omega$.

Thus the universal subobject is of the form $t: 1 \to \Omega$. An alternative way of stating the universality is that every monic $i: A \hookrightarrow X$ is the equalizer of a diagram

for some unique choice of map $\chi_i: X \to \Omega$. This has several immediate consequences:

Cartesian closure

There is of course another familiar definition of elementary topos, in which cartesian closure and the subobject classifier $\Omega$ are basic. To get from Definition to the other definition involves some slightly fiddly details (the other direction is easier), but basically the cartesian closure comes about in two steps:

• For a power object $P A$ and object $B$, the exponential $P(A)^B$ is given by $P(A \times B)$. Indeed, the adjunction $i \dashv P$ gives natural bijections between arrows
  $$\array{\arrayopts{\rowlines{solid}} X \times B \to P A\;\;\; in\; \mathbf{E} \\ X \times B \nrightarrow A\;\;\; in\; Rel(\mathbf{E}) \\ X \nrightarrow A \times B\;\;\; in\; Rel(\mathbf{E}) \\ X \to P(A \times B)\;\;\; in \; \mathbf{E} }$$

  so that $P(A \times B)$ satisfies the universal property expected of $(P A)^B$. In other words, cartesian closure in $\mathbf{E}$ is closely related to the compact closure of $Rel(\mathbf{E})$. The detailed proof of this step is easily extracted from this short computation.

In particular, we have a natural isomorphism $P A \cong (P 1)^A = \Omega^A$. Read this way, we have contravariance in the argument $A$, i.e., $A \mapsto P A$ is the object part of the contravariant power object functor.

• The singleton map $\sigma A: A \to P A$ is monic, as we will show in a moment, and thus defines a relation $P A \; ⇸ \; 1$ classified by a map $\chi_{\sigma A}: P A \to P 1$. Thus we have a pullback
  $$\array{ A & \to & 1 \\ \mathllap{\sigma A} \downarrow & & \downarrow \mathrlap{t} \\ P A & \underset{\chi_{\sigma A}}{\to} & P 1 }$$

  where the subdiagram consisting of the three objects $P A$, $P 1$, $1$ and the two morphisms between them admit exponentials with exponent $B$. It is easy to verify that the pullback of the exponentiated subdiagram gives the exponential $A^B$.

For this we need to show that the singleton map $\sigma A$ is monic.

This is obvious from the point of view that the unit $\sigma: 1 \to P i$ of an adjunction $i \dashv P$ is monic whenever the left adjoint $i$ is faithful. The proof below is a more formal working out.

Slice theorem

A major qualitative distinction between the vanilla category of sets $Set$ and a general topos $\mathbf{E}$ is that sets $X$ are determined by their points $1 \to A$ (and functions are determined by what they do to points). For a general topos $\mathbf{E}$, this is much too restrictive; for example, sheaves of sets generally form a topos, but a general sheaf is hardly determined by its points $1 \to A$ (which are global sections of $A$). In fact, $A$ may be a highly nontrivial sheaf and yet not have any such points at all: consider for example the principal $\mathbb{Z}/(2)$-bundle over $S^1$ associated with the Möbius strip, living in $Sheaves(S^1)$, which has no global sections.

Instead, in accordance with the Yoneda lemma, objects $A$ are determined up to isomorphism by maps $X \to A$ into $A$, which one sometimes calls “generalized points”. Thus, instead of constant points $1 \to A$, we should consider variable points $X \to A$ with variation over other domains $X$. But in fact these can be reconstituted again as ordinary points $1 \to A$ if we switch our point of view to a universe of “variable objects” $\mathbf{E}/X$. That is to say: an object $A$ of $\mathbf{E}$ can be reinterpreted along a map $X^\ast: \mathbf{E} \to \mathbf{E}/X$ which sends $A$ to $\pi: X \times A \to X$. The generic point $1$ is thereby interpreted in $\mathbf{E}/X$ as $X^\ast 1 = 1_X: X \to X$, and then a point or global section $X^\ast 1 \to X^\ast A$ in $\mathbf{E}/X$ is exactly tantamount to a generalized point $X \to A$ back in $\mathbf{E}$.

So we can, in topos theory, perform arguments and constructions naively as if with “points” $1 \to A$, provided that we consider them uniformly across all slices $\mathbf{E}/X$.⁵

So our first major task is to prove the slice theorem, which says that if $\mathbf{E}$ is a topos, then also the slice $\mathbf{E}/X$ of objects “varying over $X$” is a topos, and moreover that the interpretation functor $X^\ast: \mathbf{E} \to \mathbf{E}/X$ preserves all conceivable topos structure, i.e., is a “logical functor” and has adjoints on both sides (so that any limits or colimits that $\mathbf{E}$ has are preserved under reinterpretation).

Notice that this point of view signals a major departure from ZFC since, for example, a slice of a model of ZFC (more precisely, a category $Set$ formed from a model of ZFC) is not itself a model of ZFC; rather it is some Boolean-valued model. Of course, toposes are far more general still than mere slices of ZFC models, but the takeaway here is that the notion of topos is closed with respect to moving to universes of greater variability, while still retaining fundamental set-like features.

Intuitive view

It is not hard to guess what the topos structure of $\mathbf{E}/X$ looks like, based on the special case $\mathbf{E} = Set$. In this special case, an object $f: Y \to X$ may be regarded as equivalent to a function $X \to Set$ which sends $x \in X$ to the fiber $Y_x = f^\ast(\{x\})$, and indeed $Set/X$ is equivalent to the category $Set^X$ of functors $X \to Set$ (from $X$ as discrete category). Here $Set^X \simeq Set/X$ carries obvious pointwise-defined topos structure, so that the power object of $f: Y \to X$ is the fiberwise power set $x \mapsto P(Y_x)$. Thus $P(Y_x)$ is the fiber over $x$ of the power object.

Assembling these fibers into a total set $P_X(Y, f) \to X$ over $X$, we may describe elements of $P_X(Y, f)$ as pairs $(x \in X, S \in P(Y))$ such that $S \subseteq Y_x = f^\ast(x)$. This inclusion may be expressed as an equation: consider the function $\langle f, 1 \rangle: Y \to X \times Y$; then the equation is

and so if we like, we can describe the elements of the power object $P_X(Y, f)$ as fixed points $(x, S) \in X \times P(Y)$ of the (idempotent) operator $X \times P Y \to X \times P Y$ defined by the composite

Considered as a set $P_X(Y, f) \to X$ over $X$, such a fixed point $(x, S)$ of course maps to $x$.

This in fact is how we proceed below (except we generalize even further).

Coalgebras of pullback-preserving comonads

As mentioned in the introduction, the slice theorem and the theorem on lex (= left exact) comonads on a topos can be proved together in one fell swoop. We observe that the functor $X \times -: \mathbf{E} \to \mathbf{E}$ carries a comonad structure with comultiplication induced from $\delta: X \to X \times X$ and counit induced from $!: X \to 1$. A coalgebra of this comonad is a map $\langle f, 1_A \rangle: A \to X \times A$, tantamount to a single datum $f: A \to X$, and coalgebra maps $(A, f) \to (B, g)$ boil down to maps $h: A \to B$ making the obvious triangle commute. In other words, the category of coalgebras of $X \times -: \mathbf{E} \to \mathbf{E}$ is equivalent to the slice $\mathbf{E}/X$.

This comonad $X \times -$ is not left exact, but it does preserve pullbacks. The theorem we prove is this:

We return to the proof of Theorem ; it remains to show that the equalizer $j: P_G(Y) \to G P Y$ of the pair of maps in (2) is the power object of the coalgebra $(Y, \eta: Y \to G Y)$. Let $(X, \theta: X \to G X)$ be a coalgebra, and $f: X \to P_G(Y)$ a coalgebra map. Then $g = j f: X \to G P Y$ equalizes the maps in (2). Moreover, since $G P Y$ is cofree, we have that to each $G$-coalgebra map $g: X \to G P Y$, there exists a unique $h: X \to P Y$ in the topos $\mathbf{E}$ such that

Thus $g: X \to G P Y$ in $\mathbf{E}_G$ or $h: X \to P Y$ in $\mathbf{E}$ corresponds to a subobject $i: R \hookrightarrow X \times Y$ in $\mathbf{E}$. We need to check that the condition that $g$ equalizes the pair of maps in (2) corresponds precisely to the condition that $R$ is a subcoalgebra of $X \times_{G 1} Y$ (the product of $X$ and $Y$ in $\mathbf{E}_G$). Or, taking into account Lemmas and : precisely to the condition that there is a pullback diagram in $\mathbf{E}$ of the form

where $\gamma$ is the coalgebra structure on $X \times_{G 1} Y$, and $k$ is monic.

The hard part is over. Much simpler is the observation that in the slice topos case, the right adjoint $X^\ast: \mathbf{E} \to \mathbf{E}/X$ to the forgetful functor $\Sigma_X: \mathbf{E}/X \to \mathbf{E}$ is a logical functor, i.e., preserves finite limits and power objects.

Consequences of the slice theorem

We see now that for a topos $\mathbf{E}$, each slice $\mathbf{E}/X$ is cartesian closed (and of course finitely complete). We say that $\mathbf{E}$ is locally cartesian closed.

Therefore $X^\ast: \mathbf{E} \to \mathbf{E}/X$, in addition to being a logical functor between toposes, is also a left adjoint and a right adjoint.

For instance, once we prove that coproducts $X + Y$ exist, with monic and disjoint coproduct inclusions $X \to X + Y$ and $Y \to X + Y$, then armed with the fact that coproducts are stable under pullback, we obtain the result that toposes $\mathbf{E}$ are extensive categories.

Similarly, once we show that coequalizers exist, we infer (from their stability under pullback) that toposes are regular categories. As part of this, we will exhibit the (regular epi)-mono factorization of a map $f: X \to Y$.

Internal logic

One respect which sets topos theory apart from ordinary set theory is that a topos has its own form of “internal logic”. In the most familiar topos $Set$, this logic will be the one we are all familiar with: good old-fashioned logic with two truth values $true$ and $false$, formulas which are manipulated according to the laws of Boolean algebra, and quantification with the familiar meanings of “all” and “some”.

However, in working with a general topos, some of these expectations must be adjusted. In general there may be many truth values (which are points $1 \to \Omega$), and some of the cozy comforts of classical logic (the law of excluded middle for example) must be abandoned in general – not out of some whim or philosophical attraction to intuitionism, but because that’s simply the way things turn out to be in the inner world of a general topos.

For people whose experience with formal logic has been in terms of truth tables and the laws of Boolean algebra, and various reductions which say that the operations $\neg, \wedge, \forall$ are enough, there is inevitably a learning curve here. Readers of standard texts may be assisted by various formal devices which give rules for reasoning in a general topos, such as the Mitchell-Bénabou language and Kripke-Joyal semantics. All that is fine, but what I want to emphasize in these notes is what logic (broadly conceived) is really, to use the words of Lawvere: an interlocking system of certain types of adjoint functors. The sooner one thinks of the logical operations as no longer described by truth table assignments or Venn diagrams and the like but directly in terms of universal properties, the quicker the process will be.

Thus, internal logic is simply a reflection of the categorical properties one can infer about posets of subobjects ordered by inclusion, and functors (such as pullback functors) between them. For example, logical conjunction reflects meets which are cartesian products in $Sub(X)$; logical disjunction reflects joins which are coproducts in $Sub(X)$. Logical implication reflects how $Sub(X)$ is (as we shall see) cartesian closed. And quantification, according to one of the great lessons taught by Lawvere, is a reflection of there being an adjoint (on one side or the other) to pullback functors of the form $f^\ast: Sub(Y) \to Sub(X)$. The rules of inference for logic in a general topos are just those we can derive from such adjoint relationships and general results such as the slice theorem, which guarantees that pullback functors $f^\ast: \mathbf{E}/Y \to \mathbf{E}/X$ are logical functors with adjoints on both sides. Such rules will be developed as we go along.

Internal versus external

In developing of the internal logic of a topos $\mathbf{E}$, a useful heuristic⁶ is that the subobject classifier $\Omega$ represents, more or less by definition, the contravariant functor $Sub: \mathbf{E}^{op} \to Set$ mapping an object $X$ to its set of subobjects $Sub(X)$, and mapping a morphism $f: X \to Y$ in $\mathbf{E}$ to the function $Sub(f) = f^\ast(-): Sub(Y) \to Sub(X)$ that sends a subobject $i$ of $Y$ to its pullback (aka inverse image) along $f$, as a subobject of $X$:

In more detail, the heuristic is first to interpret familiar logical operations, for example conjunction, as natural operations on subobjects, for example the intersection operator

which takes a pair of subobjects to their pullback. This is the external view.

Second, by the representability, this corresponds to a natural transformation

or to a natural transformation $\hom_\mathbf{E}(-, \Omega \times \Omega) \to \hom_\mathbf{E}(-, \Omega)$, which by the Yoneda lemma corresponds to a morphism in $\mathbf{E}$,

called “internal conjunction” or “internal meet”. This is the internal view. Basically one builds up the internal logic of a topos by playing the external and internal views off of each other, building up a repertoire of internal logical operations.

Building up the logical operations proceeds in a certain order: in some sense the definition of topos is naturally “biased” towards negative types (finite limits, exponentials) and so it is natural to begin with the correspondingly negative logical operations: $t = true$, $\wedge$, $\Rightarrow$, $\forall$, before tackling the positive operations: $\bot = false$, $\vee$, $\exists$.

Internal meet

Let us now work through this procedure to construct the internal meet in more detail. In the first place, the isomorphism $\hom_\mathbf{E}(-, \Omega) \stackrel{\sim}{\to} Sub(-)$ is given, à la Yoneda, by a representing or universal element in $Sub(\Omega)$. This of course is the universal subobject $t: 1 \hookrightarrow \Omega$.

Now, the external operation $\cap: Sub(X) \times Sub(X) \to Sub(X)$ is natural: given $f: X \to Y$, the diagram

commutes because $f^\ast$ preserves pullbacks. By representability and Yoneda, the natural transformation $\cap$ is classified by a map $\Omega \times \Omega \to \Omega$ produced by chasing an identity element as follows (now using $\mathbf{E}(a, b)$ as abbreviation of $\hom_\mathbf{E}(a, b)$):

Here $\pi_1^{-1}(t) = (1 \times \Omega \stackrel{t \times 1_{\Omega}}{\to} \Omega \times \Omega)$ and $\pi_2^{-1}(t) = (\Omega \times 1 \stackrel{1_{\Omega} \times t}{\to} \Omega \times \Omega)$; their intersection is $1 \times 1 \stackrel{t \times t}{\to} \Omega \times \Omega$. Thus the internal meet is $\wedge = \chi_{t \times t}: \Omega \times \Omega \to \Omega$. The basic properties of $\wedge$ (associativity, commutativity, idempotence) follow immediately from the corresponding properties of the external operation $\cap$ (which in turn are argued by applying universal properties of pullback). The unit of $\wedge$ is of course $t: 1 \to \Omega$, which is the maximal element (i.e., classifies the maximal subobject $1_\Omega$).

Internal implication

Now we construct an internal implication operator $\Rightarrow: \Omega \times \Omega \to \Omega$, corresponding to a natural external operation $\Rightarrow_X: Sub(X) \times Sub(X) \to Sub(X)$ on subobjects that is appropriately adjoint to $\wedge$, i.e., satisfies

for subobjects $A, B, C$ of $X$.

In this case it is not immediately obvious that there is such an external operation, but obviously it is unique if it exists, and one can try to work out what the corresponding internal operation would look like. We start by working our way to the external view: the internal operation $\Rightarrow$ would be the classifying map of the subobject $\Rightarrow^\ast(1 \stackrel{t}{\to} \Omega)$, and so we proceed to analyze this subobject.

A point $1 \stackrel{\langle u, v \rangle}{\to} \Omega \times \Omega$ belongs to (i.e., factors through) the subobject $\Rightarrow^{-1}(t) \hookrightarrow \Omega \times \Omega$ if and only if $t = u \Rightarrow v$. The same holds true for generalized points $X \stackrel{\langle u, v \rangle}{\to} \Omega \times \Omega$, where now “$t$” is interpreted by pulling back along $X \to 1$, i.e., we define $t_X = X \stackrel{!}{\to} 1 \stackrel{t}{\to} \Omega$: this is the universal subobject $t: 1 \to \Omega$ when interpreted in the topos $\mathbf{E}/X$. (Remember that the pulling-back functor $X^\ast: \mathbf{E} \to \mathbf{E}/X$ is logical.) In general, points $u, v: 1 \to \Omega$ in $\mathbf{E}/X$ correspond to maps $u, v: X \to \Omega$ in $\mathbf{E}$.

Thus, working in a general slice $\mathbf{E}/X$, let us interpret the condition $t = u \Rightarrow v$, passing now to the external picture. If $[u]$ denotes the subobject of the terminal classified by the point $u$, then the external condition $[t] = [u] \Rightarrow [v]$ is equivalent to the condition $[t] \hookrightarrow [u] \Rightarrow [v]$ (since $[t]$ is maximal), which by the adjunction would be equivalent to $[t] \cap [u] \hookrightarrow [v]$, or just $[u] \hookrightarrow [v]$. Let us write this as $[u] \subseteq [v]$, in keeping with set-theoretic notation.

Thus we define $\Rightarrow: \Omega \times \Omega \to \Omega$ to be the classifying map of the subobject of $\Omega \times \Omega$ consisting of points $(u, v)$ such that $[u] \subseteq [v]$ (uniformly over all slices). This last condition coincides with $[u] = [u] \cap [v]$, and so to complete the construction we define the subobject $(\subseteq) \hookrightarrow \Omega \times \Omega$ to be the equalizer of the two maps

It remains to check that this works as advertised: that for points $u, v, w: 1 \to \Omega$ we have (externally)

(again, as always now, this is meant to be interpreted over all slice toposes). The condition on the right means that any (generalized) element $e$ of $[u]$ satisfies $[v(i e)] \subseteq [w(i e)]$, where $i$ is the inclusion $[u] \to 1$. It is sufficient to consider the generic element where $e = 1_{[u]}$, where we have a pullback

from which we see $[v(i e)] = [u] \cap [v]$. Thus the condition on the right is $[u] \cap [v] \subseteq [u] \cap [w]$; as this is equivalent to $[u] \cap [v] \subseteq [w]$, we are done.

Internal universal quantification

So far we have dealt just with propositional logic, internalized in terms of operations $\Omega^n \to \Omega$ within the topos $\mathbf{E}$. These operations pull back to any slice $\mathbf{E}/X$, and externalize to operations on $Sub(X)$ over each individual object (or “type”) $X$.

In predicate logic, quantification involves operations that change the type: if $\phi: X \times A \to \Omega$ is a predicate of type $X \times A$, then quantification over $A$ produces a predicate of type $X$, e.g., $\forall_A \phi: X \to \Omega$. Externally, universal quantification is a natural operation $Sub(X \times A) \to Sub(X)$. Internally, universal quantification is given by a map

which classifies a subobject $\forall_A^\ast(t) \hookrightarrow P A$. An element $\phi: 1 \to P A$ belongs to (factors through) $\forall_A^\ast(t)$ if $t = \forall_A \phi$. In ordinary logic terms, this should mean $\phi(a) = t$ for all elements $a$ of $A$, i.e., that $\phi$ is constantly true over all of $A$: $\phi = t_A = (A \to 1 \stackrel{t}{\to} A)$. This leads us to conclude that $\forall_A^\ast(t) = t_A: 1 \hookrightarrow P A$, and therefore that

The fundamental property of universal quantification, originally observed by Lawvere, is as follows.

The other half of Lawvere’s insight is that existential quantification is left adjoint to pulling back. We will come to this later.

One import of this insight is that quantification has a wider meaning than is found in traditional logic: whereas the traditional quantification $\forall_{a: A} \phi(x, a)$ has to do with a right adjoint to pulling back along a projection map $\pi_1: X \times A \to X$ (in $Set$), in principle we can consider a right adjoint to pulling back along any map $f: Y \to X$. One way to consider this is topos theory is that, working in a slice $\mathbf{E}/X$ and considering an object $f: Y \to X$ ….

Internal intersection of definable families

Now we put some of the logic we have developed to use, defining an internal intersection operator

which externally takes a family $F \hookrightarrow P A$ to its intersection $\bigcap F \hookrightarrow A$.

To do this, we simply write down the appropriate logical formula for the relation $R \hookrightarrow P P A \times A$ to be classified by $\bigcap$: it consists of points $(F, a): \forall_{S: P A} (F \ni S) \Rightarrow (S \ni a)$. We remember here the precept that this formula is to be interpreted uniformly over all slices $\mathbf{E}/X$.

Internal union of definable families

Images and existential quantification

Construction of coproducts

We construct coproducts in an elementary topos one does in naive set theory: as disjoint unions. Letting $X, Y$ be sets (objects in an ETCS category), a disjoint union of $X$ and $Y$ is a pair of monos

whose intersection in $Sub(Z)$ is empty (i.e., initial), and whose union or join in $Sub(Z)$ is all of $Z$. We will show that disjoint unions exist and are essentially unique, and that they satisfy the universal property for coproducts. We use the notation $X + Y$ for a disjoint union.

Construction of initial object

We first construct an initial object $0$ by taking the intersection of all subobjects of $1$, i.e., as the subobject $0 \hookrightarrow 1$ classified by the composite

Incidentally, we may now define the negation operator:

Construction of disjoint unions

Disjoint unions are coproducts

Construction of coequalizers

In this section we prove that a topos admits coequalizers; in conjunction with Theorem , this shows that toposes are finitely cocomplete.

But the real motif of this section is the Barr exactness of a topos, which is effectively summarized by a Galois correspondence between equivalence relations on an object $Y$ and regular epimorphisms out of $Y$, stable under pullback. We begin with a few preliminary observations, valid for any category $\mathbf{E}$.

For an object $Y$, let $Rel_Y$ be the class of subobjects of $\langle p_1, p_2\rangle: A \hookrightarrow Y \times Y$. As usual, this class is the partial order reflection of the preorder (thin category) given by the full subcategory of $\mathbf{E}/Y \times Y$ whose objects consist of monomorphisms into $Y \times Y$.

Let $Quot_Y$ be the class of quotients = co-subobjects of $Y$, that is to say equivalence classes of epis $h: Y \twoheadrightarrow Z$. This class is the partial order reflection of the preorder given by the full subcategory of the co-slice $Y/\mathbf{E}$ whose objects consist of epimorphisms out of $Y$ (so $(p: Y \twoheadrightarrow P) \leq (q: Y \twoheadrightarrow Q)$ if there is a map $f: P \to Q$ such that $f \circ p = q$; such an $f$ is unique and necessarily an epi).

There is a fundamental relation between $Rel_Y$ and $Quot_Y$, which we denote as $\perp$, where by definition $\langle p_1, p_2\rangle \perp h$ iff $h p_1 = h p_2$. For $h \in Quot_Y$, let $h^\wedge$ denote the class of $R \in Rel_Y$ such that $R \perp h$. A kernel pair of $h$, if it exists (as it certainly will in any category with pullbacks, for example a topos), is the maximal element of $h^\wedge$. It is denoted $\ker(h)$.

Similarly, for $R = \langle p_1, p_2 \rangle \in Rel_Y$, let $R^\vee$ denote the class of $h \in Quot_Y$ such that $R \perp h$. A coequalizer of the pair $(p_1, p_2)$, if it exists, is the minimal element of $R^\vee$. It is denoted $coeq(p_1, p_2)$ or $quot(R)$.

If kernel pairs and coequalizers exist, then we get a monotone Galois connection between $Rel_Y$ and $Quot_Y$, where $quot: Rel_Y \to Quot_Y$ is left adjoint to $\ker: Quot_Y \to Rel_Y$. That is to say, $quot \langle p_1, p_2 \rangle \leq h$ iff $\langle p_1, p_2 \rangle \leq \ker(h)$, since both sides are equivalent to $h p_1 = h p_2$.

Reduction to quotients

The goal of this section is to show that in order to prove that a topos has coequalizers, it suffices to construct quotients of equivalence relations.

In combination with Corollary , we derive the following consequence.

The next proposition provides a kind of dual form of the preceding proposition and its corollary.

This proposition shows that to construct coequalizers in a topos, it suffices to construct quotients of equivalence relations.

Equivalence relations are effective

By this proposition, we have that $E \leq ker(\chi_E)$ for equivalence relations $E$.

Quotients of equivalence relations

In this subsection we construct quotients of equivalence relations.

It follows from the general theory of pretoposes that all epimorphisms in a topos are regular. However, we can also prove this easily from the theory developed above.

References

• F. William Lawvere, An elementary theory of the category of sets, Proceedings of the National Academy of Science of the U.S.A 52 (1965), 1506-1511. Reprinted in an expanded version, with commentary by Colin McLarty and by Lawvere, in Reprints in Theory and Applications of Categories, No. 11 (2005), pp. 1-35. (link)

• Saunders Mac Lane and Ieke Moerdijk, Sheaves in Geometry and Logic – A First Introduction to Topos Theory, Springer Verlag, 1992.

• Robert Paré, Colimits in Topoi , Bull. AMS 80 (1974) pp.556-561. (pdf)

• Peter Johnstone, Sketches of an Elephant: A Topos Theory Compendium, Oxford University Press, 2002.

• Peter Freyd and André Scedrov, Categories, Allegories, Mathematical Library Vol 39, North-Holland (1990). ISBN 000-0-000-00000-0.

• Michael Shulman, Stack semantics and the comparison of material and structural set theories, (submitted on 21 Apr 2010) http://arxiv.org/abs/1004.3802

• Toby Kenney, Diads and Their Application to Topoi, Applied Categorical Structures 17 (December 2009), 567-590. (Springer link)

• Todd Trimble, Three topos theorems in one, this site.

Endnotes