7.4: Toposes

Toposes

A topos is defined to be a category of sheaves.\(^{9}\) So for any topological space (X, Op), the category Shv(X, Op) defined in Definition 7.35 is a topos. In particular, taking the one-point space X = 1 with its unique topology, we find that the category Set is a topos, as we’ve been saying all along and saw again explicitly in Example 7.48. And for any database schema—i.e. finitely presented category—C, the category C-Inst of database instances on C is also a topos.10 Toposes encompass both of these sources of examples, and many more.

Toposes are incredibly nice structures, for a variety of seemingly disparate reasons. In this sketch, the reason in focus is that every topos has many of the same structural properties that the category Set has. Indeed, we discussed in Section 7.2.1 that every topos has limits and colimits, is cartesian closed, has epi-mono factorizations, and has a subobject classifier (see Section 7.2.2). Using these properties, one can do logic with semantics in the topos E. We explained this for sets, but now imagine it for sheaves on a topological space. There, the same logical symbols \(\land\), \(\lor\), ¬, ⇒, ∃, ∀ become operations that mean something about sub-sheaves—e.g. vector fields, sections of continuous functions, etc.—not just subsets.

To understand this more deeply, we should say what the subobject classifier true : 1 → Ω is in more generality. We said that, in the topos Set, the subobject classifier is the set of booleans Ω = \(\mathbb{B}\). In a sheaf topos \(\mathcal{E}\) = Shv(X, Op), the object Ω \(\in\) \(\mathcal{E}\) is a sheaf, not just a set. What sheaf is it?

The subobject classifier Ω in a sheaf topos

In this subsection we aim to understand the subobject classifier Ω, i.e. the object of truth values, in the sheaf topos Shv(X, Op). Since Ω is a sheaf, let’s understand it by going through the definition of sheaf (Definition 7.35) slowly in this case. A sheaf Ω is a presheaf that satisfies the sheaf condition.

As a presheaf it is just a functor Ω: Op\(^{op}\) → Set; it assigns a set Ω(U) to each open U \(\subseteq\) X and comes with a restriction map Ω(U) → Ω(V) whenever V \(\subseteq\) U. So in our quest to understand Ω, we first ask the question: what presheaf is it?

The answer to our question is that Ω is the presheaf that assigns to U \(\in\) Op the set of open subsets of U:

Ω(U) := {U ′ \(\in\) Op | U ′ \(\subseteq\) U}. (7.50)

That was easy, right? And given the restriction map for V \(\subseteq\) U is given by

Ω(U) → Ω(V) (7.51)

U′ \(\longmapsto\) U′ ∩ V.

One can check that this is functorial see Exercise 7.53—and after doing so we will still need to see that it satisfies the sheaf condition. But at least we don’t have to struggle to understand Ω: it’s a lot like Op itself.

Exercise 7.52

Let X = {1} be the one point space. We said above that its subobject classifier is the set \(\mathbb{B}\) of booleans, but how does that align with the definition of Ω given in Eq. (7.50)? ♦

Exercise 7.53

1. Show that the definition of Ω given above in Eqs. (7.50) and (7.51) is functorial , i.e., that whenever W \(\subseteq\) V \(\subseteq\) U, the restriction map Ω(U) → Ω(V) followed by the restriction map Ω(V) → Ω(W) is the same as the restriction map Ω(U) → Ω(W).
2. Is that all that’s necessary to conclude that Ω is a presheaf? ♦

To see that Ω as defined in Eq. (7.50) satisfies the sheaf condition (see Definition 7.35), suppose that we have a cover U = \(\bigcup_{i \in I} U_{i}\), and suppose given an element V\(_{i}\) \(\in\) Ω(U\(_{i}\)), i.e. an open set V\(_{i}\) \(\subseteq\) U\(_{i}\), for each i \(\in\) I.

Suppose further that for all i, j \(\in\) I, it is the case that V\(_{i}\) ∩ U\(_{j}\) = V\(_{j}\) ∩ U\(_{i}\), i.e. that the elements form a matching family.

Define V := \(\bigcup_{i \in I} V_{i}\); it is an open subset of U, so we can consider V as an element of Ω(U).

The following verifies that V is indeed a gluing for the (V\(_{i}\))\(_{i \in I}\):

\(V \cap U_{j}=\left(\bigcup_{i \in I} V_{i}\right) \cap U_{j}=\bigcup_{i \in I}\left(V_{i} \cap U_{j}\right)=\bigcup_{i \in I}\left(V_{j} \cap U_{i}\right)=\left(\bigcup_{i \in I} U_{i}\right) \cap V_{j}=V_{j}\)

In other words V ∩ U\(_{j}\) = V\(_{j}\) for any j \(\in\) I. So our Ω has been upgraded from presheaf to sheaf!

The eagle-eyed reader will have noticed that we haven’t yet given all the data needed to define a subobject classifier. To turn the object Ω into a subobject classifier in good standing, we also need to give a sheaf morphism true: {1} → Ω. Here {1}: Op\(^{op}\) → Set is the terminal sheaf; it maps every open set to the terminal, one element set {1}.

The correct morphism true: {1} → Ω for the subobject classifier is the sheaf morphism that assigns, for every U \(\in\) Op the function {1} = {1}(U) → Ω(U) sending 1 → U, the largest open set U \(\subseteq\) U. From now on we denote {1} simply as 1.

Upshot: Truth values are open sets. The point is that the truth values in the topos of sheaves on a space (X, Op) are the open sets of that space. When someone says “is property P true?,” the answer is not yes or no, but “it is true on the open subset U.” If this U is everything, U = X, then P is really true; if U is nothing, U = Ø, then P is really false. But in general, it’s just true some places and not others.

Example 7.54

The category Grph of graphs is a presheaf topos, and one can also think of it as the category of instances for a database schema, as we saw in Example 7.23. The subobject classifier Ω in the topos Gr is thus a graph, so we can draw it. Here’s what it looks like:

Finding Ω for oneself is easiest using something called the Yoneda Lemma, but we have not introduced it. For a nice, easy introduction to the topos of graphs, see [Vig03]. The terminal graph is a single vertex with a single loop, and the graph homomorphism true:1 → Ω sends that loop to(V,V ; A).

Given any graph G and subgraph i : H \(\subseteq\) G, we need to construct a graph homomorphism \(lceil{H}rceil\): G → Ω classifying H. The idea is that for each part of G, we decide “how much of it is in H. A vertex in v in G is either in H or not; if so we send it to V and if not we send it to 0. But arrows a are more complicated. If a is in H, we send it (V,V ;A). But if it is not in H, the mathematics requires us to ask more questions: is its source in H? is its target in G”? both? neither? Based on the answers to these questions we send a to (V, 0; 0), (0, V ; 0), (V, V ; 0), or (0, 0; 0), respectively.

Exercise 7.55

Consider the subgraph H \(\subseteq\) G shown here:

Find the graph homomorphism \(lceil{H}rceil\) : G → Ω classifying it. See Example 7.54. ♦

7.4.2 Logic in a sheaf topos

Let’s consider the logical connectives, AND, OR, IMPLIES, and NOT. Suppose we have a topological space X \(\in\) Op.

Given two open sets U,V, considered as truth values U, V \(\in\) Ω(X), then their conjunction ‘U AND V’ is their intersection, and their disjunction ‘U OR V’ is their union;

(U \(land\) V) := U ∩ V and (U \(\lor\) V) := U \(\bigcup\) V. (7.56)

These formulas are easy to remember, because \(land\) looks like ∩ and \(\lor\) looks like \(\bigcup\).

The implication U ⇒ V is the largest open set R such that R ∩ U \(\subseteq\) V, i.e.

\((U \Rightarrow V):=\bigcup_{\left\{R \in \mathbf{O}_{\mathbf{p}} \mid R \cap U \subseteq V\right\}} R .\) (7.57)

In general, it is not easy to reduce Eq. (7.57) further, so implication is the hardest logical connective to think about topologically.
Finally, the negation of U is given by ¬U := (U ⇒ false), and this turns out to be relatively simple.

By the formula in Eq. (7.57), it is the union of all R such that R ∩U = Ø,i.e. the union of all open sets in the complement of U. If you know topology, you might recognize that ¬U is the ‘interior of the complement of U.’

Example 7.58

Consider the real line X = \(\mathbb{R}\) as a topological space (see Exercise 7.27).

Let U, V \(\in\) Ω(X) be the open sets U = {x \(\in\) R | x < 3} and V = {x \(\in\) \(\mathbb{R}\) | −4 < x < 4}. Using interval notation, U = (−∞, 3) and V = (−4, 4). Then

• U \(\land\) V = (−4, 3).

• U \(\lor\) V = (−∞, 4).

• ¬U = (3, ∞).

• ¬V = (−∞, −4) ∪ (4, ∞).

• (U ⇒ V) = (−4, ∞)

• (V ⇒ U) = U

Exercise 7.59

Consider the real line \(\mathbb{R}\) as a topological space, and consider the open subset U = \(\mathbb{R}\) − {0}.

1. What open subset is ¬U?
2. What open subset is ¬¬U?
3. Is it true that U \(\subseteq\) ¬¬U?
4. Is it true that¬¬U \(\subseteq\) U? ♦

Above we explained operations on open sets, one corresponding to each logical connective; there are also open sets corresponding to the the symbols true and false. We explore this in an exercise.

Exercise 7.60

Let (X, Op) be a topological space.

1. Suppose the symbol true corresponds to an open set such that for any open set U \(\in\) Op, we have (true \(\land\) U) = U. Which open set is it?
2. Other things we should expect from true include (true \(\lor\) U) = true and (U ⇒ true) = true and (true ⇒ U) = U. Do these hold for your answer to 1?
3. The symbol false corresponds to an open set U \(\in\) Op such that for any open set U \(\in\) Op, we have (false \(\lor\) U) = U. Which open set is it?
4. Other things we should expect from false include (false \(\land\) U) = false and (false ⇒ U) = true. Do these hold for your answer to 1? ♦

Example 7.61

For a vector bundle π: E → X over a space X, the corresponding sheaf is Secπ corresponding to its sections: to each open set i\(_{U}\) : U \(\subseteq\) X, we associate the set of functions s: U → E for which s ; π = i\(_{U}\). For example, in the case of the tangent bundle π : T M → M (see Example 7.46), the corresponding sheaf, call it VF, associates to each U the set VF(U) of vector fields on U.

The internal logic of the topos can then be used to consider properties of vector fields. For example, one could have a predicate Grad: VF → Ω that asks for the largest subspace Grad(v) on which a given vector field v comes from the gradient of some scalar function. One could also have a predicate that asks for the largest open set on which a vector field is non-zero. Logical operations like \(\land\) and \(\lor\) could then be applied to hone in on precise submanifolds throughout which various desired properties hold, and to reason logically about what other properties are forced to hold there.

7.4.3 Predicates

In English, a predicate is the part of the sentence that comes after the subject. For example “. . . is even” or “. . . likes the weather” are predicates. Not every subject makes sense for a given predicate; e.g. the sentence “7 is even” may be false, but it makes sense. In contrast, the sentence “2.7 is even” does not really make sense, and “2.7 likes the weather” certainly doesn’t. In computer science, they might say “The expression ‘2.7 likes the weather’ does not type check.”

The point is that each predicate is associated to a type, namely the type of subject that makes sense for that predicate. When we apply a predicate to a subject of the appropriate type, the result has a truth value: “7 is even” is either true or false. Perhaps “Bob likes the weather” is true some days and false on others. In fact, this truth value might change by the year (bad weather this year), by the season, by the hour, etc. In English, we expect truth values of sentences to change over time, which is exactly the motivation for this chapter. We’re working toward a logic where truth values change over time.

In a topos \(\mathcal{E}\) = Shv(X, Op), apredicate is a sheaf morphism p: S → Ω where S \(\in\) \(\mathcal{E}\) is a sheaf and Ω \(\in\) \(\mathcal{E}\) is the subobject classifier, the sheaf of truth values. By Definition 7.35 we get a function p(U): S(U) → Ω(U) for any open set U \(\subseteq\) X. In the above example which we will discuss more carefully in Section 7.5—if S is the sheaf of people (people come and go over time), and Bob \(\in\) S(U) is a person existing over a time U, and p is the predicate “likes the weather,” then p(Bob) is the set of times during which Bob likes the weather. So the answer to “Bob likes the weather” is something like “in summers yes, and also in April 2018 and May 2019 yes, but in all other times no.” That’s p(Bob), the temporal truth value obtained by applying the predicate p to the subject Bob.

Exercise 7.62

Just now we described how a predicate p : S → Ω, such as “. . . likes the weather,” acts on sections s \(\in\) S(U), say s = Bob. But by Definition 7.12, any predicate p : S → Ω also defines a subobject of {S | p} \(\subseteq\) S. Describe the sections of this subsheaf. ♦

The poset of subobjects. For a topos \(\mathcal{E}\) = Shv(X, Op) and object (sheaf) S \(\in\) \(\mathcal{E}\), the set of S-predicates |Ω\(^{E}\)| = \(\mathcal{E}\)(S, Ω) is naturally given the structure of a poset, which we denote

(|Ω\(^{S}\)|, ≤\(^{S}\)) (7.63)

Given two predicates p, q : S → Ω, we say that p ≤\(^{S}\) q if the first implies the second. More precisely, for any U \(\in\) Op and section s \(\in\) S(U) we obtain two open subsets p(s) \(\subseteq\) U and q(s) \(\subseteq\) U. We say that p ≤\(^{S}\) q if p(s) \(\subseteq\) q(s) for all U \(\in\) Op and s \(\in\) S(U). We often drop the superscript from ≤\(^{S}\) and simply write ≤. In formal logic notation, one might write p ≤\(^{S}\) q using the ⊢ symbol, e.g. in one of the following ways:

s:S | p(s) ⊢ q(s) or p(s) ⊢\(_{s:S}\) q(s).

In particular, if S = 1 is the terminal object, we denote |Ω\(^{S}\)| by |Ω|, and refer to elements p \(\in\) |Ω| as propositions. They are just morphisms p : 1 → Ω.

This preorder is partially ordered a poset meaning that if p ≤ q and q ≤ p then p = q.

The reason is that for any subsets U, V \(\subseteq\) X, if U \(\subseteq\) V and V \(\subseteq\) U then U = V.

Exercise 7.64

Give an example of a space X, a sheaf S \(\in\) Shv(X), and two predicates p,q: S → Ω for which p(s) ⊢\(_{s:S}\) q(s) holds.

You do not have to be formal. ♦

All of the logical symbols (true, false, \(\land\), \(\lor\), ⇒, ¬) from Section 7.4.2 make sense in any such poset |Ω\(^{S}\)|.

For any two predicates p, q: S → Ω, we define (p \(\land\) q): S → Ω by (p \(\land\) q)(s) := p(s) \(\land\) q(s), and similarly for \(\lor\). Thus one says that these operations are computed pointwise on S.

With these definitions, the \(\land\) symbol is the meet and the \(\lor\) symbol is the join in the sense of Definition 1.81 for the poset |Ω\(^{S}\)|.

With all of the logical structure we’ve defined so far, the poset |Ω\(^{S}\)| of predicates on S forms what’s called a Heyting algebra. We will not define it here, but more information can be found in Section 7.6. We now move on to quantification.

7.4.4 Quantification

Quantification comes in two flavors: universal and existential, or ‘for all’ and ‘there exists.’ Each takes in a predicate of n + 1 variables and returns a predicate of n variables.

Example 7.65

Suppose we have two sheaves S, T \(\in\) Shv(X, Op) and a predicate p : S × T → Ω. Let’s say T represents what’s considered news worthy and S is again the set of people. So for a subset of time U, a section t \(\in\) T(U) is something that’s considered newsworthy throughout the whole of U, and a section s \(\in\) S(U) is a person that lasts throughout the whole of U. Let’s imagine the predicate p as “s is worried about t.” Now recall from Section 7.4.3 that a predicate p does not simply return true or false; given a person s and a news-item t, it returns a truth value corresponding to the subset of times on which p(s, t) is true.

“For all t in T, . . . is worried about t” is itself a predicate on just one variable, S, which we denote

∀(t : T). p(s, t).

Applying this predicate to a person s returns the times when that person is worried about everything in the news. Similarly, “there exists t in T such that s is worried about t” is also a predicate on S, which we denote ∃(t : T). p(s, t). If we apply this predicate to a person s, we get the times when person s is worried about at least one thing in the news.

Exercise 7.66

In the topos Set, where Ω = \(\mathbb{B}\), consider the predicate p : \(\mathbb{N}\) × \(\mathbb{Z}\) → \(\mathbb{B}\) given by

1. What is the set of n \(\in\) \(\mathbb{N}\) for which the predicate ∀(z : \(\mathbb{Z}\)). p(n, z) holds?
2. What is the set of n \(\in\) \(\mathbb{N}\) for which the predicate ∃(z : \(\mathbb{Z}\)). p(n, z) holds?
3. What is the set of z \(\in\) \(\mathbb{Z}\) for which the predicate ∀(n : \(\mathbb{N}\)). p(n, z) holds?
4. What is the set of z \(\in\) \(\mathbb{Z}\) for which the predicate ∃(n : \(\mathbb{N}\)). p(n, z) holds? ♦

So given p, we have a universally- and an existentially-quantified predicate ∀(t : T). p(s, t) and ∃(t : T). p(s, t) on S. How do we formally understand them as sheaf morphisms S → Ω or, equivalently, as subsheaves of S?

Universal quantification. Given a predicate p : S × T → Ω, the universally-quantified predicate ∀(t : T). p(s, t) takes a section s \(\in\) S(U), for any open set U, and returns a certain open set V \(\in\) Ω(U). Namely, it returns the largest open set V \(\subseteq\) U for which p(s|\(_{v}\), t) = V holds for all t \(\in\) T(V).

Exercise 7.67

Suppose s is a person alive throughout the interval U. Apply the above definition to the example p(s, t) = “person s is worried about news t” from Example 7.65. Here, T(V) is the set of items that are in the news throughout the interval V.

1. What open subset of U is ∀(t : T). p(s, t) for a person s?
2. Does it have the semantic meaning you’d expect, given the less formal description in Section 7.4.4? ♦

Abstractly speaking, the universally-quantified predicate corresponds to the subsheaf given by the following pullback:

where p′:S → Ω\(^{T}\) is the currying of S × T → Ω and true\(^{T}\) is the currying of the composite 1 × \(T \stackrel{!}{\rightarrow} A \stackrel{true}{\rightarrow} Ω\).

See Eq. (7.10).

Existential quantification. Given a predicate p : S × T → Ω, the existentially quantified predicate ∃(t : T). p(s, t) takes a section s \(\in\) S(U), for any open set U, and returns a certain open set V \(\in\) Ω(U), namely the union V = \(\bigcup_{i}\)V\(_{i}\) of all the open sets Vi for which there exists some ti \(\in\) T(Vi) satisfying p(s|\(_{Vi}\), t\(_{i}\)) = V\(_{i}\). If the result is U itself, you might be tempted to think “ah, so there exists some t \(\in\) T(U) satisfying p(t),” but that is not necessarily so. There is just a cover of U = \(\bigcup{U_{i}}\) and local sections ti \(\in\) T(U\(_{i}\)), each satisfying p, as explained above. Thus the existential quantifier is doing a lot of work “under the hood,” taking coverings into account without displaying that fact in the notation.

Exercise 7.68

Apply the above definition to the “person s is worried about news t” predicate from Example 7.65.

1. What open set is ∃(t : T). p(s, t) for a person s?
2. Does it have the semantic meaning you’d expect? ♦

Abstractly speaking, the existentially-quantified predicate is given as follows.

Start with the subobject classified by p, namely {(s, t) \(\in\) S × T | p(s, t)} \(\subseteq\) S × T, compose with the projection π\(_{S}\) : S × T → S as on the upper right; then take the epimono factorization of the composite as on the lower left:

Then the bottom map is the desired subsheaf of S.

7.4.5 Modalities

Back in Example 1.123 we discussed modal operators also known as modalities saying they are closure operators on preorders which arise in logic. The preorders we were referring to are the ones discussed in Eq. (7.63): for any object S \(\in\) \(\mathcal{E}\) there is the poset (|Ω\(^{S}\)|,≤\(^{S}\)) of predicates on S, where |Ω\(^{S}\)| = \(\mathcal{E}\)(S,Ω) is just the set of morphisms S → Ω in the category \(\mathcal{E}\).

Definition 7.69

A modality in Shv(X) is a sheaf morphism j : Ω → Ω satisfying three properties for all U \(\subseteq\) X and p, q \(\in\) Ω(U):

(a) p ≤ j(p);

(b) (j ; j)(p) ≤ j(p); and

(c) j(p \(\land\) q) = j(p) \(\land\) j(q).

Exercise 7.70

Suppose j : Ω → Ω is a morphism of sheaves on X, such that p ≤ j(p) holds for all U \(\subseteq\) X and p \(\in\) Ω(U). Show that for all q \(\in\) Ω(U) we have j(j(q)) ≤ j(q) iff j(j(q)) = j(q). ♦

In Example 1.123 we informally said that for any proposition p, e.g. “Bob is in San Diego,” there is a modal operator “assuming p, ....” Now we are in a position to make that formal.

Proposition 7.71

Fix a proposition p \(\in\) |Ω|. Then
(a) the sheaf morphism Ω → Ω given by sending q to p ⇒ q is a modality.
(b) the sheaf morphism Ω → Ω given by sending q to p \(\lor\) q is a modality.
(c) the sheaf morphism Ω → Ω given by sending q to (q ⇒ p) ⇒ p is a modality.

We cannot prove Proposition 7.71 here, but we give references in Section 7.6.

Exercise 7.72

Let S be the sheaf of people as in Section 7.4.3, and let j : Ω → Ω be “assuming Bob is in San Diego...”

1. Name any predicate p : S → Ω, such as “likes the weather.”
2. Choose a time interval U. For an arbitrary person s \(\in\) S(U), what sort of thing is p(s), and what does it mean?
3. What sort of thing is j(p(s)) and what does it mean?
4. Is it true that p(s) ≤ j(p(s))? Explain briefly.
5. Is it true that j(j(p(s))) = j(p(s))? Explain briefly.
6. Choose another predicate q : S → Ω. Is it true that j(p \(\land\) q) = j(p) \(\land\) j(q)? Explain briefly. ♦

7.4.6 Type theories and semantics

We have been talking about the logic of a topos in terms of open sets, but this is actually a conflation of two ideas that are really better left unconflated. The first is logic, or formal language, and the second is semantics, or meaning. The formal language looks like this:

∀(t : T). ∃(s : S). f(s) = t (7.73)

and semantic statements are like “the sheaf morphism f : S → T is an epimorphism.” In the former, logical world, all statements are linguistic expressions formed according to strict rules and all proofs are deductions that also follow strict rules. In the latter, semantic world, statements and proofs are about the sheaves themselves, as mathematical objects. We admit these are rough statements; again, our aim here is only to give a taste, an invitation to further reading.

To provide semantics for a logical system means to provide a compiler that converts each logical statement in the formal language into a mathematical statement about particular sheaves and their relationships. A computer can carry out logical deductions without knowing what any of them “mean” about sheaves. We say that semantics is sound if every formal proof is converted into a true fact about the relevant sheaves.

Every topos can be assigned a formal language, often called its internal language, in which to carry out constructions and formal proofs. This language has a sound semantics a sort of logic-to-sheaf compiler which goes under the name categorical semantics or Kripke-Joyal semantics. We gave the basic ideas in Section 7.4; we give references to the literature in Section 7.6.

Example 7.74

In every topos E, and for every f : S → T in E, the morphism f is an epimorphism if and only if Eq. (7.73) holds. For example, consider the case of database instances on a schema C, say with 100 tables (one of which might be denoted c \(\in\) Ob(C)) and 500 foreign key columns (one of which might be denoted f : c → c′ in C); see Eq. (3.2).

If S and T are two instances and f is a natural transformation between them, then we can ask the question of whether or not Eq. (7.73) holds. This simple formula is compiled by the Kripke-Joyal semantics into asking:

Is it true that for every table c \(\in\) Ob(C) and every row s \(\in\) S(c) there exists a row t \(\in\) T(c) such that f (s) = t?

This is exactly what it means for f to be surjective. Maybe this is not too impressive, but whether one is talking about databases or topological spaces, or complex ideas from algebraic geometry, Eq. (7.73) always compiles into the question of surjectivity. For topological spaces it would say something like:

Is it true that for every open set U \(\subseteq\) X and every section s \(\in\) S(U) of the bundle S, there exists an open covering of (U\(_{i}\) \(\subseteq\) U)\(_{i \in I}\) of U and a section t\(_{i}\) \(\in\) T(U\(_{i}\)) of the bundle T for each i \(\in\) I, such that f (t\(_{i}\)) = s|\(_{U_{i}}\) is the restriction of s to U\(_{i}\)?