In this short note, I provide a tutorial on sheaf semantics, aiming to invalidate the dichotomy of real numbers on the unit interval $(0,1)$: $$(0,1)\not\Vdash \forall x : \mathbf{R}.\;x \leq 0 \lor x \geq 0$$ while validating it on the discrete topology of the booleans $\{0, 1\}$: $$\{0,1\}\Vdash \forall x : \mathbf{R}.\;x \leq 0 \lor x \geq 0.$$ As a general statement, we show that the law of excluded middle (LEM) holds on a topological space if and only if the space is locally indiscrete.
But what does it mean for a mathematical principle to hold or fail on a topological space, such as an interval or the booleans? This note answers this question by introducing the concept of topoi of sheaves on topological spaces. Sheaf semantics in these topoi then allows us to interpret mathematical statements on topological spaces.
I have tried to explain everything starting from the basics of sheaves over topological spaces, rather than using Grothendieck topologies. I hope this note helps those who feel somewhat overwhelmed by the abstract mathematics typically encountered in presentations of the general theory of Grothendieck topoi.
This note is essentially an excerpt and a rephrasing of “Sheaves in Geometry and Logic” by Saunders Mac Lane and Ieke Moerdijk. It does not include many interesting results or proofs. Readers interested in this topic are strongly encouraged to refer to the book.
I assume that the readers are familiar with the basic concepts of category theory and topology. If any reader feels that this note demands more than that, please complain to the author so that this note can be improved.
For each topological space $X$, we write $\mathcal{O}(X)$ to denote the category of opens: the objects are the open sets of $X$ and $U \to V$ if and only if $U \subseteq V$. Between two objects, there is at most one morphism.
For a topological space $X$, a presheaf $P$ on $X$ is a functor $P : \mathcal{O}(X)^{op} \to \mathbf{Set}$. That means
For any $t \in PV$, we write $t\vert_{U}$ to denote $P(U\subseteq V)(t)$. This notation conveys the intuitive meaning of presheaves. For each open subset $U$, we attach a set of data $PU$. From a datum $t \in PV$, we can restrict the datum locally to $U \subseteq V$ and obtain $t\vert_U$. Requirement (b) means that the restrictions are consistent: $(t\vert_{V})\vert_{U} = t\vert_{U}$ for $t \in PW$.
These are some examples of presheaves:
For any topological space $X$, presheaves and natural transformations between them (seeing presheaves as functors) form a category called $\mathbf{PSh}(X)$. In other words, a presheaf morphism $\mu : P \to Q$ is a family of maps $\mu_U : P U \to Q U$ indexed by the opens $U\subseteq X$ such that $\mu_U(t\vert_U) = \mu_V(t)\vert_U$ for each $U\subseteq V$ and $t \in P V$.
A presheaf $P$ is called a sheaf if, for each open $U$ and each open covering $U = \bigcup_{i \in I}U_i$, the restriction map $e : PU \to \prod_iPU_i$ defined by $e(t) = (t\vert_{U_i})_i$ is an equalizer
$$ PU \overset{e}{\dashrightarrow} \prod_iPU_i \overset{p}{\underset{q}{\rightrightarrows}} \prod_{j,k}P(U_j\cap U_k)$$
where $p((t_i)_i) =(t_j\vert_{U_j\cap U_k})_{j,k}$ and $q((t_i)_i) =(t_k\vert_{U_j\cap U_k})_{j,k}$.
The requirement says that a datum defined at $U$, when localized to the opens $U_i$ of the cover, is compatible on the overlaps (intersections). Furthermore, the universal property of the equalizer says that any family of local data that is compatible on the overlaps collates to a unique datum at $U$.
An important property of a sheaf $F$ is that $F\emptyset$ is always a singleton set. For any sheaf $F$ on a topological space $X$, considering the empty set that is trivially open, we can choose its empty covering $I = \emptyset$. Since the empty product is a singleton set, the two mappings $p, q : \{*\} \rightrightarrows \{*\}$ are equal, so their equalizer $e : F\emptyset \to \{*\}$ must be a bijection.
Due to this property, constant presheaves in general fail to be sheaves. In fact, we need a more clever way to construct trivial sheaves from sets. For each set $S$, the constant sheaf associated with $S$ is a sheaf $\Delta(S)$ that for each open $U$ assigns the set of continuous functions from $U$ to the discrete space $S$ (that is, locally constant functions to $S$). In the next section, we show that this modification to make a sheaf is not ad hoc but is indeed optimal and universal.
Another very important sheaf is that of continuous real functions. For each open $U$, define $\mathbf{C}_\mathbb{R}U = \{f : U \to \mathbb{R} \mid f\text{ is continuous}\}$ and let $f \vert_V$ be the usual domain restriction. The additional sheaf axiom says that when we have continuous functions defined locally on the opens of an open cover and they agree on the intersections, we can glue them together to obtain one global real function. Hopefully, this example explains enough of the meaning of the additional requirement.
By definition, every sheaf is a presheaf, meaning that there is a trivial inclusion functor $$\mathbf{Sh}(X) \hookrightarrow \mathbf{PSh}(X).$$ Here, $\mathbf{Sh}(X)$ denotes the category of sheaves on $X$ with presheaf morphisms. What about the other direction? Above, we have noticed that not all presheaves are sheaves. However, there is no reason to be disappointed because there is a canonical way to make a presheaf into a sheaf, namely sheafification.
A bundle over a topological space $X$ is a continuous mapping $p : Y \to X$, where for each $x \in X$, the set $p^{-1}(\{x\})$ can be seen as the fiber at $x$. For a bundle $p : Y \to X$ and an open subset $U \subseteq X$, write $$\Gamma_p U = \{s : U \to Y \mid s \text{ is continuous} \land p\circ s=id\}$$ for the set of cross-sections. Defining $\Gamma_p(U\subseteq V)$ to be the domain restriction $s \mapsto s\vert_U$, $\Gamma_p$ defines a presheaf on $X$. We can easily verify that $\Gamma_p$ is a sheaf.
Knowing that any bundle yields a sheaf, we turn a presheaf $P$ on $X$ into a bundle over $X$. For each point $x \in X$, open neighbourhoods $U, V$ of $x$ and local data $u \in P(U), v \in P(V)$, define $(U, u) \sim (V,v)$ by the existence of an open neighbourhood $W$ of $x$ such that $W \subseteq U\cap V$ and $u\vert_W = v\vert_W$. Note that this binary relation $\sim$ is an equivalence relation, and we call the quotient of the set of local data $$\text{stalk}_x = \{(U,u) \mid x\in U\text{ open and }u \in P(U)\}/_\sim$$ the stalk at $x$. In other words, the stalk at $x$ consists of local data near $x$, where two data are identified when they coincide on some neighbourhood of $x$.
Define the total space $\Lambda_P = \sum_x\text{stalk}_x$ and its first projection $p : \Lambda_P \to X$. For each open $U$ and $u \in PU$, define the base section $$ s_u : U \to \Lambda_P := x \mapsto \big(x, (U, u) \in \text{stalk}_x\big). $$ We make $p$ a bundle by giving $\Lambda_P$ a suitable topology that makes both $p$ and every base section $s_u$ continuous, taking each $s_u(U)$ to be a basic open. Leaving it as an exercise to prove that this topology works, we call $\Gamma_p$ the sheafification of $P$ and write $\mathbf{a}P$.
For a set $S$, consider the constant presheaf $P$ associated with $S$. We have $(U, u) \sim (V, v)$ iff $u=v$. Hence, $\text{stalk}_x \simeq S$ and $\Lambda_P \simeq X\times S$. For each open $U$ and $u \in S = P(U)$, the base section is $$s_u : x \mapsto (x, u)$$ for any $x \in U$. Hence, the basic open is $s_u(U) = U\times \{u\}$, which makes $\Lambda_P$ the product of $X$ and the discrete space $S$. Therefore, any cross-section $s : U \to X \times S$ is essentially a continuous function from $U$ to $S$ with the discrete topology (aka a locally constant function). In other words, the sheafification of the constant presheaf is the constant sheaf.
There are some more things to say about sheafification. For a presheaf $P$ and its sheafification $\mathbf{a}P$, the base sections send each $u \in PU$ to $s_u \in \mathbf{a}PU$. In fact, in the category of presheaves, $$\eta : P \to \mathbf{a}P$$ is a natural transformation where $\eta_U : u \mapsto s_u$. The sanity check of the sheafification follows from the facts that (1) $\eta$ is an isomorphism when $P$ is already a sheaf and that (2) for any presheaf $P$, any sheaf $F$ and any presheaf morphism $\gamma : P \to F$, there is a unique presheaf morphism $\bar{\gamma} : \mathbf{a}P \to F$ that makes $\gamma = \bar{\gamma}\circ \eta$. In other words, $\mathbf{a}P$ is the optimal sheaf that embodies $P$. We leave it as an exercise to verify that this sheafification as a functor $$\mathbf{a} : \mathbf{PSh}(X) \to \mathbf{Sh}(X)$$ is the left adjoint to the inclusion functor.
The category $\mathbf{Sh}(X)$ is a topos, meaning that it
The small limits in $\mathbf{Sh}(X)$ are those of $\mathbf{PSh}(X)$, which are constructed pointwise in $\mathbf{Set}$ at each open $U$. For example, the terminal sheaf $1$ is the sheaf that assigns a singleton set to each open. For two sheaves $F$ and $G$, the product is the sheaf that assigns $FU \times GU$ to each open $U$.
For two sheaves $F$ and $G$, the exponent $G^F$ is a sheaf where $$G^FU = \mathbf{Set}^{\mathcal{O}(X)^{op}}(\mathbf{y}_U\times F, G),$$ that is, $G^F$ attaches to each $U$ the set of natural transformations $\mu$ with components $\mu_V : FV \to GV$ for $V \subseteq U$. The restriction is defined naturally. Of course, proving that this presheaf indeed is a sheaf and further is an exponent is not trivial.
A sheaf morphism $\mu : F \to G$ is a mono if and only if $\mu_U : FU \to G U$ is injective for all open $U$. (However, the statement fails for epi and surjectivity.) There is more to say about the subsheaves. For a presheaf mono $\mu : F \rightarrowtail G$ where $G$ is a sheaf, $F$ is a sheaf if and only if, for any open $U$, $u \in GU$ and open covering $\{U_i\}_{i\in I}$ of $U$, the locality condition holds: $$ u \in \mu_U(FU) \quad \text{iff} \quad u\vert_{U_i} \in \mu_{U_i}(FU_i)\text{ for all }i\in I. $$
The subobject classifier $\Omega$ is a sheaf that maps each $U$ to the set of opens included in $U$, whose restriction is defined by $S\vert_U = S\cap U$. The true morphism $\text{true} : 1\to \Omega$ selects the maximum opens $\text{true}_U(*) = U\in\Omega U$. As can be easily seen and could be guessed, $\mathbf{Sh}(X)$ is a topos where the number of truth values can be more than just 2. Roughly speaking, at each local universe $U$, there are as many truth values as open subsets of $U$.
Given a sheaf mono $m : M \rightarrowtail F$, the corresponding characteristic sheaf morphism is then $\chi : F \to \Omega$ such that $$\chi_U : (u \in FU) \mapsto \bigcup_{u\vert_V \in m_V(MV)}V \in \Omega U.$$ Since the pullback of the corresponding diagram $$ \begin{array}{ccc} M & \rightarrowtail & F \\ {}^!\downarrow & & \downarrow{}^{\chi} \\ 1 & \xrightarrow{\text{true}} & \Omega \end{array} $$ is also constructed pointwise, we can check that at $U$, the set-theoretic pullback $$\{(u, *) \in FU \times\{*\}\mid \bigcup_{u\vert_V \in m_V(MV)}V = U\}$$ is (isomorphic to) $MU$ due to the aforementioned locality condition of sheaf monos.
Now, we define the logical operators. Since any $1 \to F$ is mono, consider the mono $$\langle \text{true}, \text{true}\rangle : 1 \rightarrowtail \Omega \times \Omega.$$ The conjunction $\land : \Omega \times \Omega \to \Omega$ is defined as its characteristic sheaf morphism, which we can easily check to be $$ \land_U : \Omega U\times \Omega U \ni (V_1, V_2) \mapsto V_1 \cap V_2 \in \Omega U. $$ The disjunction is defined less directly, but in sheaves it becomes $$\lor_U : \Omega U\times \Omega U \ni (V_1, V_2) \mapsto V_1 \cup V_2 \in \Omega U$$ as one could easily guess. A difference from the classical connectives is the negation: $$\neg_U : \Omega U \ni V \mapsto \bigcup\{W\in \Omega U\mid W\cap V = \emptyset\}\in \Omega U.$$ Namely, $\neg_U$ maps $V$ to the largest open subset of $U$ disjoint from $V$. Therefore, $\neg_U\neg_UV = V$ will not hold in general. More interestingly, $V\cup\neg_U V \neq \text{true}_U$ in general.
We leave verifying the other requirements as an exercise.
The Mitchell–Bénabou language is an internal language (type theory) of a topos, where each type denotes an object and each term denotes a generalized element of the object denoted by its type. For example, each variable $x$ of type $\tau$ denotes the identity morphism $x : \tau \to \tau$. Terms of type $\Omega$ are called formulae, so formulae are not a separate syntactic class. Logical operations are defined using the standard operations on truth values. For example, when $\phi : A \to \Omega$ and $\psi : B \to \Omega$ are formulae, the conjunction $\phi \land \psi : A\times B \to \Omega$ is defined by composing $\phi\times\psi : A\times B \to \Omega \times \Omega$ with $\land : \Omega\times\Omega \to \Omega$. The quantifiers are defined in a more sophisticated way using internal adjoints, which we will not deal with here.
An equality of two terms $f, g$ of type $\tau$ is defined by $\delta_\tau \circ \langle f, g\rangle$ where $\delta_\tau$ is the characteristic morphism of $\langle id_\tau, id_\tau \rangle : \tau \to \tau\times \tau$. For a category of sheaves, the characteristic map $\delta_F$ becomes $$ (\delta_F)_U : FU \times FU \ni (v_1, v_2) \mapsto \bigcup \{V \subseteq U \mid v_1\vert_V = v_2\vert_V\}. $$
There is Kripke–Joyal semantics for the Mitchell–Bénabou language in a topos. However, we do not deal with it for an arbitrary topos but only for $\mathbf{Sh}(X)$. For a topos of sheaves, Kripke–Joyal semantics takes a more explicit form called sheaf semantics, which resembles more the original semantics of S. A. Kripke.
For a topological space $X$, consider a formula $\phi(x)$ with a free variable $x$ of type (sheaf) $F$ in the Mitchell–Bénabou language of $\mathbf{Sh}(X)$, which is hence a sheaf morphism $\phi : F \to \Omega$. For an open $U$ and $u \in FU$, the relation of $U$ forcing $\phi(u)$ is defined recursively as:
When $\phi(x,y)$ is a formula with free variables $x$ of type $F$ and $y$ of type $G$, for all $u \in FU$,
Then, the soundness theorem states $$U\Vdash \phi(u) \quad\text{iff}\quad u \in \{x \mid \phi(x) \}U.$$
Let us make a comment on the disjunction. For an open $U$ to force a disjunction $\phi \lor \psi$, it is not that either $\phi$ or $\psi$ should be chosen for the entire $U$. We only need to find one open covering where for each open, we can choose differently either $\phi$ or $\psi$.
Consider the formula $\phi \lor \neg \phi : \Omega \to \Omega$ where $\phi : \Omega\to\Omega$ is a propositional, $\Omega$-typed variable, in the language of $\mathbf{Sh}(X)$. For an open $U \subseteq X$, $U$ forces the law of excluded middle (LEM) $$ U \Vdash \forall \phi.\; \phi \lor \neg \phi $$ if and only if for all open subsets $V \subseteq U$ and $W \in \Omega V$, it holds that $V \Vdash \phi(W) \lor \neg \phi(W)$. This holds if and only if there is an open covering $\{V_i\}_{i\in I}$ of $V$ such that $$ V_i \Vdash \phi(W\cap V_i)\quad \text{or} \quad V_i \Vdash \neg\phi(W\cap V_i). $$ Applying the soundness theorem, we get it equivalent to $$ V_i \subseteq W \quad \text{or} \quad V_i \subseteq W^c. $$ We can conclude that LEM is forced by an open $U$ if and only if for any open $V \subseteq U$, its complement in $U$ is open. In other words, $U$ forces LEM if and only if the lattice of opens of $U$ is Boolean.
As a consequence, LEM is invalidated at the unit interval $(0,1)$ but is valid at (and only at) a locally indiscrete topology, that is, a topology in which every open set is closed.
Any topos of sheaves $\mathbf{Sh}(X)$ has natural number, integer and rational objects that are constant sheaves associated with sets of natural numbers $\mathbb{N}$, integers $\mathbb{Z}$, and rational numbers $\mathbb{Q}$. Hence, a naïve guess for the sheaf of real numbers would be the constant sheaf associated with the set of real numbers $\mathbb{R}$, which then would have made this note boring.
An obvious choice for the sheaf of real numbers is the object of Dedekind cuts. Since we have a rational number object $\mathbf{Q} = \Delta(\mathbb{Q})$, we can use the Mitchell–Bénabou language to write the predicate saying that a pair of terms $\langle D_L, D_U \rangle$ of type $\Omega^{\mathbf{Q}} \times \Omega^{\mathbf{Q}}$ is a Dedekind cut. It means we can define the subsheaf of $\Omega^{\mathbf{Q}} \times \Omega^{\mathbf{Q}}$ of real numbers by simply writing $$\mathbf{R} = \{\langle D_L, D_U \rangle \in \Omega^{\mathbf{Q}} \times \Omega^{\mathbf{Q}} \mid \langle D_L, D_U \rangle\text{ is a Dedekind cut} \}.$$ Skipping all the important calculations and discussions, we can conclude that $$\mathbf{R} \simeq \mathbf{C}_{\mathbb{R}}\;!$$ In other words, in any category of sheaves, the sheaf of Dedekind real numbers is the sheaf of continuous real functions.
Now, let us consider the dichotomy of real numbers. Assume the unit interval forces it: $$ (0,1) \Vdash \forall x : \mathbf{R}.\;x \leq 0 \lor x \geq 0 $$ meaning that for any open subset $U$ of the unit interval and any continuous real function $f : U \to \mathbb{R}$, we have $U \Vdash f \leq 0 \lor f \geq 0$. Choose $U = (0,1)$ and $f(x) = x - 0.5$. Then the forcing semantics for disjunction implies that there is an open covering $\{U_i\}_{i\in I}$ of the unit interval such that for each $i\in I$, $$ U_i \Vdash f\vert_{U_i} \leq 0 \quad \text{or} \quad U_i \Vdash f\vert_{U_i} \geq 0 $$ meaning that $$ f(x) \leq 0 \text{ for all }x \in U_i\quad \text{or} \quad f(x) \geq 0 \text{ for all }x \in U_i. $$ However, this cannot be true for $U_i$ containing $0.5$. Hence, $$ (0,1) \not\Vdash \forall x : \mathbf{R}.\;x \leq 0 \lor x \geq 0. $$
We instead consider the discrete topology on $\{0,1\}$. For any open $V \subseteq \{0,1\}$, a continuous function $f : V \to \mathbb{R}$ is essentially a family of reals $(f(a))_{a \in V}$. Hence, for any $f$, we can choose the open cover of $V$ by its singletons $\{a\}$, and on each $\{a\}$ choose whether $f(a) \leq 0$ or $f(a) \geq 0$. Hence, $$ \{0,1\} \Vdash \forall x : \mathbf{R}.\;x \leq 0 \lor x \geq 0. $$