An example of a forcing argument in geometry - down-to-earth uses of topos theory

Topos theory leads with the slogan - ``unification of logic and geometry.'' This theory has been more effective in marketing than in actually giving effective cross-fertilization between the two fields. A subject in between $A$ and $B$ may draw on both fruitfully and give back to both fruitfully, but it is most exciting when it really serves as a bridge between $A$ and $B$, allowing you to transfer ideas back and forth.

The notion of ``Kripke model'' is one of the oldest proposed semantics for forcing. Some category theorists have noticed that a Kripke model (let's say a model of a first order theory) over an index set $I$ with partial-ordering relation $\leq$ can be viewed as a functor from $I$ as a poset category into the category of sets, or a presheaf depending on your orientation of $I$. This observation has led to a development of a general forcing semantics in an elementary topos; a good reference is Sheaves in Geometry and Logic by Mac Lane and Moerdijk, in particular the chapter on ``Topoi and Logic'', which dedicates a section to sheaf semantics. This has been influential among category theorists who are also interested in set theory.

In short, there is a natural forcing logic associated to any sheaf; and many arguments in the sheaf can be formalized into the forcing logic. Sheaves have come to engulf huge parts of modern geometry, and I am always on the hunt for examples of forcing being used fruitfully in geometry, or a geometric perspective to illuminate forcing arguments in set theory.

Andrei Sipos has put together here: ( https://cs.unibuc.ro/~asipos/sheaves.pdf ) a very good introduction to the internal forcing logic of sheaves, including a beautiful example. A family of first-order structures $\left\{ M_i \right\}_{i\in I}$ of a given language $\mathcal{L}$ can be regarded as a a sheaf $\mathcal{M}$ of structures in a fairly trivial sense: we regard $I$ as a discrete topological space, whose opens are all subsets of $I$; if $A\subset I$, the set of sections of our sheaf over $A$ is defined to be $\prod_{i\in A}M_i$. The restriction maps are simply the projections; that it forms a sheaf is fairly obvious.

Now, the set of all ultrafilters on the powerset of $I$, which I denote $\beta I$, is often endowed with a standard choice of topology. Equipped with this topology, it is the Stone-Cech compactification of the discrete space $I$. There is then a natural continuous embedding $\eta : I\to \beta I$. There is now a direct image functor $\eta_{\ast} : \mathbf{Shv}(I)\to \mathbf{Shv}(\beta I)$; I apply the direct image functor $\eta_{\ast}$ to the sheaf $\mathcal{M}$ of structures to extend the domain of the sheaf of structures over $\beta I$.

When I embed $I$ into $\beta I$, I think of adjoining generic points to $I$, just as in algebraic geometry, one adjoins prime ideals as points to the space, each of which lies somewhere on the variety associated to it, but nowhere in particular. The parallel is quite literal, as a ``generic point'' on a scheme can be identified with a completely prime filter on the lattice of open subsets of the scheme, whereas a point in $\beta I$ can be identified with a prime filter on the lattice of opens of $I$.  The motivation of adjoining these generic points is a bit subtle to me, but at the very least we can point out that: (1.) there are natural examples of filtered colimits which look like the formation of stalk at an imaginary point that seems to want to be there, such as the construction of the field of rational functions over an irreducible variety, and (2.) such a choice is a technical necessity for developing scheme theory over arbitrary commutative rings.

(If you have better intuition for why we want to ``flesh out'' our space by passing to the soberification, I'd love to hear it; it seems to have something to do with the fact that a sober space can be functorially reconstructed from its lattice of opens and so they are the ideal spaces for sheaf theory. This way you have a nice precise theorem which roughly reads that every filtered colimit in the lattice of opens which seems like it might be the set of all opens containing a point, is actually indeed the stalk at a point. But how is this useful?)

As I have just pointed out, the reason I adjoin new generic points to my space (and expand the domain of this sheaf so that it includes the new points, using the direct image functor) is exactly so that I can localize my structure sheaf at a point which lies ``somewhere'' in $I$, but nowhere in particular, and thus has all the properties which hold ``almost everywhere on $I$'' (on certain large open sets). And when I localize the direct image sheaf at a nonprincipal ultrafilter, I recover exactly the ultraproduct of the family of structures at the ultrafilter; the ultraproduct is exactly the stalk of the sheaf at the generic point.

Sipos (using the work of Ellerman and others) goes on to show how we can derive Los's theorem using the internal forcing logic of the sheaf, which is an absolutely beautiful idea. This shows that there is a general Los's theorem for sheaves of models rather than families of models. Go check it out!

Let me return to the main subject of this blog post. I want to give an example of forcing being used fruitfully in geometry. The point I want to make is about lower semicontinuity. The basic theorems about lower semicontinuous functions (or upper semicontinuous) have proofs which strike me as obviously as being a forcing argument in the sheaf.

I would like to equip the set of natural numbers with an unusual topology. I will use $\mathbb{N}$ to denote the set of natural numbers with the usual (discrete) topology; and I will use $\mathbf{N}$ to denote the set of natural numbers with the topology where upper sets are open.

Let $X$ be a topological space. A continuous function $f : X\to \mathbf{N}$ is said to be lower semicontinuous. In other words, for each $x\in X$; $x$ lives in an open neighborhood $U$ such that $f(x')\geq f(x)$ for all $x\in U$. So the value of the function only falls at certain closed sets; and points not in these ``critical regions'' where the value of the function drops can be isolated away from them by an open set.

Example: Suppose that $X, Y$ are smooth $C^{\infty}$ manifolds, and $F : X\to Y$ is a smooth map. Then let $f : X\to \mathbf{N}$ assign each point $x$ the rank of the differential $d_xF$, or equivalently, choosing a coordinate system, the rank of the Jacobian determinant.

Example: Suppose that $X$ is an algebraic variety, and let $M :X \to \mathbb{A}^{n^2}$ be a map of varieties which assigns to each point in $x$ an $n\times n$ matrix $M_x$, so that we can regard $M$ as a family of $n^2$ regular functions $\left\{ g_i \right\}$ from $X$ into our underlying field, which serve as the entries of $M$. Then the rank of the matrix $M_x$ is at least $k$ at $x$ if and only if one of the $k\times k$ minors of $M_x$ has nonvanishing determinant; which is the union of of open subsets of $X$ whose complements are carved out by the vanishing of regular functions on $X$ (the determinants of the entries).

The purpose of this blog post is to state and prove the following theorem by translating it into the intuitionistic higher order logic which is the internal logic of topos theory, and then proving it in that internal logic.

Theorem: Let $X$ be a topological space, and let $\rho: X\to \mathbf{N}$ be a lower semicontinuous function. Suppose there is an open covering $\left\{ U_i \right\}_{i\in I}$ of $X$ so that on each open set, $\rho\mid_{U_i}$ is bounded above by some $n_i$. Then
 
\begin{equation}
\label{eq:1}
\left\{ x\in X \mid \rho \textrm{ is constant on a neighborhood of } x \right\}
\end{equation}
is open and dense in $X$.

Let $\alpha : \mathbb{N}\to \mathbf{N}$ be the map which is the identity at the set theoretic level. $\alpha$ is bijective, and continuous, but not bicontinuous.

I am interested in the sheaves (over $X$) of continuous functions from $X$ into $\mathbb{N}$ and $\mathbf{N}$; I will also denote these by $\mathbb{N}$ and $\mathbf{N}$. Hopefully it is clear from context what is meant. $\alpha$ determines a natural transformation from $\mathbb{N}\to \mathbf{N}$.

We have now entered into topos land - specifically the topos $\operatorname{Shv}(X)$. I can think of $\mathbb{N}, \mathbf{N}$ as types in a certain higher order many-sorted intuitionistic logic, and think of $\alpha$ as a term; the sheaves are their semantics, the objects they denote.

$\mathbb{N}$ is the natural numbers object (NNO) in the category of sheaves, and is very richly structured. It carries the usual induction principle. So far, other than the basic operators of arithmetic $0,1,+,\times, \dots$, we have only the constant term $\rho : \mathbf{N}$. Every term in our language is a term over a certain context; for example, $\alpha$ is a term over the context $\mathbb{N}$, and we should write

\begin{equation}
\label{eq:2}
n : \mathbb{N} \vdash \alpha(n):\mathbf{N}
\end{equation}

Since $\rho$ is a global section, however, it can be regarded as a morphism from the terminal object in $\operatorname{Shv}(X)$, $\mathbf{1}$, which is assumed inhabited by a unique inhabitant by default. It is common to therefore regard $\rho$ as a term over the empty context, and simply write

\begin{equation}
\label{eq:3}
\vdash \rho: \mathbf{N}
\end{equation}
We can form basic predicates in the logic, such as
\begin{equation}
\label{eq:4}
n: \mathbb{N} \vdash \alpha(n)\leq \rho : \mathbf{Prop}
\end{equation}
By applying the comprehension principle to this predicate, we define a subobject/subtype/subsheaf of $\mathbb{N}$, which I'll call $\mathcal{P}$; $\mathcal{P}\subset \mathbb{N}$ and $n\in\mathcal{P} \iff \alpha(n)\leq \rho$.

The hypothesis that ``there exists an open covering $\left\{ U_i \right\}_{i\in I}$ such that $\rho\mid_{U_i}$ is bounded above by some $n_i$'' can be simply translated as
\begin{equation}
\label{eq:5}
\vdash  \exists n: \mathbb{N}. \rho < \alpha(n)
\end{equation}
The fact that we don't reference many different $n$'s in this sentence, referring to different open sets of the cover, is one of the elegant features in topos logic: truth, like everything else about sheaves, is local, and a sentence is true iff it's true locally.

On the other hand, the predicate that $\rho$ is locally constant can be translated into the topos language as $\exists n: \mathbb{N}. \alpha(n)=\rho$. We want this to hold true on an open dense set. Because this sentence in the formal language has no free variables, its context is the terminal object, $\mathbf{1}$, and so its interpretation will determine a subobject of $\mathbf{1}$; these subobjects are exactly the open sets. We can point out that it suffices to prove
\begin{equation}
\label{eq:6}
\vdash \lnot\lnot \exists n :\mathbb{N}.\rho =\alpha(n)
\end{equation}
because this will be valid on the whole space $X$ iff $\exists n :\mathbb{N}\rho=\alpha(n)$ is true on an open dense set. This is the topological import of the Godel double-negative translation of classical logic into intuitionistic logic.

So I will prove \ref{eq:6}, as much as possible relying only on straightforward intuitionistic logic, but it cannot be ``purely'' in this setting - occasionally I will have to introduce new sentences that I need for the argument which are easily proven by direct inspection of $\mathbb{N},\mathbf{N}$ and $\alpha$.

We have to prove \ref{eq:6} by contradiction, of course, so suppose that
\begin{equation}
\lnot \exists
n:\mathbb{N}. \rho=\alpha(n)\label{eq:7}
\end{equation}
That is, we want to prove that the maximal open subset $U$ on which the predicate $\lnot \exists n:\mathbb{N}.\alpha(n)=\rho$ is the empty set. To give some geometric intuition, our assumption means that, fixing any open subset $V$, the sheaf associated to thesentence $\exists n:\mathbb{N}.\alpha(n)=\rho$ doesn't admit a section over any open subset $V'\subset V$; there's no open set $V'$ where $\rho$ is equal to any constant $n$.

Because in intuitionistic logic the transformation $\lnot\exists \to \forall\lnot$ is acceptable, we have
\begin{equation}
\label{eq:8}
\forall n: \mathbb{N}. \lnot (\alpha(n)=\rho)
\end{equation}
Let's remind ourselves for a minute about what the ``inequality sheaf'' $\lnot(x =y)$ looks like here, for sections $x,y$ of $\mathbf{N}$. This should be a subsheaf of $\mathbf{N}\times \mathbf{N}$, and it should be the topos complement of $a=b$ in $\mathbf{N}\times \mathbf{N}$, which means it should be the sheaf of all pairs of functions $(a,b)$ into $\mathbf{N}$ which don't agree everywhere on any nonempty open subset of their domain of definition. This isn't the same as saying they can't agree at any point! They can have equal values at points; they just can't have the same germ at any point, i.e. they can't agree on any nonempty open subset. The set where they agree is nowhere dense.

Earlier we defined a predicate $\mathcal{P}(n) = \alpha(n)\leq \rho$, $\mathcal{P}\subset \mathbb{N}$.  I claim it follows from \ref{eq:8} that $\lnot\lnot \mathcal{P}$ holds everywhere on $\mathbb{N}$, i.e. $\lnot\lnot \mathcal{P}=\mathbb{N}$.
\begin{equation}
\label{eq:9}
\forall n:\mathbb{N}.\lnot\lnot \alpha(n)\leq \rho
\end{equation}
Here, I follow the convention that whenver I use a single symbol $\leq$, or $<$, or $=$, I'm referring to the relation sheaf on continuous functions into $\mathbf{N}\times \mathbf{N}$ which is inherited directly from the corresponding relation on $\mathbf{N}\times \mathbf{N}$. To avoid confusion I will never use $\alpha(n)\neq \rho$ to refer to what I have described in \ref{eq:8} as $\lnot(\alpha(n)=\rho)$, because by the convention I have just referred to, the relation sheaf $a\neq b$ should refer to the sheaf of all pairs of continuous functions which disagree at every point.

To prove the claim, we induct on $n:\mathbb{N}$. Now it is a miracle that induction makes sense at all in this scenario, and that the resulting deduction is valid, considering that the induction is not really over the natural numbers at all but over the sheaf of locally constant functions on $X$ taking values in $\mathbb{N}$. But the sheaf $\mathbb{N}$ has the universal property of a natural numbers object in $Sh(X)$, and induction can be carried out in this generality, which allows us to show that the whole theory of Heyting arithmetic at higher types $(HA^{\omega})$ holds true for $\mathbb{N}$ in $Sh(X)$; in the context of the translation between topos theory and higher-order typed intuitionistic logic, this is the translation into topos theory of Godel's Dialectica proof of the consistency of arithmetic by showing that every provable sentence of $HA^{\omega}$ has a computational realizer in his System T.

So let us induct. In the case $n=0$,
\begin{equation}
\label{eq:10}
\alpha(0)\leq \rho
\end{equation}
this is self explanatory, as of course $\alpha(0)\leq \rho$ everywhere. (This is an example of what I mean when I say we cannot proceed by pure logic alone but have to make some elementary observations.)

So in particular $\lnot \lnot \alpha(0)\leq \rho$, and we are done with the base case.

Now assume $\lnot\lnot \alpha(n)\leq \rho$. Then since $\lnot \alpha(n)=\rho$ by assumption, I claim that
\begin{equation}
  \alpha(n)\leq \rho\implies \lnot\lnot(\alpha(n)=\rho\lor \alpha(n)<\rho)
  \label{eq:11}
\end{equation}
This is a classic example of typical intuitionistic reasoning. We know that $\alpha(n)\leq \rho$, but we don't know either that $\alpha(n)=\rho$ or $\alpha(n)<\rho$, so we can't conclude their disjunction. However, we can conclude that it would be absurd if neither were true. To justify my claim, we interpret it in the sheaf: if $\alpha(n)\leq \rho$ everywhere on an open subset $V$, then by definition of the topology on $\mathbf{N}$, $\alpha(n)<\rho$ (equivalently $\alpha(n+1)\leq\rho$) on an open subset $V_{<}\subset V$. On the other hand, the open set $\alpha(n)=\rho\subset V$ is the maximal open subset where this is everywhere true, which is the interior $V_{=}$ of $V-V_{<}$. The union $V_{=}\cup V_{<}$ is therefore open and dense in $V$, and so its double negation in the Heyting algebra of opens is all of $V$.

In intuitionistic logic, \ref{eq:11} can be strengthened to
\begin{equation}
\label{eq:12}
  \lnot\lnot \alpha(n)\leq \rho\implies \lnot\lnot(\alpha(n)=\rho\lor \alpha(n)<\rho)
\end{equation}
because whenever $A\implies \lnot\lnot B$, $\lnot\lnot A\implies\lnot\lnot B$. (Assume $\lnot\lnot A$, and assume for contradiction that $\lnot B$. First, we prove that as a result of the assumption $\lnot B$, we can conclude $\lnot A$. For contradiction, assume $A$; we can apply $A\implies \lnot\lnot B$ to conclude $\lnot\lnot B$, but by our assumption $\lnot B$, so we have $\lnot B\land \lnot \lnot B$, this is a contradiction, as desired, so we conclude $\lnot A$. Now, to return to the main proof: we now have $\lnot \lnot A$ and $\lnot A$, a contradiction, so we conclude $\lnot\lnot B$.)

Since $\lnot \lnot \alpha(n)\leq \rho$ was our induction hypothesis, we conclude
\begin{equation}
\label{eq:13}
\lnot\lnot(\alpha(n)=\rho\lor \alpha(n)<\rho)
\end{equation}
Now by \ref{eq:8}, we have $\lnot\alpha(n)=\rho$. From this it is again an exercise in intuitionistic logic to conclude $\lnot\lnot \alpha(n)<\rho$, as whenever we have $\lnot\lnot (A\lor B)$ and $\lnot B$ we can conclude $\lnot \lnot A$. (Proof: Assume $\lnot A$ for contradiction. By DeMorgan's law, $\lnot \lnot (A\lor B)$ implies $\lnot(\lnot A\land\lnot B)$; we already have $\lnot B$, so assuming $\lnot A$ gives us $\lnot A\land \lnot B$, a contradiction, as desired.)

Now we have already pointed out that $\alpha(n)<\rho$ is equivalent (by inspection of the meaning of the sentence when interpreted over a small open neighborhood of a point) to $\alpha(n+1)\leq \rho$. So our conclusion $\lnot\lnot \alpha(n)<\rho$ is equivalent to $\lnot \lnot \rho+1(n)\leq\rho$, which concludes the proof of the inductions step. Therefore we have proven \ref{eq:9}. It is now quick work to prove that this is in contradiction with \ref{eq:5}, which gives us the contradiction we sought when we assumed \ref{eq:7}.

Fix some large $N$ given by \ref{eq:5} which is an upper bound for $\rho$. (Again, the beauty of the sheaf logic is that when I say this, you can either think concretely about the model and choose some sufficiently small open set on which such an $N$ exists, or you can stop thinking of the sheaf theory at all and just reason in the intuitionistic predicate calculus, which is totally legitimate and backed up by soundness theorems.) Now set $N'=N+1$, so we have $\rho <\alpha(N)$ by assumption and also $\lnot\lnot \alpha(N+1)\leq \rho$. In the intuitionistic propositional calculus, from $(\lnot\lnot A)\land B$ we can conclude $\lnot\lnot(A\land B)$, as assume for contradiction that $\lnot (A\land B)$, then as we already are given $B$ by assumption, we must have $\lnot A$; but we have $\lnot\lnot A$, a contradiction.) This gives us $\lnot\lnot (\alpha(N)<\rho \land \rho <\alpha(N))$. It suffices now to observe the following simple facts about $\mathbf{N}$ and $\alpha$: that

• the relation $<$ is transitive on $\mathbf{N}$, and
• for any $n, m :\mathbb{N}$, $n<m$ iff $\alpha(n)<\alpha(m)$

From these two we should be able to conclude $\lnot\lnot (\alpha(N)<\alpha(N))$ and finally $\lnot\lnot N<N$. But of course it is a theorem of Heyting arithmetic that $\lnot N < N$, and any theorem of Heyting arithmetic goes through in the NNO. So we have our contradiction to \ref{eq:5}, as desired, proving the theorem.

It is clear that my explanation here takes up much more space than the usual work it would take to prove this in topology, but I have assumed unfamiliarity with even the basic tautologies of the intuitionistic propositional calculus. If the commentary between the formal theorems and sentences is removed, as well as the frequent sanity checks where we translate back into topology, and remove the proofs of standard, well known theorems of the intuitionistic propositional calculus which are easily learned, I think the proof is actually fairly short and simple. Beyond the conciseness of eliminating the bookkeeping of which open neighborhood of a point we are actually working with, there is something thrilling about saying ``It doesn't matter'' and throwing out the topology altogether.