Sewon's Wiki

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
====== Sheaf semantics on topological spaces ======


===== 1. Introduction =====

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 in 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.

===== 2. Preliminaries ==== 
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. 

===== 3. Presheaves and sheaves =====

For a topological space $X$, a //**presheaf**// $P$ on $X$ is a contravariant functor $P : \mathcal{O}(X)^{op} \to  \mathbf{Set}$. That means

  - for each open $U \subseteq X$, there is a set $PU$, and
  - for each inclusion of opens $U \subseteq V$, there is a mapping $P(U\subseteq V) : PV \to PU$ satisfying (a) $P(U\subseteq U)$ is the identity map, and (b) $P(U\subseteq W) = P(U\subseteq V) \circ P(V\subseteq W)$ for each $U\subseteq V \subseteq W$.

For any $t \in PV$, we write $t\vert_{U}$ to denote $P(U\subseteq V)(t)$ that conveys the intuitive meaning of presheaves. For each open subset $U$, we attach a set of data $PU$. From a datum $t$ that is defined in $t \in PU$, we can //restrict// the datum $t\vert_V$ locally at $V \subseteq U$. Requirement (b) means that the restrictions are consistent: $(t\vert_{V})\vert_{U} = t\vert_{U}$.

These are some examples of presheaves:
  * A trivial example of presheaf is the //**constant presheaf**// associated with a set $S$ that maps each open to the constant set $S$ where the restrictions are defined by identity.
  * The //**Yoneda embedding**// $\mathbf{y}$ in each open $U$ defines a presheaf such that $\mathbf{y}_UV = \{* \mid V \subseteq U\}$ and $\mathbf{y}_U(V\subseteq T)$ defined uniquely.

For any topological space $X$, collecting presheaves and natural transformations (seeing presheaves as functors) between them forms a category called $\textbf{PSh}(X)$. In other words, a presheaf morphism $\mu : P \to Q$ from a presheaf $P$ to another presheaf $Q$ is a mapping indexed with each open $U\subseteq X$ such that $\mu_U : P U \to Q U$ and $\mu_U(t\vert_U) = \mu_V(t)\vert_U$ for each $U\subseteq V$ and $t \in P V$.

A presheaf is called a //**sheaf**// if it further satisfies:

  3. for each open $U$ and its 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 global defined datum at $U$ when it is localized to the open cover $U_i$, is compatible in the overlaps (intersections). Furthermore, the universal property of the equalizer says that the original global datum is a unique one that can be collated from the local data defined compatibly over the cover.

An important property of a sheaf is that it on the empty set is always a singleton set. For any sheaf $F$ in 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, for the two mappings $p, q : \{*\} \rightrightarrows \{*\}$, their equalizer $e$ must be the unique map from a singleton set $\{*\}.$

Due to the 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 of $S$ (that is, locally constant functions to $S$.) In the next section, 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 cont.}\}$ and $f \vert_V$ be the usual domain restriction. The additional sheaf axiom says that when we have continuous functions defined locally at each open of an open cover, when 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. 

===== 4. Sheafification =====
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 presheave 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 continous} \land p\circ s=id\}$$ for the set of cross-sections. Defining $\Gamma_p(U\subseteq V)$ to be $(s : V \to Y)\vert_U : U \to Y$ the domain restriction, $\Gamma_p$ defines a presheaf on $X$. We can easily verify that $\Gamma_p$ is a sheaf.

Having known that any bundle yields a sheaf, we turn a presheaf $P$ on $X$ into a bundle over $X$. For each point $x \in X$ and its open neighbourhoods $U, V$ 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 \in U\cap V$ and $u\vert_W = v\vert_W$. Note that this binary relation $\sim$ is an equivalence relation and we quotient the set of local data: $$\text{stalk}_x = \{(U,u) \mid x\in U\text{ open and }u \in P(U)\}/_\sim$$
and say //**stalk**// at $x$. In other words, the stalk at $x$ consists of local data that never coincide locally near $x$.

Define the entire space $\Lambda = \sum_x\text{stalk}_x$ and its first projection $p : \Lambda \to X$. We make this $p$ a bundle by giving a suitable topology on $\Lambda$ that makes both $p$ and the //**base section**// map
$$
s_u : U \to \Lambda := x \mapsto \big(x, (U, u) \in \text{stalk}_x\big)
$$
for any $U$ and $u \in PU$ continuous for each $U$ and $u \in PU$ taking $s_u(U)$ to be a basic open. Leaving it as an exercise to prove that this topology works, we conclude that $\Gamma\Lambda_P$ is the //**sheafification**// of $P$ and write $\mathbf{a}P$.

For a set $S$, consider the constant presheaf associated with $S$. We have $(U, u) \sim (V, v)$ iff $u=v$. Hence, $\text{stalk}_x \simeq S$ and $\Lambda \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 base open is $s_u(U) = U\times \{u\}$ which makes the topology on $\Lambda$ have the discrete topology on its second component $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 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 serve as a way to restrict each $u \in PU$ into $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 that (1) $\eta$ is an isomorphism when $P$ was already a sheaf and that (2) for any presheaf $P$ and a sheaf $F$ such that there is a presheaf morphism $\gamma : P \to F$, there is a unique presheaf morphism $u : \mathbf{a}P$ that makes $\gamma = u\circ \eta$. In other words, in some sense, $\mathbf{a}P$ is the most 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}$$
is the left adjoint to the inclusion functor.


===== 5. Topos of sheaves =====
The category $\mathbf{Sh}(X)$ is a topos meaning that it
  - has all finite limits,
  - is cartesian closed, and 
  - has a subobject classifier $\Omega$.
The small limits in $\mathbf{Sh}(X)$ are those of $\mathbf{PSh}(X)$ which are the limits in $\mathbf{Set}(X)$ constructed pointwise in each open $U$. For example, a terminal sheaf $1$ is a sheaf that assigns a singleton set to each open. For two sheaves $F$ and $G$, the product is the sheave that assigns $FU \times GU$ for each open $U$.

For two sheaves $F$ and $G$, the exponent $G^F$ is a sheaf where
$$G^FU = \mathbf{Set}^{\mathcal{O}^{op}}(\mathbf{y}_U\times F, G)$$ that for each $U$ attaches the set of natural transformations $\mu$ such that for each $V \subseteq U$, $\mu_V : FV \to GV$. 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$ when $G$ is a sheaf, the mono becomes a sheaf mono if and only if for any open $U$ and $u \in GU$, and an open covering $\{U_i\}_{i\in I}$, 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 naturally 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 it 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 truths as the number of 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 topos 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 characteristic 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 by the characteristic sheaf morphism which we can easily check 
$$
\land_U : \Omega U\times \Omega U \ni (V_1, V_2) \mapsto V_1 \cap V_2 \in \Omega U.
$$
Not so similarly, but the topos disjunction in sheaves 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 connectivity is the negation:
$$\neg_U : \Omega U \ni V \mapsto \bigcup\{W\in \Omega U\mid W\cap U = \emptyset\}\in \Omega U.$$
Namely, $\neg_U$ maps $V$ to its largest open set in $U$ in the complement of $V$. Therefore, $\neg\neg_UV = V$ will not hold in general. More interestingly, for $V\cup_U\neg_U V \neq \text{true}_U$ in general.

Leaving verifying other requirements as an exercise, we put a remark here that a topos of sheaves has all small limits not restricted to finite ones. 

===== 6. The Mitchell-Bénabou language ===== 

is an internal language (type theory) of a topos where each type denotes an object and a term denotes a general point of the corresponding object of the type of the term. For example, each variable $x$ of type $\tau$ denotes the identity morphism $x : \tau \to \tau$. Without distinguishing types and formulae, terms of type $\Omega$ are called formulae. Logical operations are defined using the standard operations on truth values. For example, when $\phi : A \to \Omega$ and $\phi : B \to \Omega$ are formulae, the conjunction is defined as $\phi \land \psi : (A\times B) \to \Omega$ by post-composing $\land : \Omega\times\Omega \to \Omega$ on $\langle \phi, \psi\rangle : (A\times B) \to \Omega \times \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\}.
$$

===== 7. Sheaf semantics and forcing =====

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 a $\mathbf{Sh}(X)$. For a topos of sheaves, Kripke-Joyal semantics takes a more explicit form, which is called the 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)$, hence is a sheaf morphism $\phi : F \to \Omega$. For a open $U$ and $u \in FU$, the relation of $U$ //**forcing**// $\phi(u)$ is defined recursively as: 
  * $U \Vdash \phi(u) \land \psi(u)$ iff $U \Vdash \phi(u)$ and $U \Vdash \psi(u)$
  * $U \Vdash \phi(u) \lor \psi(u)$ iff there is an open covering $\{U_i\}_{i\in I}$ of $U$ such that for each $i$, $U_i \Vdash \phi(u\vert_{U_i})$ or $U_i \Vdash \psi(u\vert_{U_i})$
  * $U \Vdash \phi(u) \Rightarrow \psi(u)$ iff for all $V \subseteq U$, $V \Vdash \phi(u\vert_V)$ implies $V\Vdash\psi(u\vert_V)$
  * $U \Vdash \neg\phi(u)$ iff for all $V\subseteq U$, $V\Vdash \phi(u\vert_V)$ implies $V$ is empty

When $\phi(x,y)$ is a formula with free variables $x$ of type $F$ and $y$ of type $G$, for all $u \in FU$, 
  * $U\Vdash \exists y \phi(u, y)$ iff there is an open covering $\{U_i\}_{i\in I}$ of $U$ and $v_i \in  G U_i$ such that $U_i \Vdash \phi(u\vert_{U_i}, v_i)$ for each $i \in I$
  * $U \Vdash \forall y\phi(u, y)$ iff for all $V\subseteq U$ and $v \in GV$, $V \Vdash \phi(u\vert_V, v)$

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$ or $\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 subset $V \subseteq U$ and $W \in \Omega V$ it holds that $V \Vdash \phi(W) \lor \neg \phi(W)$; which 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, **LEM** at $U$ is completely determined by the lattice structure of the opens of $U$ if it is **Boolean**. 

As a consequence, **LEM** is invalidated at a unit interval $(0,1)$ but is valid at (and only at) a locally indiscrete topology.
===== 8. Real numbers in a topos of sheaves =====
Any topos of sheaves $\mathbf{Sh}(X)$ have 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 sheave 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 to define the set 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 for a pair of terms $\langle D_L, D_U \rangle$ of type $\Omega^{\mathbf{Q}} \times \Omega^{\mathbf{Q}}$ to be a Dedekind cut. It means we can define a sub-object, a 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 D_L, D_U\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}$, the forcing $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\}$. A continuous function $f : \{0,1\} \to \mathbb{R}$ is essentially $(f(0),f(1)) \in \mathbb{R}^2$. Hence, we can choose the open cover $(\{0\}, \{1\})$ for any $f$, and choose if $f(0) \leq 0$ or $f(0) \geq 0$, and if $f(1) \leq 0$ or $f(1) \geq 0$. Hence, 
$$
\{0,1\} \Vdash \forall x : \mathbf{R}.\;x \leq 0 \lor x \geq 0.
$$


{{tag>[completed]}}