claim follows.

A description of the stalks of the tensor product
follows purely by considering the logical form of the construction:
Let $X$ be a scheme (or a ringed space). Let $\F$ and $\G$
be $\O_X$-modules. Then the stalks of the tensor product coincide with the
tensor products of the stalks: $(\F \otimes_{\O_X} \G)_x \cong \F_x
\otimes_{\O_{X,x}} \G_x$.

We constructed the tensor product using the following operations: product of
two sets, free module on a set, quotient module with respect to a submodule;
submodule generated by a set of elements given by a geometric formula.
All of these operations are geometric, so the tensor product construction is
geometric as well (see Section <ref>). Hence taking stalks commutes with performing the

Recall that an $\O_X$-module $\F$ is flat if and only if all
stalks $\F_x$ are flat $\O_{X,x}$-modules. We can characterize flatness in the
internal language.

Let $X$ be a scheme (or a ringed space). Let $\F$ be
an $\O_X$-module. Then $\F$ is flat if and only if, from the internal
perspective, $\F$ is a flat $\O_X$-module.

Recall that flatness of an $A$-module $M$ can be characterized without
reference to tensor products by the following condition (using
suggestive vector notation): For any natural number $p$,
any $p$-tuple $m \? M^p$ of elements of $M$ and
any $p$-tuple $a \? A^p$ of elements of $A$, it should hold that

\[
a^T m = 0 \ \Longrightarrow\
\bigvee\limits_{q \geq 0} \exists n\?M^q, B\?A^{p \times q}\_
Bn = m \wedge a^T B = 0. \]

The equivalence of this condition with tensoring being exact holds
intuitionistically as
well <cit.>.
This formulation of flatness has the advantage that it is the conjunction of
geometric implications (one for each $p \geq 0$); therefore it holds internally
if and only if it holds at any point.

§.§ Support
Recall that the support of an $\O_X$-module $\F$ is
the subset $\supp\F \defeq \{ x \in X \,|\, \F_x \neq 0 \} \subseteq X$. If $\F$ is
of finite type, this set is closed, since its complement is then open by a
standard lemma. (We will give an internal proof of this fact in
Lemma <ref>.)

Let $X$ be a scheme (or a ringed space). Let $\F$ be
an $\O_X$-module. Then the interior of the complement of the support of $\F$
can be characterized as the largest open subset of $X$ on which the internal
statement $\F = 0$ holds.

For any open subset $U \subseteq X$, it holds that:

\begin{align*}
&\ U \subseteq \Int(X \setminus \supp \F) \\
\Longleftrightarrow&\ U \subseteq X \setminus \supp \F \\
\Longleftrightarrow&\ U \subseteq \{ x \in X \,|\, \forall s \in \F_x\_ s = 0 \} \\
\Longleftrightarrow&\ U \models \forall s\?\F\_ s = 0 \\
\Longleftrightarrow&\ U \models \speak{$\F = 0$}
\end{align*}

The second to last equivalence is because “$\forall s\?\F\_ s = 0$” is a
geometric implication and can thus be checked stalkwise.

The support of a sheaf of sets $\F$ is defined as the subset $\{ x \in X \,|\,
\text{$\F_x$ is not a singleton} \}$. A similar proof shows that the interior
of its complement can be characterized as the largest open subset of $X$ where
the internal statement $\speak{$\F$ is a singleton}$ holds.

§.§ Torsion
Let $R$ be a ring. Recall that the
torsion submodule $M_\tors$ of an $R$-module $M$ is defined as

\[ M_\tors \defeq \{ x\?M \,|\, \exists a\?R\_ \speak{$a$ regular} \wedge ax = 0 \}
\subseteq M. \]

This definition is meaningful even if $R$ is not an integral domain.
An $R$-module $M$ is torsion-free if and only if $M_\tors$ is
the zero submodule; an $R$-module $M$ is a torsion module if and only
if $M_\tors = M$.

Recall also that if $\F$ is a sheaf of $\O_X$-modules on an integral
scheme $X$, there is a unique subsheaf $\F_\tors \subseteq \F$ with the
property that $\Gamma(U,\F_\tors) = \Gamma(U,\F)_\tors$ for all affine open
subsets $U \subseteq X$. The content of the following proposition is that
internally constructing the torsion submodule of $\F$, regarded as a plain
module from the internal perspective, gives exactly this subsheaf. There is
therefore no harm in using the same notation “$\F_\tors$” for the result of
the internal construction.

Let $X$ be an integral scheme. Let $\F$ be an $\O_X$-module. Let $U
= \Spec A \subseteq X$ be an affine open subset. Let $s \in \Gamma(U,\F)$ be a local
section. Then

\[ s \in \Gamma(U,\F)_\tors \quad\text{if and only if}\quad
U \models s \in \F_\tors. \]

The “only if” direction is trivial in view of
Lemma <ref>: If $s$ is a torsion element
of $\Gamma(U,\F)$, there exists a regular element $a \in \Gamma(U,\O_X)$ such
that $as = 0$. By the lemma, this element is regular from the internal
perspective as well, so $U \models \speak{$a$ regular} \wedge as = 0$.

For the “if” direction, we may assume that there exists an open covering $X =
\bigcup_i U_i$ by standard open subsets $U_i = D(f_i)$ such that there are
sections $a_i \in \Gamma(U_i,\O_X) = A[f_i^{-1}]$ with $U_i \models \speak{$a_i$ regular}
\wedge a_i s = 0$. Without loss of generality, we may assume that the
denominators of the $a_i$'s are ones, that the $f_i$ are
finite in number, and that the $f_i$ are regular (nonzero, since $A$ is an
integral domain). By Lemma <ref>, the $a_i$ are
regular in $A[f_i^{-1}]$ and by regularity of the $f_i$ also regular in $A$.
Therefore their product $\prod_i a_i \in A$ is regular in $A$ as well and
annihilates $s$.

Let $X$ be a locally Noetherian scheme. Let $\F$ be
an $\O_X$-module. Let $x \in X$ be a point. Then $(\F_\tors)_x =
This would be obvious if the condition on an element $s\?\F$ to
belong to $\F_\tors$ were a geometric formula. Because of the universal
quantifier, it is not:

\[ s \in \F_\tors \quad\Longleftrightarrow\quad
\exists a\?\O_X\_ (\forall b\?\O_X\_ ab = 0 \Rightarrow b = 0) \wedge as = 0. \]

But since $X$ is assumed to be locally Noetherian, regularity is an open
property nonetheless (see Proposition <ref> for an
internal proof of this fact). Thus the claim still follows, just like in the
proof of Proposition <ref>.

§.§ Kähler differentials

Let $A \to B$ be a homomorphism of rings. The $B$-module $\Omega^1_{B|A}$ of
Kähler differentials can be constructed as the free $B$-module on the
basis $(db)_{b \in B}$ consisting of formal symbols modulo appropriate
relations ensuring that the map $b \mapsto db$ is $A$-linear and satisfies the
Leibniz rule; it verifies the universal property that the map $B \to
\Omega^1_{B|A}$ is the initial $A$-linear derivation of $B$.

For constructing the sheaf of Kähler differentials for a morphism of schemes,
one often resorts to the alternative construction as $I/I^2$, where $I
\subseteq B \otimes_A B$ is the kernel of the multiplication map $B \otimes_A B
\to B$. The verification of the universal property is slightly harder for this
construction. Gathmann comments on this situation as follows <cit.>:

Of course, if $f : X \to Y$ is a morphism of general (not necessarily affine)
schemes, we want to consider the relative differentials of every restriction
of $f$ to affine opens of $X$ and $Y$, and glue them together to get a quasi-coherent
sheaf $\Omega_{X|Y}$. To do this, we have to give a different description of the relative
differentials, as the construction [via the free module] does not glue very well.

After having constructed a global sheaf of Kähler differentials using the
alternative description (only in the case that $f$ is separated, though with a
little bit of more work this assumption can be dispensed with), he goes on as
follows <cit.>:

It should be stressed that [the definition using the alternative construction]
is essentially useless for practical computations. Its only use is to show that
a global object $\Omega_{X|Y}$ exists that restricts to the old definition on
affine open subsets. For applications, we will always use [the definition using
the free module and the calculation of the Kähler differentials of a morphism
of the form $k \to k[x_1,\ldots,x_n]/(f_1,\ldots,f_m)$] on open subsets.

Vakil chooses a similar route <cit.>.

Regarding the sheaf of Kähler differentials as the conormal sheaf of the
diagonal embedding (and hence using the alternative construction) is of course
essential for further developments and hence very useful. However, if the goal
is just to construct a global sheaf of Kähler differentials, we can employ the
internal language to construct it using only the formal construction via the
free module.

Specifically, if $f : X \to S$ is a morphism of schemes, we can construct, in
the internal universe of $\Sh(X)$, the module of Kähler differentials of the
morphism $f^\sharp : f^{-1}\O_S \to \O_X$. A number of basic properties then
follow purely formally:

Let $f : X \to S$ be a morphism of schemes (or of locally ringed
spaces). Let $\Omega^1_{X|S}$ be defined as the interpretation of the internal
construction $\Omega^1_{\O_X|f^{-1}\O_S}$.

* The sheaf of Kähler differentials has the following universal property:
For any open subset $U \subseteq X$, any $(f^{-1}\O_S)|_U$-linear
derivation $\O_X|_U \to \E$ over $U$ uniquely factors over $\O_X|_U \to
\Omega^1_{X|S}|_U$.

* The stalks $(\Omega^1_{X|S})_x$ are canonically isomorphic
to $\Omega^1_{\O_{X,x}|\O_{S,f(x)}}$.

* The sheaf $\Omega^1_{X|S}$ is quasicoherent.

The first claim is just the interpretation of the internal
universal property using the Kripke–Joyal semantics and using the
simplification rule given in Proposition <ref>.

The second claim is immediate because the construction of Kähler differentials
via the free module is geometric (page
page:geometric-constructions). Therefore the operations “taking
Kähler differentials” and “taking the stalk at $x$” commute.

For verifying the third claim, it suffices to verify that $\Omega^1_{X|S}$ is
quasicoherent in the case that $X = \Spec(B)$ and $S = \Spec(A)$ are affine.
Let $\varphi : A \to B$ be the homomorphism of rings given by $f$. We employ the
technique and notation of Section <ref>:

\begin{align*}
(\Omega^1_{B|A})^\sim &\cong
\underline{\Omega^1_{B|A}}[\F^{-1}] \cong
\Omega^1_{\ul{B}|\ul{A}}[\F^{-1}] \\
\Omega^1_{\ul{B}[\F^{-1}]|\ul{A}[(\varphi^{-1}[\F])^{-1}]} \cong
\Omega^1_{\O_{\Spec(B)}|f^{-1}\O_{\Spec(A)}}.
\end{align*}

The first isomorphism is by
Proposition <ref>, the second because the
geometric construction “taking Kähler differentials” commutes with “taking
constant sheaves” (since it can be expressed as pullback along a geometric
morphism), the third by 00RT, and the fourth
by Proposition <ref>.

Incidentally, the Stacks Project too uses the construction via the free
module 08RL, however because the Stacks Project doesn't employ
the internal language they have to manually sheafify and keep track of open

§.§ Internal proofs of common lemmas

Let $X$ be a scheme (or a ringed space). Let

\[ 0 \lra \F \lra \G \lra \H \lra 0 \]

be a short exact sequence of $\O_X$-modules. If $\F$ and $\H$ are of finite
type, so is~$$; similarly, if~$$ and~$$̋ are finite locally free, so
is $\G$.

From the internal perspective, we are given a short exact sequence
of modules with the outer ones being finitely generated (finite free)
and we have to show that the middle one is finitely generated (finite
free) as well. It is well-known that this follows; and since the usual proof of
this fact is intuitionistically valid, we are done.

The proof works very generally, in the context of arbitrary ringed
spaces, and is still very simple. This is common to proofs using the internal
language. Particular features of schemes enter only at clearly recognizable
points, for instance when an internal property specific to the structure sheaf
of schemes is used (such as in Proposition <ref>).

Let $X$ be a scheme (or a ringed space).

* Let $0 \to \F \to \G \to \H \to 0$ be an exact sequence
of $\O_X$-modules. If two of the three modules are coherent, so is the third.

* Let $\F \to \G$ be a morphism of $\O_X$-modules such that $\F$ is
of finite type and $\G$ is coherent. Then its kernel is of finite type as well.

* If $\F$ is a finitely presented $\O_X$-module and $\G$ is a
coherent $\O_X$-module, the $\O_X$-modules $\HOM_{\O_X}(\F,\G)$ and $\F \otimes_{\O_X} \G$
are coherent as well.

These statements follow directly from interpreting the
corresponding standard proofs of commutative algebra in the internal language.
For those standard proofs, see for instance the lecture notes of Ravi
Vakil <cit.>, where they are given as a series of

Let $X$ be a scheme (or a locally ringed space). Let $\alpha : \G
\to \H$ be an epimorphism of finite locally free~$Ø_X$-modules. Then the
kernel of~$α$ is finite locally free as well.\end{lemma}
\begin{proof}It suffices to give an intuitionistic proof of the following
statement: The kernel of a matrix over a local ring, which as a linear map is
surjective, is finite free.

Let~$M \? R^{n \times m}$ be such a matrix. Since by the surjectivity
assumption some linear combination of the columns is~$e_1$ (the first canonical
basis vector), some linear combination of the entries of the first row of~$M$
is~$1$. By locality of~$R$, at least one entry of the first row is invertible.
By applying appropriate column and row transformations, we may therefore assume that~$M$
is of the form
\[ \left(
\begin{array}{c|ccc}
1 & 0 & \cdots & 0 \\ \hline
0 & \multicolumn{3}{c}{\multirow{3}{*}{\raisebox{-5mm}{\scalebox{1.2}{$\widetilde M$}}}} \\
\raisebox{2pt}{\vdots} & & & \\
0 & & &
\end{array}
\right) \]
with the submatrix~$\widetilde M$ fulfilling the same condition as~$M$.
Continuing in this way, it follows that~$m \geq n$ and that we may assume
that~$M$ is of the form
\[ \left(
\begin{array}{ccc|c}
1 & & & \multirow{3}{*}{\raisebox{-3mm}{\scalebox{1.2}{\ 0}}} \\
& \ddots && \\
&& 1
\end{array}
\right)\!. \]
The kernel of such a matrix is obviously freely generated by the canonical
basis vectors corresponding to the zero columns. In particular, the rank of the
kernel is~$m-n$.
\end{proof}

\begin{rem}The internal language machinery gives no reason to believe that the
dual statement is true, \ie that the cokernel of a monomorphism of finite
locally free~$\O_X$-modules is finite locally free. This would follow from
an intuitionistic proof of the statement that the cokernel of an injective map
between finite free modules over a local ring is finite free. But this
statement is of course false (consider the exact sequence
$0 \lra \ZZ_{(2)} \stackrel{\cdot 2}{\lra} \ZZ_{(2)} \lra \FF_2 \lra 0$
\end{rem}

\begin{lemma}\label{lemma:epi-iso}Let~$X$ be a scheme (or a locally ringed space). Let~$\alpha : \G
\to \H$ be an epimorphism of finite locally free~$\O_X$-modules of the same
rank. Then~$\alpha$ is an isomorphism.\end{lemma}
\begin{proof}It suffices to give an intuitionistic proof of the following
statement: A square matrix over a local ring, which as a linear map is
surjective, is invertible.

This follows from the proof of the previous lemma, since it shows that the
kernel of such a matrix is finite free of rank zero.
\end{proof}

\begin{rem}The conclusion of Lemma~\ref{lemma:epi-iso} also holds if~$X$ is
only assumed to be a ringed space. To show this, it suffices to give an
intuitionistic proof of the following statement: A square matrix over a (not
necessarily local) ring, which as a linear map is surjective, is invertible.
Such a matrix~$A$ possesses a right inverse. Therefore~$\det A$ is invertible.
Thus~$A$ is invertible with inverse~$(\det A)^{-1} \cdot \operatorname{ad} A$.
\end{rem}

\begin{lemma}\label{lemma:mono-iso}Let~$X$ be a scheme (or a locally ringed space).
Let~$\alpha : \G \to \H$ be a morphism of finite locally
free~$\O_X$-modules. If~$\alpha$ is a monomorphism, then the rank of~$\G$ is
less than or equal to the rank of~$\H$.\end{lemma}

\begin{proof}It suffices to give an intuitionistic proof of the following
statement: A matrix over a nontrivial ring, which as a linear map is injective,
has a smaller or equal number of columns than rows. Such a proof can for instance be found
\end{proof}

\begin{lemma}Let~$X$ be a scheme (or a ringed space). Let
$0 \to \F \to \G \to \H \to 0$ be a short exact sequence of~$\O_X$-modules.
Then for the closures of the supports there holds the equation
$\Clos \supp \G = \Clos \supp \F \cup \Clos \supp \H$.
\end{lemma}
\begin{proof}Switching to complements, we have to prove that
\[ \Int(X \setminus \supp\G) = \Int(X \setminus \supp\F) \cap \Int(X \setminus
\supp\H). \]
By Proposition~\ref{prop:characterization-support}, it suffices to prove
\[ \Sh(X) \models (\G = 0\ \Longleftrightarrow\ \F = 0 \wedge \H = 0); \]
this is a basic observation in linear algebra, valid intuitionistically.
\end{proof}
Of course, a stronger version of this lemma -- about the supports themselves
instead of their closures -- is easily proven without using the internal
language. We included this example only for illustrative purposes.

\begin{lemma}Let~$X$ be a scheme (or a locally ringed space). Let~$\L$ be a line
bundle on~$X$, \ie an~$\O_X$-module locally free of rank~1.
Let~$s_1,\ldots,s_n \in \Gamma(X,\L)$ be global sections. Then these sections
globally generate~$\F$ if and only if
\[ \Sh(X) \models \bigvee_i \speak{$\alpha(s_i)$ is invertible for some
isomorphism~$\alpha : \L \to \O_X$}. \]
\end{lemma}
\begin{proof}It suffices to give an intuitionistic proof of the following fact:
Let~$R$ be a local ring. Let~$L$ be a free~$R$-module of rank~1.
Let~$s_1,\ldots,s_n\?L$ be given elements. Then~$L$ is generated as
an~$R$-module by these elements if and only if for some~$i$, the image of~$s_i$
under some isomorphism~$L \to R$ is invertible.

The choice of such an isomorphism does not matter, since any two such
isomorphisms~$\alpha, \beta : L \to R$ differ by a unit of~$R$: $\alpha(x) =
\alpha(\beta^{-1}(1)) \cdot \beta(x)$ for any~$x\?L$,
and~$\alpha(\beta^{-1}(1)) \cdot \beta(\alpha^{-1}(1)) = 1$ in~$R$.

For the ``if'' direction, we have that some~$\alpha(s_i)$ is a generator
of~$R$. Since~$\alpha$ is an isomorphism, it follows that~$s_i$ generates~$L$,
and thus that in particular, the family~$s_1,\ldots,s_n$ generates~$L$.

For the ``only if'' direction, we have that the unit of~$R$ can be expressed as
a linear combination of the~$\alpha(s_i)$, where~$\alpha : L \to R$ is some
isomorphism (whose existence is assured by the assumption on the rank of~$L$).
Since~$R$ is a local ring, it follows that one of the summands and thus one of
the~$\alpha(s_i)$ is invertible.
\end{proof}

\begin{rem}The canonical ring homomorphism~$\O_{X,x}
\twoheadrightarrow k(x)$ is local. Therefore a germ in~$\O_{X,x}$ is invertible
if and only if its image in~$k(x)$ is not zero. From this one can conclude that
global sections~$s_1,\ldots,s_n \in \Gamma(X,\F)$ generate~$\F$ if and only if,
for any point~$x \in X$, the images~$s_i \in \F|_x$ in the fibers do not vanish
\end{rem}

\begin{lemma}Let~$X$ be a scheme (or a ringed space). Let~$\L$ be a locally
free~$\O_X$-module of rank~1. Then~$\L^\vee \otimes_{\O_X} \L \cong \O_X$.\end{lemma}
\begin{proof}Recall that the dual is defined by~$\L^\vee \defeq
\HOM_{\O_X}(\L,\O_X)$. Since~``$\HOM$'' looks like~``$\Hom$'' from the internal
point of view, the dual sheaf~$\L^\vee$ looks just like the ordinary dual
module. However, to prove the claim, it does \emph{not} suffice to give an
intuitionistic proof of the following fact of linear algebra: ``Let~$L$ be a
free~$R$-module of rank~1. Then there exists an isomorphism~$L^\vee \otimes_R L
\to R$.'' Since the interpretation of ``$\exists$'' using the Kripke--Joyal
semantics is local existence, this would only show that~$\L^\vee \otimes_{\O_X}
\L$ is \emph{locally} isomorphic to~$\O_X$.

Instead, we have to actually \emph{write down} (\ie explicitly give) a
linear map in the internal language -- not using the assumption that~$L$ is
free of rank~1, as this would introduce an existential quantifier again (see
So we have to prove the following fact: Let~$L$ be an~$R$-module. Then there
explicitly exists a linear map~$L^\vee \otimes_R L \to R$ such that this map is
an isomorphism if~$L$ is free of rank~1.

This is done as usual: Define~$\alpha : L^\vee \otimes_R L \to R$ by~$\lambda
\otimes x \mapsto \lambda(x)$. Since~$L$ is free of rank~1, there is an
isomorphism~$L \cong R$. Precomposing~$\alpha$
with the induced isomorphism~$R^\vee \otimes_R R \to L^\vee \otimes_R L$,
we obtain the linear map~$R^\vee \otimes_R R \to R$ given by the same
term: $\lambda \otimes x \mapsto \lambda(x)$. One can check that an inverse is given
by~$x \mapsto \id_R \otimes x$.
\end{proof}

\begin{lemma}\label{lemma:torsion-stuff}
Let~$X$ be a scheme (or a ringed space). Let~$\F$ be
\begin{enumerate}
\item Assume~$X$ to be a locally Noetherian scheme. Then $\F$ is torsion-free
(meaning~$\F_\tors = 0$) if and only if all stalks~$\F_x$ are torsion-free.
\item The quotient sheaf~$\F/\F_\tors$ is torsion-free and the torsion
submodule~$\F_\tors$ is a torsion module.
\item The dual sheaf $\F^\vee$ is torsion-free.
\item If~$\F$ is reflexive (meaning that the canonical morphism~$\F \to
\F^{\vee\vee}$ is an isomorphism), then~$\F$ is torsion-free.
\item If~$\F$ is finite locally free, then~$\F$ is reflexive.
\item Assume~$X$ to be a Dedekind scheme and~$\F$ to be of finite presentation.
If~$\F$ is torsion-free, then~$\F$ is finite locally free.
% change references below if numbering changes
\end{enumerate}
\end{lemma}
\begin{proof}The first statement follows from the observation that~$(\F_\tors)_x
= (\F_x)_\tors$ (Proposition~\ref{prop:torsion-submodule-stalks}). All the
others follow simply by interpreting the corresponding facts of linear algebra
in the internal universe. For concreteness, we give intuitionistic proofs of
the last three statements.

So let~$M$ be a reflexive~$R$-module. We have to show that~$M$ is
torsion-free. To this end, let an element~$x \? M$ and a regular element~$a \?
R$ such that~$ax = 0$ be given. For any~$\vartheta \? M^\vee$, it follows
that~$\vartheta(x) = 0$, since~$a \vartheta(x) = \vartheta(ax) = \vartheta(0) =
0$ and~$a$ is regular. Thus the image of~$x$ under the canonical map~$M \to
M^{\vee\vee}$ is zero. By reflexivity, this implies that~$x$ is zero.

For statement~(5), we have to prove that~$R$-modules of the form~$R^n$ are
reflexive. This is obvious, the required inverse map is~$(R^n)^{\vee\vee} \to
R^n,\ \lambda \mapsto \sum_i \lambda(\vartheta_i)$ where~$\vartheta_i : R^n \to
R,\ (x_j)_j \mapsto x_i$.

In view of Corollary~\ref{cor:dedekind-smith} we can put matrices over~$\O_X$
into Smith canonical form if~$X$ is a Dedekind scheme. Therefore it suffices
to give an intuitionistic proof of the following fact: Let~$R$ be an integral
domain in the strong sense such that matrices over~$R$ can be put into
Smith canonical form. Let~$M$ be a finitely presented torsion-free~$R$-module.
Then~$M$ is finite free.

Such a proof can proceed as follows: Since~$M$ is finitely presented, it is the cokernel of
some matrix. Without loss of generality, we may assume that the presentation matrix is diagonal,
so~$M$ is isomorphic to some finite direct sum~$\bigoplus_i R/(a_i)$.
Since~$M$ is torsion-free, all the summands~$R/(a_i)$ are torsion-free as well.
Since~$R$ is an integral domain in the strong sense,
the~$a_i$ are either zero or invertible. Thus~$R/(a_i)$ is isomorphic to~$R$ or
to the zero module. In any case,~$R/(a_i)$ is finite free and therefore~$M$
is finite free as well.
\end{proof}

\section{Upper semicontinuous functions}
\label{sect:upper-semicontinuous-functions}

\subsection{Interlude on natural numbers}
In classical logic, the natural numbers are complete in the sense that any
inhabited set of natural numbers possesses a minimal element. This statement
cannot be proven intuitionistically -- intuitively, this is because one cannot
explicitly pinpoint the (classically existing) minimal element of an arbitrary
inhabited set;\footnote{Let~$\varphi$ be an arbitrary formula. Assuming that
any inhabited subset of the natural numbers possesses a minimal element, we
want to show that~$\varphi \vee \neg\varphi$. Define the subset $U \defeq \{ n \in
\NN \,|\, (n = 1) \vee \varphi \} \subseteq \NN$, which surely is inhabited by~$1
\in U$. So by assumption, there exists a number~$z \in \NN$ which is the
minimum of~$U$. We have $z = 0$ or $z > 0$. If~$z = 0$, we have~$0 \in U$,
so~$(0 = 1) \vee \varphi$, so~$\varphi$ holds.  If~$z > 0$, then~$\neg\varphi$
holds: If~$\varphi$ were true, zero would be an element of~$U$, contradicting
the minimality of~$z$.} see below for a sheaf-theoretic interpretation.

In intuitionistic logic, the completeness principle can be salvaged in two
essentially different ways: either by strengthening the premise, or by
weakening the conclusion.

\begin{lemma}\label{lemma:minimum-subset-naturals}
Let~$U \subseteq \NN$ be an inhabited subset of the natural
\begin{enumerate}
\item Assume~$U$ to be \emph{detachable}, \ie assume that for any natural
number~$n$, either~$n \in U$ or~$n \not\in U$. Then~$U$ possesses a minimal
\item In any case,~$U$ does \notnot possess a minimal element.
\end{enumerate}
\end{lemma}
\begin{proof}
The first statement can be proven by induction on the witness of inhabitation,
\ie the given number~$n$ such that~$n \in U$. We omit further details, since we will
not need this statement in our applications.

For the second statement, we give a careful proof since logical subtleties matter. To simplify the
exposition, we assume that~$U$ is upward-closed, \ie that any number
larger than some element of~$U$ lies in~$U$ as well. Any subset can be closed
in this way (by considering~$\{ n \in \NN \,|\, \exists m \in U\_ n \geq m \}$)
and a minimal element of the closure will be a minimal element for~$U$ as well.

We induct on the number~$n \in U$ given by the assumption that~$U$ is
inhabited. In the case~$n = 0$ we are done since~$0$ is a minimal element
of~$U$. For the induction step~$n \to n+1$, the intuitionistically valid double
negation of the law of excluded middle
\[ \neg\neg(n \in U \vee n \not\in U). \]
Because of the tautologies $(\varphi \Rightarrow \psi) \Rightarrow
(\neg\neg\varphi \Rightarrow \neg\neg\psi)$ and~$\neg\neg\neg\neg\varphi \Rightarrow
\neg\neg\varphi$ (see Section~\ref{sect:appreciating-intuitionistic-logic}), it
suffices to show that~$n \in U \vee n \not\in U$ implies the conclusion.
So assume~$n \in U \vee n \not\in U$.
If~$n \in U$, then~$U$ does \notnot possess a minimal element by the induction
hypothesis. If~$n \not\in U$, then~$n+1$ is a minimal element (and so, in
particular,~$U$ does \notnot possess a minimal element): If~$m$ is
any element of~$U$, we have~$m \geq n+1$ or~$m \leq n$. In the first case,
we're done. In the second case, it follows that~$n \in U$ because~$U$ is
upward-closed and so we obtain a contradiction. From this contradiction we
can trivially deduce~$m \geq n+1$ as well. \qedhere
\end{proof}

If we want to work with a complete partially ordered set (poset) of natural numbers in intuitionistic
logic, we have to construct a suitable completion. The idea of the following
definition is to encode numbers as the (not necessarily existing) minimum of
inhabited upward-closed subsets.
\begin{defn}The \emph{completed poset of natural numbers} is
the set~$\widehat{\NN}$ of all inhabited upward-closed subsets of~$\NN$, ordered by
reverse inclusion. The elements of~$\widehat{\NN}$ are called \emph{generalized natural numbers}.\end{defn}
\begin{lemma}The completed poset of natural numbers is the least poset
containing~$\NN$ and possessing minima
of arbitrary inhabited subsets.\end{lemma}
\begin{proof}
The embedding $\NN \hookrightarrow \widehat\NN$ is given by
\[ n \in \NN \quad\longmapsto\quad {\uparrow}(n) \defeq \{ m \in \NN \,|\, m \geq n \}. \]
If~$M \subseteq \widehat\NN$ is an inhabited subset, its minimum is
\[ \min M = \bigcup M \in \widehat\NN. \]
We omit the proof of the universal property.
\end{proof}

\begin{rem}\label{rem:surjectivity-embedding}
In classical logic, the map~$\widehat\NN \to \NN,\ U \mapsto \min U$
is a well-defined isomorphism of partially ordered sets. In fact, it is the
inverse of the canonical embedding~$\NN \hookrightarrow \widehat\NN$. In
intuitionistic logic, this embedding is still injective, but it cannot be
shown to be surjective: It is only the case that any element of~$\widehat\NN$
does \notnot possess a preimage (by Lemma~\ref{lemma:minimum-subset-naturals}).
\end{rem}

\subsection{A geometric interpretation}
We are interested in the completed natural numbers for the following reason: A
generalized natural number in the topos of sheaves on a topological space~$X$ is
the same as an upper semicontinuous function~$X \to \NN$.

\begin{lemma}\label{lemma:upper-semicontinuous-functions}
Let~$X$ be a topological space. The sheaf~$\widehat\NN$ of
generalized natural numbers on~$X$ is canonically isomorphic to the sheaf of upper
semicontinuous~$\NN$-valued functions on~$X$.\end{lemma}
\begin{proof}
When referring to the natural numbers in the internal language, we actually
refer to the constant sheaf~$\ul{\NN}$ on~$X$. (This is because the
sheaf~$\ul{\NN}$ fulfills the axioms for a natural numbers object,
cf.\@~\cite[Section~VI.1]{moerdijk-maclane:sheaves-logic}.) Recall that its sections on an
open subset~$U \subseteq X$ are continuous functions~$U \to \NN$, where~$\NN$
is equipped with the discrete topology.

Therefore, a section of~$\widehat\NN$ on an open subset~$U \subseteq X$ is
given by a subsheaf~$\A \hookrightarrow \ul{\NN}|_U$ such that
\[ U \models \exists n\?\ul{\NN}\_ n \in \A
\quad\text{and}\quad
U \models \forall n,m\?\ul{\NN}\_ n \geq m \wedge n \in \A \Rightarrow m \in
\A. \]
Since these conditions are geometric implications, they are satisfied if and only if any
stalk~$\A_x$ is an inhabited upward-closed subset of~$\ul{\NN}_x \cong \NN$.
The association
\[ x \in X \quad\longmapsto\quad \min\{ n \in \NN \,|\, n \in \A_x \} \]
thus defines a map~$X \to \NN$. This map is indeed upper semicontinuous, since
if~$n \in \A_x$, there exists an open neighborhood~$V$ of~$x$ such that the constant
function with value~$n$ is an element of~$\Gamma(V,\A)$ and therefore~$n \in
\A_y$ for all~$y \in V$.

Conversely, let~$\alpha : U \to \NN$ be an upper semicontinuous function. Then
\[ \text{$V \subseteq U$ open} \quad\longmapsto\quad \{ f : V \to \NN \,|\, \text{$f$
continuous,\ $f \geq \alpha$ on~$V$} \} \]
is a subobject of~$\ul{\NN}|_U$ which internally is inhabited and upward-closed.
Further details are left to the reader.
\end{proof}

Under the correspondence given by Lemma~\ref{lemma:upper-semicontinuous-functions}, locally \emph{constant}
functions map precisely to the (image of the) \emph{ordinary} internal natural numbers
(in the completed natural numbers).
In a similar vein, the sheaf given by the internal construction of
the set of \emph{all} upward-closed subsets of the natural numbers (not
only the inhabited ones) is canonically isomorphic to the sheaf of
upper semicontinuous functions with values in~$\NN \cup \{ +\infty
\}$.

The correspondence can be used to understand classical facts about
upper semicontinuous functions as features of intuitionistic number theory. For
instance, it is well-known that any upper semicontinuous~$\mathbb{N}$-valued
function on an arbitrary topological space is locally constant on a dense open subset.
This can be explained as follows: The generalized natural number associated to such a
function is \notnot an ordinary natural number from the internal point of view.
Since ``not not'' translates to ``holding on a dense open subset''
(Proposition~\ref{prop:modops-kripke}), it follows that there is a dense open
subset on which the function corresponds to an ordinary internal natural
number, \ie is locally constant.

\subsection{The upper semicontinuous rank function}
Recall that the rank of an~$\O_X$-module~$\F$ on a scheme~$X$ (or
locally ringed space) at a point~$x \in X$ is defined as the~$k(x)$-dimension
of the vector space~$\F_x \otimes_{\O_{X,x}} k(x)$. If we assume that~$\F$ is
of finite type around~$x$, this dimension is finite and equals the minimal
number of elements needed to generate~$\F_x$ as an~$\O_{X,x}$-module by
Nakayama's lemma.

In the internal language, we can define an element of~$\widehat\NN$ by
\begin{multline*}
\rank\F \defeq \min\{ n \in \NN \,| \\
\speak{there is a gen.\@ family for~$\F$ consisting of~$n$ elements} \} \in \widehat\NN.
\end{multline*}
If the module~$\F$ is finite locally free, it will be a finite free module from the
internal point of view and the rank defined in this way will be an
actual natural number (see below); but in general, the rank is really an element of the

\begin{prop}\label{prop:rank-function-internally}
Let~$\F$ be an~$\O_X$-module of finite type on a scheme~$X$ (or a locally ringed
space). Under the correspondence given by Lemma~\ref{lemma:upper-semicontinuous-functions}, the internally
defined rank maps to the rank function of~$\F$.
\end{prop}
\begin{proof}
We have to show that for any point~$x \in X$ and natural number~$n$, there
exists a generating family for~$\F_x$ consisting of~$n$
elements if and only if there exists an open neighborhood~$U$ of~$x$ such that
\[ U \models \speak{there exists a generating family
for~$\F$ consisting of~$n$ elements}. \]
The ``if'' direction is obvious. For the ``only if'' direction, consider
(liftings to local sections of a)
generating family~$s_1,\ldots,s_n$ of~$\F_x$. Since~$\F$ is of finite type,
there also exist sections~$t_1,\ldots,t_m$ on some neighborhood~$V$ of~$x$ which
generate any stalk~$\F_y$, $y \in V$. Since the~$t_i$ can be expressed as a
linear combination of the~$s_j$ in~$\F_x$, the same is true on some open
neighborhood~$U \subseteq V$ of~$x$. On this neighborhood, the~$s_j$ generate
any stalk~$\F_y$, $y \in U$, so by geometricity we have
\[ U \models \speak{$s_1,\ldots,s_n$ generate~$\F$}. \qedhere \]
\end{proof}
Once we understand when properties spread from points to
neighborhoods in logical terms, we will be able to give a simpler proof of Proposition~\ref{prop:rank-function-internally} (see

\begin{lemma}\label{lemma:rank-functor-locally-constant}
Let~$X$ be a scheme (or a locally ringed space). Let~$\F$ be an~$\O_X$-module of
finite type. If~$\F$ is finite locally free, its rank function is locally
constant. The converse holds if~$X$ is a reduced scheme.
\end{lemma}
\begin{proof}The rank function is locally constant if and only if internally,
the rank of~$\F$ is an actual natural number. Also recall that the structure
sheaf fulfills a certain field condition if~$X$ is a reduced
scheme (Corollary~\ref{cor:field-reduced}). Therefore it suffices to give a
proof of the following fact of intuitionistic linear algebra: Let~$R$ be a
local ring. Let~$M$ be a finitely generated~$R$-module. If~$M$ is finite
free, its rank is an actual natural number. The converse holds if~$R$ fulfills
the field condition that any element which is not invertible is zero.

So assume that such a module~$M$ is finite free. Then it is isomorphic
to~$R^n$ for some actual natural number~$n$; by the internal proof in
Lemma~\ref{lemma:kernel-of-epi-fingen}, the rank of~$M$ is therefore this
number~$n$ (for any surjection~$R^m \twoheadrightarrow R^n$ it holds that~$m
\geq n$).

Conversely, assume that the rank of~$M$ is an actual natural number. Then
there exists a minimal generating family~$x_1,\ldots,x_n\?M$. We can verify that this family is
indeed linearly independent (and thus a basis, demonstrating that~$M$ is finite
free): Let~$\sum_i a_i x_i = 0$ with~$a_i\?R$. If any~$a_i$ were
invertible, the family~$x_1,\ldots,x_{i-1},x_{i+1},\ldots,x_n$ would too
generate~$M$, contradicting the minimality. So each~$a_i$ is not invertible.
By the field property of~$R$, each~$a_i$ is zero.
\end{proof}

\begin{lemma}\label{lemma:locally-free-dense}
Let~$X$ be a reduced scheme. Let~$\F$ be an~$\O_X$-module of
finite type. Then~$\F$ is finite locally free on a dense open subset.\end{lemma}
\begin{proof}Since ``dense open'' translates to ``not not'' in the internal
language (Proposition~\ref{prop:modops-kripke}), it suffices to give an
intuitionistic proof of the following fact: Let~$R$ be a local ring which fulfills an
appropriate field condition. Let~$M$ be a finitely generated~$R$-module.
Then~$M$ is \notnot finite free.

By Remark~\ref{rem:surjectivity-embedding}, the rank of such a module~$M$ is
\notnot an actual natural number. By the last part of the
previous proof, it thus follows that~$M$ is \notnot finite free.
\end{proof}

\begin{rem}Besides basics on natural numbers in an intuitionistic
setting and some dictionary terms (``reduced'', ``finite locally free'',
``finite type``, ``dense open''), this proof does not depend on any further
tools. In particular, it doesn't depend on Nakayama's lemma or on facts about
semicontinuous functions. For the (more complex) standard proof of this fact, see for
instance~\cite{vakil:foag}, where the claim is dubbed an ``important hard
exercise'' (Exercise~13.7.K).\end{rem}

\subsection{The upper semicontinuous dimension function} Recall that the
dimension of a topological space~$X$ at a point~$x \in X$ is defined as the
\[ \dim_x X \defeq \inf\{ \dim U \,|\, \text{$U$ open neighborhood of~$x$} \}. \]

The map~$X \to \NN \cup \{+\infty\},\ x \mapsto \dim_x X$ is upper
semicontinuous and thus corresponds to an internal generalized (possibly
unbounded) natural number. The following proposition shows that this number has
an explicit description.

\begin{prop}Let~$X$ be a scheme. Then the upper semicontinuous function
associated to the internal number ``Krull dimension of~$\O_X\!$'' is the
dimension function~$x \mapsto \dim_x X$.\end{prop}
\begin{proof}Internally, we define the Krull dimension of~$\O_X$ as the infimum
over all natural numbers~$n$ such that~$\O_X$ is of Krull
dimension~$\leq n$. This infimum need not exist in the natural numbers, of
course; so we really mean the upward-closed set~$\A$ of all those numbers. (It
is inhabited if and only if, from the external perspective, the dimension
of~$X$ is locally finite. In this case, it defines a generalized natural number.)

We thus have to show for any point~$x \in X$:
\[ \inf\{ n \in \NN \cup \{+\infty\} \,|\, n \in \A_x \} =
\dim_x X. \]
The condition on~$n$ can be expressed as follows, where we write~``$\ul{n}$''
to denote the constant function with value~$n$:
\begin{align*}
&\ n \in \A_x \\
\Longleftrightarrow &\
\text{for some open neighborhood~$U$ of~$x$, $\ul{n} \in \Gamma(U,\A)$} \\
\Longleftrightarrow &\
\text{for some open neighborhood~$U$ of~$x$,} \\
& \qquad\qquad U \models \speak{$\O_X$ is of Krull dimension~$\leq n$} \\
\Longleftrightarrow &\
\text{for some open neighborhood~$U$ of~$x$,} \\
& \qquad\qquad \dim U \leq n
\end{align*}
The second equivalence follows from the external description of internally-defined
subsheaves given in Section~\ref{sect:internal-constructions}.
We thus have:
\[
\inf\{ n \,|\, n \in \A_x \} =
\inf\{ \dim U \,|\, \text{$U$ open neighborhood of~$x$} \}
= \dim_x X. \qedhere
\]
\end{proof}

\section{Modalities}
\label{sect:modalities}

Philosophers and logicians do not only study what is \emph{true}, but also what
is \emph{known}, what is \emph{believed}, what is \emph{possible}, and so on.
Such \emph{modalities} are absent from the usual mathematical practice.
However, it turns out that a specific kind of such modalities plays a role in
understanding when properties spread from points to neighborhoods.

Briefly, this is because for any point~$x$ of a topological space~$X$, there
exists a modal operator~$\Box$ such that for any formula~$\varphi$ of the
internal language of the sheaf topos~$\Sh(X)$, the internal
statement~$\Box\varphi$ means that~$\varphi$ holds on some open neighborhood
of the given point~$x$. In this way, we can reduce sheaf-theoretic questions to
questions of modal intuitionistic (non-sheafy) mathematics.

The techniques developed in this section also enable us to use the internal
language of~$\Sh(X)$ to talk about sheaves on \emph{subspaces} of~$X$ (and more
general \emph{sublocales} of~$X$).

Topological interpretations of modal logic were studied before, for instance by
Awodey and Kishida~\cite{awodey-kishida:modal}. However, they study a
different kind of modal operators, not corresponding to the Lawvere--Tierney
topologies of topos theory, and pursue different goals.

\subsection{Basics on truth values and modal operators}
\label{sect:basics-on-truth-values}

\begin{defn}The \emph{set of truth values~$\Omega$} is the powerset of the
singleton set~$1 \defeq \{\star\}$, where~$\star$ is a formal symbol.\end{defn}

In classical logic, any subset of~$\{\star\}$ is either empty or inhabited, so
that~$\Omega$ contains exactly two elements, the empty set (``false'')
and~$\{\star\}$ (``true''). But
in intuitionistic logic, this cannot be shown; indeed, if we interpret the
definition in the topos of sheaves on a space~$X$, we obtain a (rather large) sheaf~$\Omega$
\[ \text{$U \subseteq X$ open} \quad\longmapsto\quad \Gamma(U,\Omega) = \{ V \subseteq U \,|\, \text{$V$
open} \}. \]
(This is because by definition of~$\Omega$ as the power object of the terminal
sheaf~$1$, sections of~$\Omega$ on an open subset~$U$ correspond to
subsheaves~$\F \hookrightarrow 1|_U$, and those are given by the greatest open
subset~$V \subseteq U$ such that~$\Gamma(V,\F)$ is inhabited.)
Obviously, in general, this sheaf has many sections, in particular more than
the binary coproduct~$1 \amalg 1$ (unless any open subset of~$X$ is also

The \emph{truth value} of a formula~$\varphi$ is by definition the subset
$\{ x \? 1 \,|\, \varphi \} \in \Omega$, where~``$x$'' is a fresh variable not
appearing in~$\varphi$. This subset is inhabited if and only
if~$\varphi$ holds and is empty if and only if~$\neg\varphi$ holds.
Conversely, we can associate to a subset~$F \subseteq 1$ the
proposition~$\speak{$F$ is inhabited}$.

By the above description of~$\Omega$ in
a sheaf topos~$\Sh(X)$, the interpretation of the truth value
of a formula~$\varphi$ in the internal language of~$\Sh(X)$ is a certain open
subset of~$X$. Tracing the definitions, we see that this open subset is
precisely the largest open subset on which~$\varphi$ holds, \ie the union of
all open subsets~$U \subseteq X$ such that~$U \models \varphi$.

Under the correspondence of formulas with truth values, logical operations
like~$\wedge$ and~$\vee$ map to set-theoretic operations like~$\cap$ and~$\cup$
-- for instance, we have
\[ \{ x \? 1 \,|\, \varphi \} \cap \{ x \? 1 \,|\, \psi \} =
\{ x \? 1 \,|\, \varphi \wedge \psi \}. \]
This justifies a certain abuse of notation: We will sometimes treat elements
of~$\Omega$ as propositions and use logical instead of set-theoretic
connectives. In particular, if~$\varphi$ and~$\psi$ are elements of~$\Omega$,
we will write~``$\varphi \Rightarrow \psi$'' to mean~$\varphi \subseteq \psi$;
``$\bot$'' to mean~$\emptyset$; and~``$\top$'' to mean~$1$.

\begin{defn}\label{defn:modal-operator}
A \emph{modal operator} (or \emph{Lawvere--Tierney topology}) is a map~$\Box : \Omega \to \Omega$ such
that for all~$\varphi, \psi \in \Omega$,
\begin{enumerate}
\item $\varphi \Longrightarrow \Box\varphi$,
\item $\Box\Box\varphi \Longrightarrow \Box\varphi$,
\item $\Box(\varphi \wedge \psi) \Longleftrightarrow \Box\varphi \wedge \Box\psi$.
\end{enumerate}
Syntactically, the symbol~``$\Box$'' binds stronger than any other logical
connective. For instance, axiom~(2) is shorthand for~``$(\Box(\Box(\varphi)))
\Rightarrow (\Box(\varphi))$'' and axiom~(3) is shorthand for~``$(\Box(\varphi
\wedge \psi)) \Leftrightarrow ((\Box(\varphi)) \wedge (\Box(\psi)))$''.
\end{defn}

The intuition is that~$\Box\varphi$ is a certain weakening of~$\varphi$, where
the precise meaning of ``weaker'' depends on the modal operator. By the second
axiom, weakening twice is the same as weakening once.

In classical logic, where~$\Omega = \{ \bot, \top \}$, there are only two modal
operators: the identity map and the constant map with value~$\top$.
Both of these are not very interesting: The identity operator does not weaken
propositions at all, while the constant operator weakens every proposition to
the trivial statement~$\top$.

In intuitionistic logic, there can potentially exist further modal operators.
For applications to algebraic geometry, the following four operators will have
a clear geometric meaning and be of particular importance:
\begin{enumerate}
\item $\Box\varphi \defequiv (\alpha \Rightarrow \varphi)$, where~$\alpha$ is a
fixed proposition.
\item $\Box\varphi \defequiv (\varphi \vee \alpha)$, where~$\alpha$ is a
fixed proposition.
\item $\Box\varphi \defequiv \neg\neg\varphi$ (the \emph{double negation
\item $\Box\varphi \defequiv ((\varphi \Rightarrow \alpha) \Rightarrow \alpha)$,
where~$\alpha$ is a fixed proposition.
\end{enumerate}

\begin{lemma}Any modal operator~$\Box$ is monotonic, \ie if~$\varphi
\Rightarrow \psi$, then~$\Box\varphi \Rightarrow \Box\psi$. Furthermore,
a modus ponens rule holds: If~$\Box\varphi$ holds, and if~$\varphi$
implies~$\Box\psi$, then~$\Box\psi$ holds as well.\end{lemma}
\begin{proof}Assume~$\varphi \Rightarrow \psi$. This is equivalent to
supposing~$\varphi \wedge \psi \Leftrightarrow \varphi$. We are to show
that~$\Box\varphi \Rightarrow \Box\psi$, \ie that~$\Box\varphi \wedge
\Box\psi \Leftrightarrow \Box\varphi$. This follows since by the third
axiom on a modal operator, we have~$\Box\varphi \wedge \Box\psi \Leftrightarrow
\Box(\varphi \wedge \psi)$, and~$\Box$ respects equivalence of propositions.

For the second statement, consider that if~$\varphi \Rightarrow \Box\psi$, by
monotonicity and the second axiom on a modal operator it follows
that~$\Box\varphi \Rightarrow \Box\Box\psi \Rightarrow \Box\psi$.
\end{proof}

\label{proof-scheme-boxed-statements}The modus ponens rule justifies the
following proof scheme: When trying to show, given that some boxed
statement~$\Box\varphi$ holds, that some further boxed statement~$\Box\psi$
holds, we may give a proof of~$\Box\psi$ under the stronger
assumption~$\varphi$. Symbolically:
\[ (\Box\varphi \Rightarrow \Box\psi) \Longleftrightarrow
(\varphi \Rightarrow \Box\psi). \]

\begin{rem}There is some contention on what symbol one should use for modal
operators in the sense of Definition~\ref{defn:modal-operator}. This is
because, in the modal logic community, the symbol~``$\Box$'' usually refers to
the modal operator~``it is necessary that''. For this modal operator, one often
imposes the \emph{reflexivity axiom}~$\Box\varphi \Rightarrow \varphi$ which we
don't impose (and which would trivialize the theory). Conversely, our
axiom~$\varphi \Rightarrow \Box\varphi$ isn't meaningful in the necessity
interpretation. This axiom is meaningful for the modal operator~``it is
possible that'', commonly denoted~``$\Diamond$''; but for this modal operator, the
axiom~$\Diamond(\varphi \wedge \psi) \Leftrightarrow \Diamond\varphi \wedge
\Diamond\psi$ isn't meaningful.

A classical modal operator which matches our axioms is ``I believe that''
under the proviso of ultimate knowledge (``I believe every true

Goldblatt chooses the symbol~``$\nabla$'' for the modal operators in our
sense~\cite[Section~14.5]{goldblatt:topoi},~\cite{goldblatt:modality}. The
symbol~``$\varbigcirc$'' is also common, particularly in the hardware
verification community. A discussion of the relationship between these three
kinds of operators is contained in~\cite{pfenning:davies:reconstruction}. We
are grateful to Tadeusz Litak for valuable comments and references pertaining
to this topic.
\end{rem}

\subsection{Geometric meaning}\label{sect:modalities-geometric-meaning}
Let~$X$ be a topological space. As discussed
above, an open subset~$U \subseteq X$ defines an internal truth value (a global
section of the sheaf~$\Omega$). We also denote it by~``$U$'', such that
\[ V \models U \quad\Longleftrightarrow\quad V \subseteq U \]
for any open subset~$V \subseteq X$. (Shortcutting the various intermediate
steps, this can also be taken as a definition of~``$V \models U$''.)
If~$A \subseteq X$ is a closed subset, there is thus an internal truth
value~$A^c$ corresponding to the open subset~$A^c = X \setminus A$. If~$x \in
X$ is a point, we define~``$\notat{x}$'' to denote the truth value
corresponding to~$\Int(X \setminus \{x\})$, such that
\[ V \models \notat{x} \quad\Longleftrightarrow\quad V \subseteq \Int(X
\setminus \{ x \}) \quad\Longleftrightarrow\quad x \not\in V. \]

\begin{prop}\label{prop:modops-kripke}
Let~$U \subseteq X$ be a fixed open and~$A \subseteq X$ be a fixed
closed subset. Let~$x \in X$. Then, for any open subset~$V \subseteq X$, it
holds that:
\[ \renewcommand{\arraystretch}{1.3}\begin{array}{@{}lcl@{}}
V \models (U \Rightarrow \varphi) &\Longleftrightarrow&
V \cap U \models \varphi. \\[0.3em]
V \models (\varphi \vee A^c) &\Longleftrightarrow&
\textnormal{there is an open subset~$W \subseteq V$} \\
&& \quad\quad \textnormal{containing~$A \cap V$ such that $W \models \varphi$.} \\[0.3em]
V \models \neg\neg\varphi &\Longleftrightarrow&
\textnormal{there is a dense open subset~$W \subseteq V$ s.\,th.\@ $W \models
\varphi$.} \\[0.3em]
V \models ((\varphi \Rightarrow \notat{x}) \Rightarrow \notat{x}) &\Longleftrightarrow&
\textnormal{$x \not\in V$ or there is an open neighborhood~$W \subseteq V$} \\
&& \quad\quad \textnormal{of~$x$ such that $W \models \varphi$.}
\end{array} \]
\end{prop}
\begin{proof}
\begin{enumerate}
\item Omitted.

\item Let~$V \models \varphi \vee A^c$. Then there exists an open covering~$V =
\bigcup_i V_i$ such that for each~$i$, $V_i \models \varphi$ or $V_i \subseteq
A^c$. Let~$W \subseteq V$ be the union of those~$V_i$ such that~$V_i \models \varphi$.
Then~$W \models \varphi$ by the locality of the internal language and~$A \cap V
\subseteq W$.

Conversely, let~$W \subseteq V$ be an open subset containing~$A \cap V$ such
that~$W \models \varphi$. Then~$V = W \cup (V \cap A^c)$ is an open covering
attesting~$V \models \varphi \vee A^c$.

\item For the ``only if'' direction, let~$W \subseteq V$ be the largest
open subset on which~$\varphi$ holds, \ie the union of all open subsets
of~$V$ on which~$\varphi$ holds. For the ``if'' direction, we may assume that
the given set~$W$ is also the largest open subset on which~$\varphi$ holds (by
enlarging~$W$ if necessary). The claim then follows by the following chain of
\begin{align*}
&\ V \models \neg\neg\varphi \\
\Longleftrightarrow&\ \forall \text{$Y \subseteq V$ open}\_
\Bigl(\forall \text{$Z \subseteq Y$ open}\_ (Z \models \varphi) \Rightarrow Z
= \emptyset\Bigr) \Longrightarrow Y = \emptyset \\
\Longleftrightarrow&\ \forall \text{$Y \subseteq V$ open}\_
\Bigl(\forall \text{$Z \subseteq Y$ open}\_ Z \subseteq W \Rightarrow Z
= \emptyset\Bigr) \Longrightarrow Y = \emptyset \\
\Longleftrightarrow&\ \forall \text{$Y \subseteq V$ open}\_
Y \cap W = \emptyset \Longrightarrow Y = \emptyset \\
\Longleftrightarrow&\ \text{$W$ is dense in~$V$.}
\end{align*}

\item Straightforward, since the interpretation of the internal statement with
the Kripke--Joyal semantics is
\[ \forall \text{$Y \subseteq V$ open}\_
\Bigl(\forall \text{$Z \subseteq Y$ open}\_
Z \models \varphi \Rightarrow x \not\in Z\Bigr) \Longrightarrow x \not\in
Y. \qedhere \]
\end{enumerate}
\end{proof}

\subsection{The subspace associated to a modal operator}
\label{sect:subspace-to-modal-operator}
Any modal operator~$\Box : \Omega \to \Omega$ in the sheaf topos of~$X$ induces
on global sections a map
\[ j : \Open(X) \to \Open(X), \]
where~$\Open(X) = \Gamma(X,\Omega)$ is the set of open subsets of~$X$.
Explicitly, it is given by
\begin{align*}
j(U) &= \text{largest open subset of~$X$ on which~$\Box U$ holds} \\
&= \bigcup\ \{ V \subseteq X \ |\ \text{$V$ open},\ V \models \Box U \}.
\end{align*}
By the axioms for a modal operator, the map~$j$ fulfills similar such axioms: For any open
subsets~$U, V \subseteq X$,
\begin{enumerate}
\item $U \subseteq j(U)$,
\item $j(j(U)) \subseteq j(U)$,
\item $j(U \cap V) = j(U) \cap j(V)$.
\end{enumerate}
Such a map is called a \emph{nucleus} on~$\Open(X)$. Table~\ref{table:nuclei}
lists the nuclei associated to the four modal operators
of Proposition~\ref{prop:modops-kripke}.

\begin{table}
\centering
\renewcommand{\arraystretch}{1.3}
\begin{tabular}{llll}
\toprule
Modal operator & associated nucleus &
$j(V) = X$ iff \ldots &
subspace \\\midrule
$\Box\varphi \equiv (U \Rightarrow \varphi)$ &
$j(V) = \Int(U^c \cup V)$ & $U \subseteq V$ & $U$ \\
$\Box\varphi \equiv (\varphi \vee A^c)$ &
$j(V) = V \cup A^c$ & $A \subseteq V$ & $A$ \\
$\Box\varphi \equiv \neg\neg\varphi$ &
$j(V) = \Int(\Clos(V))$ & $V$ is dense in $X$ &
\multicolumn{1}{p{1cm}}{smallest dense sublocale of~$X$} \\
$\Box\varphi \equiv ((\varphi \Rightarrow \notat{x}) \Rightarrow \notat{x})$ &
%      $\Int(\Clos(V \cap \Clos\{x\}) \cup (X \setminus \Clos\{x\}))$ &
j(V) = X \setminus \Clos\{x\}, & \text{if $x \not\in V$} \\
j(V) = X, & \text{if $x \in V$}
\end{array}$ &
$x \in V$ & $\{x\}$ \\
\bottomrule
\end{tabular}
\vspace{0.5em}

\caption{\label{table:nuclei}List of important modal operators and their
associated nuclei (notation as in Proposition~\ref{prop:modops-kripke}).}
\end{table}

Any nucleus~$j$ defines a subspace~$X_j$ of~$X$, to be described below, with a small caveat: In
general, the subspace~$X_j$ cannot be realized as a topological subspace, but
only as a so-called \emph{sublocale}; the notion of a locale is a slight
generalization of the notion of a topological space, in which an underlying set
of points is not part of the definition. Instead, a locale is simply given by a
frame (a partially ordered set with certain properties) of arbitrary \emph{opens} satisfying some axioms -- these opens may, but do not necessarily have to,
be sets of points. Sheaf theory carries over to locales essentially unchanged,
since the notions of presheaves and sheaves only refer to open sets and coverings,
but not points.

Accessible introductions to the theory of locales include two notes by
Johnstone~\cite{johnstone:art,johnstone:point}. Locales are also well-known for
a curious application in the theory of

\begin{defn}\label{defn:subspace-by-nucleus}Let~$j$ be a nucleus on~$\Open(X)$.
Then the sublocale~$X_j$ of~$X$ is given by the frame of opens
$\Open(X_j) \defeq \{ U \in \Open(X) \,|\, j(U) = U \}$.
\end{defn}
If~$j$ is induced by a modal operator~$\Box$, we also write~``$X_\Box$''
for~$X_j$. In three of the four cases listed in Table~\ref{table:nuclei}, the
sublocale~$X_\Box$ can indeed be realized as a topological subspace. The only
exception is the sublocale~$X_{\neg\neg}$ associated to the double negation
modality. It can also be described as the \emph{smallest dense sublocale}
of~$X$; this is obviously a genuine locale-theoretic notion, since there
is (in general) no smallest dense topological subspace
(consider~$\RR$ and its dense subsets~$\QQ$ and~$\RR \setminus \QQ$).

The inclusion~$i : X_j \hookrightarrow X$ cannot in general be described on the
level of points, since~$X_j$ might not be realizable as a topological subspace.
But for sheaf-theoretic purposes, it suffices to describe~$i$ on the level of
opens. This is done as follows:
\[ i^{-1} : \Open(X) \lra \Open(X_j),\ \quad U \longmapsto j(U). \]
Thus we can relate the toposes of sheaves on~$X_j$ and~$X$ by the usual
pullback and pushforward functors.
\begin{align*}
i^{-1} \F &= \text{sheafification of $(U \mapsto \colim_{U \preceq i^{-1}V} \Gamma(V,\F))$} \\
i_* \G &= (U \mapsto \Gamma(i^{-1}U, \G)) = (U \mapsto \Gamma(j(U), \G))
\end{align*}
As familiar from honest topological subspace inclusions, the pushforward
functor~$i_* : \Sh(X_j) \to \Sh(X)$ is fully faithful and the composition~$i^{-1}
\circ i_* : \Sh(X_j) \to \Sh(X_j)$ is (canonically isomorphic to) the identity.

\subsection{Internal sheaves and sheafification}\label{sect:internal-sheaves}
It turns out that the image of
the pushforward functor~$i_* : \Sh(X_\Box) \to \Sh(X)$, where~$\Box$ is a modal
operator in~$\Sh(X)$, can be explicitly described. Namely, it consists exactly
of those sheaves which from the internal point of view
are so-called~\emph{$\Box$-sheaves}, a notion explained below.

Furthermore, if we identify~$\Sh(X_\Box)$ with its image in~$\Sh(X)$, the
pullback functor is given by an internal sheafification process with respect to
the modality~$\Box$. Thus the external situation of pushforward/pullback
translates to forget/sheafify. This broadens the scope of the internal
language of~$\Sh(X)$: It cannot only be used to talk about sheaves on~$X$ in a simple,
element-based language, but also to talk about sheaves on arbitrary subspaces

To describe the notion of~$\Box$-sheaves and related ones, we switch to the internal
perspective and thus forget that we're working over a base space~$X$; we are simply given a modal operator~$\Box :
\Omega \to \Omega$ and have to take care that our proofs are intuitionistically valid. A
reference for the material in this subsection is a preprint by de
Vries~\cite{vries:sheafification}.\footnote{On page~5 of that
preprint there is a slight typing error: Fact~2.1(i) gives the
characterization of~$j$-closedness, not~$j$-denseness. The correct
characterization of~$j$-denseness in that context is~$\forall b \in B\_ j(b \in

Recall that a set~$S$ is a \emph{subsingleton} if and only if~$\forall x,y\?S\_
x = y$, and that a set~$S$ is a \emph{singleton} if and only if it is a subsingleton and
it is inhabited (\ie~$\exists x\?S\_ \top$); this amounts to~$\exists!x\?S\_ \top$.

\begin{defn}\label{defn:box-sheaves}
A set~$F$ is \emph{$\Box$-separated} if and only if
\[ \forall x,y\?F\_ \Box(x = y) \Longrightarrow x = y. \]
A set~$F$ is a \emph{$\Box$-sheaf} if and only if it is~$\Box$-separated and
\[ \forall S \subseteq F\_
\Box(\speak{$S$ is a singleton}) \Longrightarrow
\exists x\?F\_ \Box(x \in S). \]
\end{defn}

The two conditions can be combined: A set~$F$ is a~$\Box$-sheaf if and only if
\[ \forall S \subseteq F\_
\Box(\speak{$S$ is a singleton}) \Longrightarrow
\exists! x\?F\_ \Box(x \in S). \]

Intuitively, reading~``$\Box\varphi$'' as ``locally~$\varphi$'', a set
is~$\Box$-separated if elements which are locally equal are in fact equal. A
set is a~$\Box$-sheaf if furthermore for any set~$S$ of elements which locally
contains just a single element there is an element which is locally contained

This phrasing is reminiscent of the usual gluing condition, which demands that
any family of sections which locally is just a single section (in that the
sections of the family agree on their common domain of definition) gives rise
to a global section which coincides with the given sections on their respective
domain. Remark~\ref{rem:modal-operator-in-presheaf-topos} below sketches how to
make this relation precise.

\begin{defn}\label{defn:plus-construction}
The \emph{plus construction} of a set~$F$ with respect to~$\Box$ is the set
\[ F^+ \defeq \{ S \subseteq F \,|\, \Box(\speak{$S$ is a singleton}) \}/{\sim},
\]
where the equivalence relation is defined by~$S \sim T \vcentcolon\Leftrightarrow
\Box(S = T)$. There is a canonical map~$F \to F^+$ given by~$x \mapsto
[\{x\}]$. The \emph{$\Box$-sheafi\-fi\-ca\-tion} of a set~$F$ is the
\end{defn}

If~$F$ is~$\Box$-separated, then for any subset~$S \subseteq F$ it holds
\[ \Box(\speak{$S$ is a singleton}) \quad\Longleftrightarrow\quad
\speak{$S$ is a subsingleton} \wedge \Box(\speak{$S$ is inhabited}). \]

\begin{rem}\label{rem:modal-operator-in-presheaf-topos}
The topos of \emph{pre}sheaves on a topological space~$X$ admits an
internal language as well~\cite[Section~VI.7, discussion after
Theorem~1]{moerdijk-maclane:sheaves-logic}. In it, there
exists a modal operator~$\Box$ reflecting the topology of~$X$. A presheaf on~$X$ is separated
in the usual sense if, from the internal perspective of~$\PSh(X)$, it
is~$\Box$-separated; and it is a sheaf if, from the internal perspective, it
is a~$\Box$-sheaf. Furthermore, the~$\Box$-sheafification of a presheaf
(considered as a set from the internal perspective) coincides with the usual

\begin{ex}\label{ex:special-sets-sheaves}
Any singleton set is a~$\Box$-sheaf. The empty set is
always~$\Box$-separated (trivially) and is a~$\Box$-sheaf if and only
if~$\Box\bot \Rightarrow \bot$.\end{ex}

We will see geometric examples of~$\Box$-sheaves in further sections.
For instance, on an integral or locally Noetherian scheme~$X$, the structure sheaf~$\O_X$
is~$\neg\neg$-separated and its~$\neg\neg$-sheafification is the sheaf~$\K_X$
of rational functions (Proposition~\ref{prop:kx-is-negneg-sheafification}).

\begin{lemma}For any set~$F$, it holds that: \begin{enumerate}
\item $F^+$ is~$\Box$-separated.
\item The canonical map~$F \to F^+$ is injective if and only if~$F$
\item If~$F$ is~$\Box$-separated, then $F^+$ is a~$\Box$-sheaf.
\item If~$F$ is a~$\Box$-sheaf, then the canonical map~$F \to F^+$ is bijective.
\end{enumerate}
Let $\Sh_\Box(\Set)$ be the full subcategory of~$\Set$ consisting of
the~$\Box$-sheaves. Then it holds that:
\begin{enumerate}
\addtocounter{enumi}{4}
\item The functor~$(\placeholder)^+ : \Set \to \Set$ is left exact.
\item The functor~$(\placeholder)^{++} : \Set \to \Sh_\Box(\Set)$ is left exact and left
adjoint to the forgetful functor~$\Sh_\Box(\Set) \to \Set,\ F \mapsto F$.
\end{enumerate}\end{lemma}
\begin{proof}These are all straightforward, and in fact simpler than their
classical counterparts, since there are no colimit formulas which would have to
be dealt with.
\end{proof}

\begin{rem}\label{rem:epi-in-box-sheaves}
As is to be expected from the familiar inclusion of sheaves in
presheaves on topological spaces, the forgetful functor~$\Sh_\Box(\Set) \to \Set$
does not in general preserve colimits. It is instructive to see why
epimorphisms in~$\Sh_\Box(\Set)$ need not be epimorphisms in~$\Set$: A map~$f:A
\to B$ between~$\Box$-sheaves is an epimorphism in~$\Sh_\Box(\Set)$ if and only
\[ \forall y\?B\_ \Box(\exists x\?X\_ f(x) = y), \]
that is preimages do not need to exist, it suffices for them to~``$\Box$-exist''.
(Using results about the~$\Box$-translation, to be introduced below, this
characterization will be obvious.) This condition is intuitionistically weaker
than the condition that~$f$ is an epimorphism in~$\Set$, \ie that~$f$ is
surjective. This should be compared to the failure of the forgetful functor~$\Sh(X)
\to \PSh(X)$ to preserve epimorphisms: A morphism of sheaves does not need to
have preimages for any local section in order to be an epimorphism. Instead, it
suffices for any local section to \emph{locally} have preimages.\end{rem}

\begin{prop}Let~$X$ be a topological space. Let~$\Box$ be a modal operator
in~$\Sh(X)$. Let~$i : X_\Box \hookrightarrow X$ be the inclusion of the
associated sublocale. Corestricting the pushforward functor~$i_* : \Sh(X_\Box) \to
\Sh(X)$ to its essential image, it induces an equivalence~$\Sh(X_\Box) \simeq
\Sh_\Box(\Sh(X))$ between the category of sheaves on~$X_\Box$ and the category
of~$\Box$-sheaves in~$\Sh(X)$.
\end{prop}
\begin{proof}For the further development of the theory, we need the statement
of this proposition, but not the proof, which really is routine in dealing with
subtoposes and modal operators. Nevertheless, a proof can proceed by
combining Example~A4.6.2(a) and Theorem~C1.4.7
of~\cite{johnstone:elephant}, observing that for a topos of sheaves on a
locale~$Y$ it holds that~$\Open(Y) = \Gamma(Y, \Omega_{\Sh(Y)})$, and that the
subobject classifier of~$\Sh_\Box(\Sh(X))$ is~$\{ \varphi : \Omega_{\Sh(X)} \,|\,
\Box \varphi \Leftrightarrow \varphi \}$.
\end{proof}

\begin{rem}It's possible to rewrite the sheaf condition in the following form.
A set~$F$ is~$\Box$-separated if and only if, for any truth value~$\varphi \?
\Omega$ such that~$\Box\varphi$, the canonical map
\[ F \lra F^\varphi, \]
which maps an element~$x\?F$ to the constant map~$\varphi \to X$ with value~$x$
(where~$\varphi$ is considered as a subset of the terminal set~$1$), is
injective. The set~$F$ is a~$\Box$-sheaf if and only if furthermore this map is
surjective for all such truth values.
\end{rem}

\subsection{Sheaves for the double negation modality}
\label{sect:negneg-sheaves}

Recall that if~$\Box$ is the modal operator associated to a sub\emph{space}~$Y$
of a topological space~$X$, then the sheaves on~$X$ which are~$\Box$-sheaves
are easy to describe: These are precisely the sheaves in the essential image of
the pushforward functor~$\Sh(Y) \to \Sh(X)$. For the double negation modality,
the same is true, only that~$Y$ is then the perhaps unfamiliar \emph{smallest
dense sublocale} of~$X$.

The following proposition gives a characterization of~$\neg\neg$-separated
presheaves and~$\neg\neg$-sheaves in explicit terms.

\begin{prop}\label{prop:negneg-sheaves}
Let~$X$ be a topological space. Let~$\F$ be a sheaf on~$X$. Then:
\begin{enumerate}
\item $\F$ is~$\neg\neg$-separated if and only if any two local sections
of~$\F$, which are defined on a common domain and which agree on a dense open
subset of their domain, are already equal.
\item $\F$ is a~$\neg\neg$-sheaf if and only if it is~$\neg\neg$-separated and
for any open~$U \subseteq X$ and any open~$V \subseteq U$ dense
in~$U$, any~$V$-section of~$\F$ extends to an~$U$-section of~$\F$.
\item If~$\F$ is~$\neg\neg$-separated, the sections of $\F^+$ on an open
subset~$U \subseteq X$ can be described by pairs~$\langle V,s \rangle$, where~$V$ is a dense
open subset of~$U$ and~$s$ is a section of~$\F$ on~$V$. Two such pairs~$\langle V,s \rangle,
\langle V',s' \rangle$ determine the same element in~$\Gamma(U,\F^+)$ if and only if~$s$ and~$s'$
agree on~$V \cap V'$.
\end{enumerate}
\end{prop}
\begin{proof}
The first statement is obvious from the definition of~$\neg\neg$-separatedness
(Definition~\ref{defn:box-sheaves} for~$\Box = \neg\neg$) and the geometric
interpretation of double negation (Proposition~\ref{prop:modops-kripke}).

For the second statement, we need to show that, assuming that~$\F$
is~$\neg\neg$-separated, the sheaf~$\F$ has the extension property if and only if
\begin{multline*}
\Sh(X) \models \forall \S \? \P(\F)\_
\speak{$\S$ is a subsingleton} \wedge
\neg\neg(\speak{$\S$ is inhabited}) \Longrightarrow \\
\exists x\?\F\_ \neg\neg(x \in \S).
\end{multline*}
A section~$\S \in \Gamma(U,\P(\F))$ which internally is a
subsingleton and \notnot inhabited is precisely a subsheaf~$\S \hookrightarrow
\F|_U$ such that all stalks~$\S_x$, $x \in U$ are subsingletons and such that for
some dense open subset~$V \subseteq U$, the stalks~$\S_x$, $x \in V$ are
inhabited. This is precisely the datum of a section of~$\F$ defined on some
dense open subset of~$U$, considering the gluing of the unique germs in~$\S_x$ for
those points~$x$ such that~$\S_x$ is inhabited. (Conversely, a section~$s \in
\Gamma(V,\F)$ defines a subsheaf~$\S$ by setting~$\Gamma(W,\S) \defeq \{ s|_W \,|\,
W \subseteq V \}$.)

In view of this explicit description and the observation that the asserted
existence~(``$\exists x\?\F\_ \neg\neg(x \in \S)$'') is actually a question of
unique existence, the second statement follows.

For the third statement, one can check that the presheaf on~$X$ defined by
\[ \text{$U \subseteq X$ open} \quad\longmapsto\quad
\{ \langle V,s \rangle \,|\, \text{$V \subseteq U$ dense open},\ s \in \Gamma(V,\F)
\}/{\sim} \]
is in fact a sheaf (with respect to the topology of~$X$), internally a $\neg\neg$-sheaf,
and that it has the universal property of the~$\neg\neg$-sheafification
\end{proof}

The conditions~(1) and~(2) of Proposition~\ref{prop:negneg-sheaves} can be
summarized as follows: A sheaf~$\F$ on a topological space is
a~$\neg\neg$-sheaf if and only if, for any open subset~$U \subseteq X$, the
restriction map~$\Gamma(\Int\Clos U, \F) \to \Gamma(U,\F)$ is

In the case that~$X$ contains a \emph{generic point}, that is a point~$\xi \in X$
such that~$\Clos\{\xi\} = X$, we can describe the sublocale~$X_{\neg\neg}$ in
simple terms: In this case, it coincides with the subspace~$\{\xi\}$.
For instance, such a generic point exists and is unique if~$X$ is an irreducible scheme.

\begin{lemma}\label{lemma:negneg-generic-point}
Let~$X$ be a topological space and~$\xi \in X$ be a point such
that~$\Clos\{\xi\} = X$. Then the modal operator~$\Box \defequiv ((\placeholder
\Rightarrow \notat{\xi}) \Rightarrow \notat{\xi})$ coincides with the double
negation modality and~$X_{\neg\neg} = \{\xi\}$ as sublocales of~$X$.\end{lemma}
\begin{proof}The semantics of the formula~$\notat{\xi}$ was defined by the
\[ U \models \notat{\xi} \quad\Longleftrightarrow\quad
\xi \not\in U. \]
By the assumption on~$\xi$, this is equivalent to requiring~$U = \emptyset$.
Thus for any open subset~$U$ the formulas~$\notat{\xi}$ and~$\bot$ have the
same meaning; they are therefore logically equivalent from the internal point of
view. The given modal operator thus simplifies:
\[ \Box\varphi \quad\equiv\quad ((\varphi \Rightarrow \notat{\xi}) \Rightarrow \notat{\xi})
\quad\Leftrightarrow\quad ((\varphi \Rightarrow \bot) \Rightarrow \bot)
\quad\Leftrightarrow\quad \neg\neg\varphi. \]
The second claim follows from Table~\ref{table:nuclei}.
\end{proof}

\begin{cor}\label{cor:negneg-generic-point-pushpull}
Let~$X$ be a topological space and let~$\xi \in X$ be a point such
that~$\Clos\{\xi\} = X$. Since~$X_{\neg\neg} = \{\xi\}$, the
category of~$\neg\neg$-sheaves in~$\Sh(X)$ coincides with the category of
sheaves on~$\{\xi\}$ and can therefore be identified with the category of sets.
Under this identification,
\begin{enumerate}
\item sheafifying an object~$\F \in \Sh(X)$ with respect
to the double negation modality (\ie pulling back to~$X_{\neg\neg}$) is the
same as calculating its generic stalk~$\F_\xi$ and
\item pushing forward a set~$M$ along~$X_{\neg\neg} \hookrightarrow X$ is the
same as calculating the constant sheaf associated to~$M$.
\end{enumerate}
\end{cor}
\begin{proof}The first statement follows because pulling back to~$X_{\neg\neg}$
is the same as pulling back to~$\{\xi\}$. The pushforward of a set~$M$,
considered as a sheaf on~$X_{\neg\neg}$, to~$X$ is explicitly given by
\[ U \quad\longmapsto\quad \begin{cases}
M, & \text{if $U \neq \emptyset$,} \\
\{\star\}, & \text{else.}
\end{cases} \]
We omit the routine verification that this sheaf coincides with the constant
sheaf~$\underline{M}$ associated to~$M$.
\end{proof}

The following technical lemma will occasionally be handy. It is an internal
reflection of the fact that an open subset of an affine scheme can always be
written as the union of standard open subsets. We will generalize it
to schemes which are not necessarily integral in
Section~\ref{sect:rational-functions} (see

\begin{lemma}\label{lemma:dense-standard-reflection}
Let~$X$ be an integral scheme. Let~$\varphi$ be any formula
over~$X$. Then
\[ \Sh(X) \models \neg\neg\varphi \Longrightarrow \exists f\?\O_X\_
\neg\neg(\speak{$f$ \inv}) \wedge (\speak{$f$ \inv} \Rightarrow \varphi). \]
\end{lemma}
\begin{proof}We may assume that~$X$ is the spectrum of an integral domain~$A$
and that there is a dense open subset~$U \subseteq X$ on which~$\varphi$ holds.
The open set~$U$ may be covered by standard open subsets~$D(f_i)$; since~$X$ is
irreducible, at least one of these is itself
dense. We may take this~$f_i$ as the sought~$f$.
\end{proof}

We can now also follow up on a promise made in Section~\ref{sect:appreciating-intuitionistic-logic} and prove the following
somewhat tangential lemma.
\begin{lemma}\label{lemma:boolean-dense}
Let~$X$ be a topological space. The internal language of~$\Sh(X)$ is Boolean if
and only if for any open subset~$U \subseteq X$ it holds that~$U$ is the only
dense open subset of~$U$.
\end{lemma}
\begin{proof}That the internal language of~$\Sh(X)$ is Boolean amounts to
\[ \Sh(X) \models \forall \varphi\?\Omega\_ \neg\neg\varphi \Rightarrow
\varphi. \]
This is equivalent to the external statement that for any open subset~$U
\subseteq X$ and for any open subset~$V \subseteq U$ it holds that: If~$V$ is
dense in~$U$, then~$V$ is equal to~$U$.
\end{proof}

\subsection{\texorpdfstring{The~$\Box$-translation}{The □-translation}}
\label{sect:box-translation}

In logic, there is certain well-known transformation~$\varphi
\mapsto \varphi^{\neg\neg}$ on formulas, the \emph{double negation
translation}, with the following curious property: A formula~$\varphi$ is
derivable in classical logic if and only if its
translation~$\varphi^{\neg\neg}$ is derivable in intuitionistic logic. The
translation~$\varphi^{\neg\neg}$ is obtained from~$\varphi$ by putting
``$\neg\neg$'' before any subformula, \ie before any~``$\exists$''
and~``$\forall$'', around any logical connective, and around any atomic
statement (``$x=y$'', ``$x \in A$''). For instance, the double negation
translation of ``$f$ is surjective'' is
\[ \neg\neg \forall y\?Y\_ \neg\neg \exists x\?X\_ \neg\neg f(x) = y. \]

We will describe a slight generalization of the double negation translation,
the~$\Box$-translation for any modal operator~$\Box$. It will be pivotal
for using the internal language of a space~$X$ to express internal statements
about sheaves defined on subspaces of~$X$. The~$\Box$-translation has been studied
in other contexts
before~\cite{aczel:russell-prawitz,escardo:oliva:peirce-shift}. To the best of
our knowledge, this application -- expressing the internal language of
subtoposes in the internal language of the ambient topos -- is new.

\begin{defn}The~\emph{$\Box$-translation} is recursively defined as follows.
\newcommand{\optBox}{\textcolor{gray}{\Box}}
\begin{align*}
(f = g)^\Box &\defequiv \Box(f = g) \\
(x \in A)^\Box &\defequiv \Box(x \in A) \\
\top^\Box &\defequiv \Box\top \quad \text{($\Leftrightarrow \top$)} \\
\bot^\Box &\defequiv \Box\bot \\
(\varphi \wedge \psi)^\Box &\defequiv \optBox(\varphi^\Box \wedge \psi^\Box) &
\textstyle (\bigwedge_i \varphi_i)^\Box &\defequiv \textstyle \optBox(\bigwedge_i \varphi_i^\Box) \\
(\varphi \vee \psi)^\Box &\defequiv \Box(\varphi^\Box \vee \psi^\Box) &
\textstyle (\bigvee_i \varphi_i)^\Box &\defequiv \textstyle \Box(\bigvee_i \varphi_i^\Box) \\
(\varphi \Rightarrow \psi)^\Box &\defequiv \optBox(\varphi^\Box \Rightarrow \psi^\Box) \\
(\forall x\?X\_ \varphi)^\Box &\defequiv \optBox(\forall x\?X\_ \varphi^\Box) &
(\forall X\_ \varphi)^\Box &\defequiv \optBox(\forall X\_ \varphi^\Box) \\
(\exists x\?X\_ \varphi)^\Box &\defequiv \Box(\exists x\?X\_ \varphi^\Box) &
(\exists X\_ \varphi)^\Box &\defequiv \Box(\exists X\_ \varphi^\Box)
\end{align*}
\end{defn}

\begin{defn}A formula~$\varphi$ is \emph{$\Box$-stable} if and only
if~$\Box\varphi$ implies~$\varphi$.\end{defn}

\begin{lemma}\begin{enumerate}
\item Formulas in the image of the $\Box$-translation are~$\Box$-stable,
\ie for any formula~$\varphi$ it holds that
$\Box(\varphi^\Box) \Longrightarrow \varphi^\Box$.
\item In the definition of the~$\Box$-translation, one may omit the boxes
printed in gray.
\end{enumerate}\end{lemma}
\begin{proof}The first statement is obvious, since one of the axioms for a modal
operator demands that~$\Box\Box\varphi \Rightarrow \Box\varphi$ for any
formula~$\varphi$. The second statement follows by an induction on the
formula structure. By way of example, we prove the case for~``$\Rightarrow$'':
\newcommand{\withgray}{\text{$\Box$ with the gray parts}}
\newcommand{\withoutgray}{\text{$\Box$ without the gray parts}}
\begin{align*}
&\ (\varphi \Rightarrow \psi)^\withgray \\
\Longleftrightarrow &\ \Box(\varphi^\withgray \Rightarrow \psi^\withgray) \\
\Longleftrightarrow &\ (\varphi^\withgray \Rightarrow \psi^\withgray) \\
\Longleftrightarrow &\ (\varphi^\withoutgray \Rightarrow \psi^\withoutgray) \\
\Longleftrightarrow &\ (\varphi \Rightarrow \psi)^\withoutgray
\end{align*}
The first step is by definition; the second by~$\Box$-stability
of~$\psi^\withgray$ and the intuitionistic tautology~$\Box(\alpha \Rightarrow
\beta) \Leftrightarrow (\alpha \Rightarrow \beta)$ for~$\Box$-stable
formulas~$\beta$; the third by the induction hypothesis; and the fourth by
\end{proof}

\begin{lemma}\label{lemma:box-translation-sound}
The~$\Box$-translation is sound with respect to intuitionistic logic:
Assume that there exists an intuitionistic proof of an
implication~$\varphi \Rightarrow \psi$. Then there is also an intuitionistic
proof of the translated implication~$\varphi^\Box \Rightarrow \psi^\Box$.
\end{lemma}
\begin{proof}This follows by an induction on the structure of intuitionistic
proofs. We have to verify that we can mirror any inference rule of
intuitionistic logic in the translation. For instance, one of the disjunction
rules justifies the following proof scheme: In order to prove~$\varphi \vee
\psi \Rightarrow \chi$, it suffices to give proofs of~$\varphi \Rightarrow
\chi$ and~$\psi \Rightarrow \chi$. We have to justify the translated proof
scheme: In order to prove~$(\varphi \vee \psi)^\Box \Rightarrow \chi^\Box$, it
suffices to give proofs of~$\varphi^\Box \Rightarrow \chi^\Box$ and~$\psi^\Box
\Rightarrow \chi^\Box$.

So assume that proofs of the two implications are given. Further
assume~$(\varphi \vee \psi)^\Box$, \ie~$\Box(\varphi^\Box \vee \psi^\Box)$.
We want to show~$\chi^\Box$. Since this is a~$\Box$-stable statement, we may
assume that in fact~$\varphi^\Box \vee \psi^\Box$ holds. Then the claim is
obvious by the two given proofs.

The cases for the other rules (see Appendix~\ref{appendix:inference-rules} for
a list) are similar and left to the reader.\end{proof}

\begin{rem}The reader well-versed in formal logic will have noticed that we are
mixing syntax and semantics here. The proper way to state Lemma~\ref{lemma:box-translation-sound} would be
to formally adjoin a box operator to the language of intuitionistic logic,
governed by three inference rules which are modeled on the three axioms for a
modal operator. This formal box operator could then be instantiated by any
concrete modal operator~$\Box : \Omega \to \Omega$.\end{rem}

Soundness of the~$\Box$-translation is important for the following reason.
If~$\varphi$ and~$\varphi'$ are equivalent formulas, we are
accustomed to be able to freely substitute~$\varphi$ by~$\varphi'$ anywhere we
want. Since a modal operator~$\Box$ is semantically defined as a map~$\Omega
\to \Omega$, it is trivially justified that~$\Box\varphi$ and~$\Box\varphi'$
are equivalent: The formulas~$\varphi$ and~$\varphi'$ give rise to the
\emph{same} element~$\{x \? 1 \,|\, \varphi\} = \{x \? 1 \,|\, \varphi'\}$
of~$\Omega$, and therefore their images under~$\Box$ are equal as well.

However, it is \emph{not} clear and in fact wrong in general that the translated formulas~$\varphi^\Box$
and~$(\varphi')^\Box$ are equivalent. This follows only if the soundness
lemma can be applied (two times, once for each direction). We should stress that to apply this
lemma, it is not enough to merely \emph{know} that~$\varphi$ and~$\varphi'$ are
equivalent; instead, there has to be an intuitionistic proof of this
equivalence. This is really a stronger requirement, since an
equivalence~$\varphi \Leftrightarrow \varphi'$ might
hold in a particular model, \ie in the internal language of some particular
topos, without possessing an intuitionistic proof, \ie holding in any topos. We
give an explicit example of this situation below

\begin{lemma}\label{lemma:open-stalk}
Let~$\varphi$ be a formula such that for any subformulas~$\psi$
appearing as antecedents of implications, it holds that~$\psi^\Box \Rightarrow
\Box\psi$. (In particular, this condition is satisfied if there are
no~``$\Rightarrow$'' signs in~$\varphi$ or if~$\varphi$ is a geometric implication.) Then $\Box\varphi \Rightarrow
\varphi^\Box$.\end{lemma}
\begin{proof}We prove this by an induction on the formula structure. All cases
except for~``$\Rightarrow$'' are obvious. For this case, assume~$\Box(\psi
\Rightarrow \chi)$; we are to show that~$(\psi^\Box \Rightarrow \chi^\Box)$.
Since this is a~$\Box$-stable statement, we can in fact assume that~$(\psi
\Rightarrow \chi)$. We then have
\[ \psi^\Box \Longrightarrow \Box\psi \Longrightarrow \Box\chi
\Longrightarrow \chi^\Box, \]
with the first step being by the requirement on antecedents, the second by the
monotonicity of~$\Box$, and the third by the induction hypothesis.
\end{proof}

\begin{lemma}\label{lemma:stalk-open}
Let~$\varphi$ be a geometric formula.
Then $\varphi^\Box \Leftrightarrow \Box\varphi$.\end{lemma}
\begin{proof}The~``$\Leftarrow$'' direction is by Lemma~\ref{lemma:open-stalk}.
The~``$\Rightarrow$'' direction is an induction on the formula structure. By way of example, we verify
the case of~``$\bigvee$''. So assume~$\Box(\bigvee_i \varphi_i^\Box)$; we are
to show that~$\Box(\bigvee_i \varphi_i)$. Since this is a boxed statement, we
may in fact assume~$\bigvee_i \varphi_i^\Box$, so for some index~$j$, it holds
that~$\varphi_j^\Box$. By the induction hypothesis, it follows
that~$\Box\varphi_j$. By~$\varphi_j \Rightarrow \bigvee_i \varphi_i$ and the
monotonicity of~$\Box$, it follows that~$\Box(\bigvee_i \varphi_i)$.
\end{proof}

An analogous argument for infinite conjunctions is not valid:
Assume~$(\bigwedge_i \varphi_i)^\Box$. So for all~$j$,~$\varphi_j^\Box$ holds.
By the induction hypothesis,~$\Box\varphi_j$ holds for any~$j$. But from this
we may not deduce~$\Box\bigwedge_i \varphi_i$, since the axioms for a modal
operator only require commutativity with finite conjunctions. This failure also
has a geometric interpretation, for instance in the special case~$\Box =
\neg\neg$: Given dense open subsets~$U_i$ on which formulas~$\varphi_i$ hold,
we may not conclude that there exists a single dense open subset~$U$ on which
all the formulas~$\varphi_i$ hold.

\begin{rem}In the special case that~$\Box$ is the double negation modality,
Lemma~\ref{lemma:stalk-open} holds with slightly weaker hypotheses: Namely, implications may occur
in~$\varphi$, provided that for their antecedents~$\psi$ it holds that~$\psi
\Rightarrow \psi^\Box$. This is because for the double negation modality,
the formula~$\Box(\psi \Rightarrow \chi)$ is equivalent to~$\psi \Rightarrow
\Box\chi$. (In general, for an arbitrary modality, only the former implies the latter, but not vice versa.) The case
for~``$\Rightarrow$'' in the inductive proof then goes as follows:
Assume~$(\psi \Rightarrow \chi)^\Box$. Then~$\psi \Rightarrow \psi^\Box
\Rightarrow \chi^\Box \Rightarrow \Box\chi$, so~$\Box(\psi \Rightarrow \chi)$.
\end{rem}

\begin{lemma}\label{lemma:stalk-open-with-hypothesis}
Let~$\varphi, \varphi', \psi$ be formulas. Assume that:
\begin{enumerate}
\item The formula $\varphi'$ is geometric. (More generally, it suffices for~$(\varphi')^\Box$
to imply~$\Box\varphi'$.)
\item There is an intuitionistic proof that~$\varphi$
and~$\varphi'$ are equivalent under the (only) hypothesis~$\psi$.
\item Both~$\Box\psi$ and~$\psi^\Box$ hold.
\end{enumerate}
Then $\varphi^\Box \Rightarrow \Box\varphi$.
\end{lemma}
\begin{proof}
Assume~$\varphi^\Box$. Since~$\psi^\Box$, $(\varphi \wedge \psi)^\Box$. Because
the~$\Box$-translation is sound with respect to intuitionistic logic
it follows that~$(\varphi')^\Box$. As~$\varphi'$ is geometric, it follows
that~$\Box\varphi'$. Since~$\Box\psi$ holds, it follows that~$\Box\varphi$.
\end{proof}

\begin{ex}\label{ex:module-zero-geometric}
Let~$M$ be an~$R$-module. The statement that~$M$ is zero is not
geometric: $\varphi \defequiv (\forall x\?M\_ x = 0)$. But if~$M$ is generated by some finite
family~$x_1,\ldots,x_n\?M$, then~$\varphi$ is equivalent to the
statement~$\varphi' \defequiv (x_1 = 0
\wedge \cdots \wedge x_n = 0)$ which is geometric; and there is an
intuitionistic proof of this equivalence. Since no implication signs occur
in~$\psi \defequiv \speak{$M$ is generated by~$x_1,\ldots,x_n$}$, Lemma~\ref{lemma:stalk-open-with-hypothesis} is
applicable and shows that~$\varphi^\Box$ implies~$\Box\varphi$.
This example will gain geometric meaning in
\end{ex}

\begin{lemma}For the modality~$\Box$ defined by~$\Box\varphi \defequiv ((\varphi
\Rightarrow \alpha) \Rightarrow \alpha)$, where~$\alpha$ is a fixed
proposition, the~$\Box$-translation of the law of excluded middle holds.
In particular, this applies to the double negation modality~$\Box = \neg\neg$, where~$\alpha =
\bot$.\end{lemma}
\begin{proof}We are to show that~$(\varphi \vee \neg\varphi)^\Box$, \ie that
\[ ((\varphi^\Box \vee (\varphi^\Box \Rightarrow \alpha)) \Longrightarrow
\alpha) \Longrightarrow \alpha. \]
So assume that the antecedent holds. If~$\varphi^\Box$ holds, then in
particular~$\varphi^\Box \vee (\varphi^\Box \Rightarrow \alpha)$ and thus~$\alpha$
hold. Therefore it follows that~$(\varphi^\Box \Rightarrow \alpha)$. This
implies~$\varphi^\Box \vee (\varphi^\Box \Rightarrow \alpha)$ and
\end{proof}

\subsection{\texorpdfstring{Truth at stalks \vs truth on neighborhoods}{Truth
at stalks vs. truth on neighborhoods}}\label{sect:spreading}
We now state the crucial property of the~$\Box$-translation. Recall
that~``$X_\Box$'' denotes the sublocale of~$X$ induced by~$\Box$
\begin{thm}\label{thm:box-translation-semantically}
Let~$X$ be a topological space. Let~$\Box$ be a modal operator
in~$\Sh(X)$. Let~$\varphi$ be a formula over~$X$. Then
\[ \Sh(X) \models \varphi^\Box \quad\text{iff}\quad
\Sh(X_\Box) \models \varphi, \]
where on the right hand side, all parameters occurring in~$\varphi$ were pulled
back to~$X_\Box$ along the inclusion~$X_\Box \hookrightarrow X$.
\end{thm}
% FUTURE: think about powersets appearing as domains of quantification

We have not yet explicitly stated the Kripke--Joyal semantics for a sheaf topos
over a locale, which~$X_\Box$ is in general. The definition is exactly the same
as in the case for sheaf toposes over a topological space, only that any
mention of ``open sets'' has to be substituted by the more general ``opens''
and any mention of the union operator~``$\bigcup$'' has to be interpreted by
the supremum operator in the frame of opens of the locale. For~$X_\Box$, this
is~$\sup U_i = j(\bigcup_i U_i)$. Before giving a proof of Theorem~\ref{thm:box-translation-semantically}, we want
to discuss some of its consequences.

\begin{cor}\label{cor:spreading}
Let~$X$ be a topological space.
\begin{enumerate}
\item Let~$U \subseteq X$ be an open subset and let~$\Box\varphi \defequiv (U
\Rightarrow \varphi)$. Then
\[ \Sh(X) \models \varphi^\Box \quad\text{iff}\quad \Sh(U) \models \varphi. \]
\item Let~$A \subseteq X$ be a closed subset and let~$\Box\varphi \defequiv
(\varphi \vee A^c)$. Then
\[ \Sh(X) \models \varphi^\Box \quad\text{iff}\quad \Sh(A) \models \varphi. \]
\item Let~$\Box\varphi \defequiv \neg\neg\varphi$. Then
\[ \Sh(X) \models \varphi^\Box \quad\text{iff}\quad \Sh(X_{\neg\neg}) \models \varphi. \]
\item Let~$x \in X$ be a point and let~$\Box\varphi \defequiv ((\varphi
\Rightarrow \notat{x}) \Rightarrow \notat{x})$. Then
\[ \Sh(X) \models \varphi^\Box \quad\text{iff}\quad \text{$\varphi$ holds
at~$x$}. \]
% change text below ("discuss the third case") if numbering of the items changes
\end{enumerate}
\end{cor}
\begin{proof}Combine Theorem~\ref{thm:box-translation-semantically} and

We want to discuss the last case of Corollary~\ref{cor:spreading} in more detail. Let~$x$ be a
point of a topological space~$X$ and let~$\varphi$ be a formula. Let~$\Box$ be
the modal operator given in the corollary. Then~$\varphi$ \emph{holds at~$x$}
if and only if, from the internal perspective of~$\Sh(X)$, the translated
formula~$\varphi^\Box$ holds; and~$\varphi$ \emph{holds on some open
neighborhood of~$x$} if and only if, from the internal perspective, the
formula~$\Box\varphi$ holds.

Thus the question whether the truth of~$\varphi$ at the point~$x$ spreads to
some open neighborhood can be formulated in the following way:
\begin{quote}
\emph{Does~$\varphi^\Box$ imply~$\Box\varphi$ in the internal language
\end{quote}
Phrased this way, technicalities like appropriately shrinking open
neighborhoods are blinded out. A purposefully trivial example to illustrate
this is the following. Let~$X$ be a scheme (or a ringed space). Let~$f,g \in
\Gamma(X,\O_X)$ be global functions. Suppose that the germs of~$f$ and~$g$ are
zero in some stalk~$\O_{X,x}$; we want to show that they are zero on a common
open neighborhood of~$x$.

\begin{proof}[Usual proof]Since the germ of~$f$ vanishes in~$\O_{X,x}$, there
is an open neighborhood~$U_1$ of~$x$ such that~$f|_{U_1} = 0$
in~$\Gamma(U_1,\O_X)$. Since furthermore the germ of~$g$ vanishes in the same stalk,
there exists an open neighborhood~$U_2$ of~$x$ such that~$g|_{U_2} = 0$. The
intersection of both neighborhoods is still an open neighborhood of~$x$; on
this neighborhood both~$f$ and~$g$ vanish.
\end{proof}

\begin{proof}[Proof in the internal language]We may suppose that~$(f = 0 \wedge
g = 0)^\Box$, that is $\Box(f=0) \wedge \Box(g=0)$, and have to prove
that~$\Box(f=0 \wedge g=0)$. (To this end, we could simply invoke the third
axiom on a modal operator, but we want to stay close to the given external
proof.) So by assumption, both~$\Box(f=0)$ and~$\Box(g=0)$ hold. Since our goal
is to prove a boxed statement, we may in fact assume that~$f = 0$ and~$g = 0$.
Thus~$f = 0 \wedge g = 0$.\end{proof}

By using the internal language with its modal operators, we can thus reduce
basic facts of scheme theory which deal with stalks and neighborhoods to facts
of algebra in a \emph{modal intuitionistic context}. As with using the internal
language in its basic form without modalities, this brings conceptual clarity
and reduced technical overhead. There are, however, two more distinctive
advantages. Firstly, many internal proofs do not require specific properties of
the modal operator and thus work with any modal operator. By interpreting such
a proof using different operators, one obtains an entire family of external
statements without any additional work (see
Lemma~\ref{lemma:module-zero-point-neighbourhood} for an example).

Secondly, the following corollary gives a general metatheorem which is
applicable to a wide range of cases. It allows to decide whether spreading will
occur (or is likely not to occur) simply by looking at the \emph{logical form}
of the statement in question.

\begin{cor}\label{cor:geometric-spreading}
Let~$X$ be a topological space. Let~$\varphi$ be a formula.
If~$\varphi$ is geometric, truth of~$\varphi$ at a point~$x \in X$ implies
truth of~$\varphi$ on some open neighborhood of~$x$, and vice versa.\end{cor}
\begin{proof}By the purely logical lemmas of Section~\ref{sect:box-translation}, it holds
that~$\varphi^\Box \Leftrightarrow \Box\varphi$.
\end{proof}

\begin{cor}
Let~$X$ be a topological space. Let~$\varphi$ be a formula.
If~$\varphi$ is geometric, the property ``$\varphi$ holds at a point~$x \in
X$'' is open.
\end{cor}
\begin{proof}This is just a reformulation of the previous corollary:
If~$\varphi$ holds at a point~$x \in X$, it holds on some open
neighborhood~$U$ of~$x$ as well. Going back to stalks, it follows
that~$\varphi$ holds at every point of~$U$.\end{proof}

\begin{ex}Let~$X$ be a scheme (or a ringed space). Since the condition for a
function~$f\?\O_X$ to be nilpotent is geometric (it is~$\bigvee_{n \geq 0} f^n
= 0$), nilpotency of~$f$ at a point is equivalent to nilpotency on some open

Combined with Lemma~\ref{lemma:stalk-open-with-hypothesis}, this metatheorem is
quite useful. We will illustrate it with several examples in the next subsection.

An important special case of spreading from stalks to neighborhoods is the
case of spreading from the generic point (should it exist) to a dense open
subset. Whether this occurs can be phrased by
Lemma~\ref{lemma:negneg-generic-point} as follows:
\begin{quote}
\emph{Does~$\varphi^{\neg\neg}$ imply~$\neg\neg\varphi$ in the internal language
\end{quote}
This question is a question of ordinary (non-modal) intuitionistic algebra.

\begin{ex}We have seen in Remark~\ref{rem:epi-in-box-sheaves} that a
morphism~$f : A \to B$ in~$\Sh(X_\Box) \simeq \Sh_\Box(\Sh(X))$ is an
epimorphism if and only if \[ \Sh(X) \models \forall y\?B\_ \Box(\exists x\?X\_
f(x) = y). \] We can now understand a simple proof of this fact:
\begin{align*}
&\ \text{$f$ is an epimorphism in~$\Sh_\Box(\Sh(X))$} \\
\Longleftrightarrow&\
\Sh_\Box(\Sh(X)) \models \speak{$f$ is surjective} \\
\Longleftrightarrow&\
\Sh(X) \models \left(\speak{$f$ is surjective}\right)^\Box \\
\Longleftrightarrow&\
\Sh(X) \models \forall y\?B\_ \Box(\exists x\?X\_ \Box(f(x) = y)) \\
\Longleftrightarrow&\
\Sh(X) \models \forall y\?B\_ \Box(\exists x\?X\_ f(x) = y).
\end{align*}
The ultimate equivalence is by Lemma~\ref{lemma:stalk-open}, applied to the
geometric subformula~``$\exists x\?X\_ f(x) = y$''.
\end{ex}

\begin{rem}Theorem~\ref{thm:box-translation-semantically} can also be motivated
by purely logical considerations. Namely, one can check that interpreting a
formula~$\varphi$ by $\Sh(X) \models \varphi^\Box$ gives rise to a model of
intuitionistic logic -- if~$\varphi$ intuitionistically implies~$\psi$,
then~$\Sh(X) \models \varphi^\Box$ implies~$\Sh(X) \models \psi^\Box$.
It is therefore a natural question whether there exists a
topos~$\E$ such that~$\E \models \varphi$ if and only if~$\Sh(X) \models
\varphi^\Box$. Theorem~\ref{thm:box-translation-semantically} gives an
affirmative answer to this question, explicitly stating that~$\E \defeq
\Sh(X_\Box)$ is such a topos.\end{rem}

\begin{proof}[Proof of Theorem~\ref{thm:box-translation-semantically}]
A fancy proof goes as follows. First, one shows intuitionistically that for a
modal operator~$\Box$ in~$\Set$, it holds that
\[ \Set \models \varphi^\Box \quad\Longleftrightarrow\quad
\Sh_\Box(\Set) \models \varphi. \]
This can be verified by induction on the structure of
formulas~$\varphi$. Then one interprets this result in the sheaf topos~$\Sh(X)$:
\begin{align*}
&\ \Sh(X) \models \varphi^\Box \\
\Longleftrightarrow&\
\Sh(X) \models \speak{$\Set \models \varphi^\Box$} &&\text{by idempotency}\\
\Longleftrightarrow&\
\Sh(X) \models \speak{$\Sh_\Box(\Set) \models \varphi$} &&\text{by the first step} \\
\Longleftrightarrow&\
\Sh_\Box(\Sh(X)) \models \varphi &&\text{by idempotency} \\
\Longleftrightarrow&\
\Sh(X_\Box) \models \varphi &&\text{since~$\Sh_\Box(\Sh(X)) \simeq
\Sh(X_\Box)$}
\end{align*}
By \emph{idempotency}, we mean that internally employing the Kripke--Joyal
semantics to interpret doubly-internal statements is the same as using the
Kripke--Joyal semantics once. However, we do not want to discuss this here any further;
some details can be found in the original article on the stack
semantics~\cite[Lemma~7.20]{shulman:stack}, but the statement given there is not
general enough to justify the second use of idempotency above. For this, one
would have to extend the stack semantics to support internal statements about
locally internal categories like~$\Sh(X_\Box) \hookrightarrow \Sh(X)$ (which
then look like locally small categories from the internal point of view). This
is worthwhile for other reasons too, but shall not be pursued here.

Therefore, we give a more explicit proof. By induction, we are going to prove
that for any open subset~$U \subseteq X$ and any formula~$\varphi$ over~$U$, it
holds that
\[ U \models_X \varphi^\Box \quad\Longleftrightarrow\quad j(U) \models_{X_\Box}
\varphi, \]
where the internal statements are to be interpreted by the Kripke--Joyal
semantics of~$X$ and~$X_\Box$ respectively and~$j$ is the nucleus associated
to~$\Box$. We may assume that any sheaves occurring in~$\varphi$ as domains of
quantifications are in fact~$\Box$-sheaves; we justify this with a separate lemma

The cases~$\varphi \equiv \top$,~$\varphi \equiv (\psi \wedge \chi)$,
and~$\varphi \equiv \bigwedge_i \psi_i$ are trivial. For~$\varphi \equiv \bot$,
the claim is that~$U \models_X \Box\bot$ if and only if~$j(U)
\models_{X_\Box} \bot$. The former means~$U \subseteq j(\emptyset)$ and the
latter means~$j(U) \leq \sup \emptyset = j(\emptyset)$, so the claim follows from
the first two axioms for a nucleus.

We omit the verification of the remaining cases.
\end{proof}

\begin{lemma}Let~$\Box$ be a modal operator. Let~$\varphi$ be a formula.
Let~$\psi \defequiv \varphi^\Box$ be the~$\Box$-translation of~$\varphi$.
Let~$\psi'$ be the formula obtained from~$\psi$ by substituting any occurring
domain of quantification by its~$\Box$-sheafification, as syntactically defined
in Definition~\ref{defn:plus-construction}. Then~$\psi$
and~$\psi'$ are intuitionistically equivalent.
\end{lemma}
\begin{proof}
For any formula~$\varphi$, we denote by~``$\varphi^\boxplus$'' the result of
first applying the~$\Box$-translation to~$\varphi$ and then substituting any
set~$F$ occurring in~$\varphi$ as a domain of quantification by the plus
construction~$F^+$. Recall that for any such~$F$ there is a canonical map~$F
\to F^+,\ x \mapsto [\{x\}]$. We are going to show by induction that for any
formula~$\varphi(x_1,\ldots,x_n)$ in which elements~$x_i\?F_i$ may occur as
terms, it holds that~$\varphi^\Box(x_1,\ldots,x_n)$ is equivalent
to~$\varphi^\boxplus([\{x_1\}],\ldots,[\{x_n\}])$. This suffices to prove the

The cases for
\[ \top \quad \bot \quad \wedge \quad \bigwedge \quad \vee \quad \bigvee \quad \implies \]
are trivial. The cases for unbounded~``$\forall$'' and~``$\exists$'' are
trivial as well. The case for~``$=$'' is slightly more interesting; let~$\varphi(x,y)
\equiv (x = y)$. Then we are to show that~$\varphi^\Box(x,y) \equiv \Box(x=y)$
(equality in some set~$F$) is equivalent to~$\varphi^\boxplus([\{x\}],[\{y\}])
\equiv \Box([\{x\}] = [\{y\}])$ (equality in~$F^+$). This follows by the
definition of the plus construction. The case for~``$\in$'' is similar.

Let~$\varphi \equiv (\exists x\?F\_ \psi(x))$, where we have dropped further
variables occurring in~$\psi$ for simplicity. Then we are to show
that~$\varphi^\Box \equiv \Box(\exists x\?F\_ \psi^\Box(x))$ is equivalent
to~$\varphi^\boxplus \equiv \Box(\exists \bar x\?F^+\_ \psi^\boxplus(\bar x))$.
The ``only if'' direction is trivial (set~$\bar x \defeq [\{x\}]$). For the ``if''
direction, we may assume that there exists~$\bar x\?F^+$ such
that~$\psi^\boxplus(\bar x)$, since we want to prove a boxed statement. By
definition of the plus construction, it holds that~$\Box(\speak{$\bar x$ is a
singleton})$. So, again since we want to prove a boxed statement, we may assume
that~$\bar x$ is actually a singleton. Therefore there exists~$x\?F$ such
that~$\bar x = [\{x\}]$ and that~$\psi^\boxplus([\{x\}])$ holds. By the induction
hypothesis, it follows that~$\psi^\Box(x)$. From this the claim follows.

The case for~``$\forall$'' is similar.
\end{proof}

\begin{ex}\label{ex:translation-equivalence}Let~$X$ be a scheme. Let~$f$ be a
global function on~$X$. Let~$\varphi \defequiv \neg(\speak{$f$ \inv})$
and~$\varphi' \defequiv \speak{$f$ nilpotent}$. Then, by Proposition~\ref{prop:cond-zero}, we
have~$\Sh(X) \models (\varphi \Leftrightarrow \varphi')$. But in general, this
does not imply that~$\Sh(X) \models (\varphi^\Box \Leftrightarrow
(\varphi')^\Box)$. Consider for instance the modal operator given by~$\Box\alpha
\defequiv ((\alpha \Rightarrow \notat{x}) \Rightarrow \notat{x})$ associated to a
point~$x \in X$. Then~$\Sh(X) \models (\varphi^\Box \Leftrightarrow
(\varphi')^\Box)$ means that the equivalence~$\varphi \Leftrightarrow \varphi'$
holds at the point~$x$. This is false for~$X = \Spec \ZZ$,~$f = 2$, and~$x =
(2)$, since in the local ring~$\O_{X,x} = \ZZ_{(2)}$, the element $f$ is not invertible
while also not being nilpotent.
\end{ex}
% Adapt rem:closed-geometric-morphism in case the example changes.

\subsection{Internal proofs of common lemmas}

\begin{lemma}\label{lemma:module-zero-point-neighbourhood}
Let~$X$ be a scheme (or a ringed space). Let~$\F$ be an~$\O_X$-module
of finite type.
\begin{enumerate}
\item Let~$x \in X$ be a point. Then the stalk~$\F_x$ is zero if and
only if~$\F$ is zero on some open neighborhood of~$x$.
\item Let~$A \subseteq X$ be a closed subset. Then the restriction~$\F|_A$ (\ie
the pullback of~$\F$ to~$A$) is zero if and only if~$\F$ is zero on some open
subset of~$X$ containing~$A$.
\end{enumerate}
\end{lemma}
\begin{proof}\emph{Both} statements are simply internalizations of
Example~\ref{ex:module-zero-geometric}, using the modal operators~$\Box =
(\placeholder \vee A^c)$ and~$\Box = ((\placeholder \Rightarrow
\notat{x}) \Rightarrow \notat{x})$.
\end{proof}

\begin{rem}Lemma~\ref{lemma:module-zero-point-neighbourhood} fails if one drops the hypothesis
that~$\F$ is of finite type. Indeed, in this case one cannot reformulate the
condition that~$\F$ is zero in a geometric way.\end{rem}

In a remark after the proof of Proposition~\ref{prop:rank-function-internally},
we promised to present a simpler proof of it once we would have developed the theory for
doing so. We can now follow up on this promise.
\begin{lemma}\label{lemma:gen-family-n}
Let~$X$ be a scheme (or a ringed space). Let~$\F$ be an~$\O_X$-module
of finite type. Let~$x \in X$ be a point. Let~$n$ be a natural number. Then the
following statements are equivalent:
\begin{enumerate}
\item There exists a generating family for~$\F_x$ consisting of~$n$ elements.
\item There exists an open neighborhood~$U$ of~$x$ such that
\[ U \models \speak{there exists a generating family for~$\F$ consisting of~$n$
elements}. \]
\end{enumerate}
\end{lemma}
\begin{proof}Using the modal operator~$\Box$ defined by~$\Box\varphi \defequiv
((\varphi \Rightarrow \notat{x}) \Rightarrow \notat{x})$, we have to show that
the following statements in the internal language are equivalent:
\begin{enumerate}
\item $\speak{there exists a generating family
for~$\F$ consisting of~$n$ elements}^\Box$.
\item $\Box(\speak{there exists a generating family
for~$\F$ consisting of~$n$ elements})$.
\end{enumerate}
By Lemma~\ref{lemma:open-stalk}, the second statement implies the first, since
in a formal spelling of the statement in quotes,
\begin{equation}\label{eqn:finitely-generated}\tag{$\star$}
\exists x_1,\ldots,x_n\?\F\_
\forall x\?\F\_
\exists a_1,\ldots,a_n\?\O_X\_
x = \textstyle\sum_i a_i x_i,
\end{equation}
no implication signs occur. To show the converse direction,
we may assume that there is a generating family~$y_1,\ldots,y_m\?\F$ for~$\F$
(since~$\F$ is, externally speaking, of finite type). Then
the~$\Box$-translation of the statement that the~$y_i$ generate~$\F$ holds as
well (again by Lemma~\ref{lemma:open-stalk}). Since there is an intuitionistic
proof of
\begin{multline*}
\speak{$y_1,\ldots,y_m$ generate~$\F$} \Longrightarrow \\
\bigl(\speak{there exist $x_1,\ldots,x_n\?\F$ which generate~$\F$}
\Longleftrightarrow \\
\exists x_1,\ldots,x_n\?\F\_
\exists A\?\O^{m \times n}\_ \speak{$\vec y = A \vec x$}\bigr),
\end{multline*}
Lemma~\ref{lemma:stalk-open-with-hypothesis} can substitute the non-geometric formula~\eqref{eqn:finitely-generated} by the geometric
\[ \exists x_1,\ldots,x_n\?\F\_ \exists A\?\O^{m \times n}\_ \speak{$\vec
y = A \vec x$} \]
(Lemma~\ref{lemma:stalk-open-with-hypothesis}). Thus the claim follows.
\end{proof}

\begin{lemma}Let~$X$ be a scheme (or a ringed space). Let~$\alpha : \F \to \G$ be
a morphism of~$\O_X$-modules. Let~$\G$ be of finite type and assume
that~$\alpha_x : \F_x \to \G_x$ is surjective for some point~$x \in X$.
Then~$\alpha$ is an epimorphism on some open neighborhood of~$x$.\end{lemma}
\begin{proof}In the presence of generators~$y_1,\ldots,y_n\?\G$, the
non-geometric surjectivity condition ($\forall y\?\G\_ \exists x\?\F\_
\alpha(x) = y$) can be reformulated in a geometric way: $\bigwedge_{i=1}^n
\exists x\?\F\_ \alpha(x) = y_i$. Thus the claim follows by

%\begin{lemma}Let~$X$ be a scheme (or a ringed space). Let~$\alpha : \F \to \G$ be
%a morphism of~$\O_X$-modules. Let~$\F$ be of finite type and~$\G$ be coherent.
%Suppose that~$\alpha_x$ is injective at some point~$x \in X$. Then~$\alpha$ is
%a monomorphism on some open neighbourhood of~$x$.
%\begin{proof}The kernel of~$\alpha$ is of finite type (by
%Lemma~\ref{lemma:coherent-stuff}) and zero at~$x$. By the previous lemma, it is
%therefore zero on some open neighbourhood of~$x$.
%This proof is precisely the classical one, so there is no need to include it here.

\begin{lemma}\label{lemma:pushforward-finite-type}
Let~$i : A \hookrightarrow X$ be a closed immersion of schemes (or
ringed spaces). Let~$\F$ be an~$\O_A$-module. Then~$i_*\F$ is of finite type if
and only if~$\F$ is of finite type.\end{lemma}
\begin{proof}
Let~$\Box$ be the modal operator defined by~$\Box\varphi \defequiv (\varphi \vee
A^c)$. From the internal perspective, we have a surjective ring homomorphism~$i^\sharp
: \O_X \to \O_A$, where we omit the forgetful functor~$i_*$ from~$\Box$-sheaves
to arbitrary sets in the notation, and an~$\O_A$-module~$\F$. Furthermore, we
may assume that~$\F$ is a~$\Box$-sheaf. We can regard~$\F$ as an~$\O_X$-module

Note that~$A^c \Rightarrow (\F = 0)$, by~$\Box$-separatedness of~$\F$.

We are to show that~$\F$ is a finitely generated~$\O_X$-module if and only if
the~$\Box$-translation of ``$\F$ is a finitely generated~$\O_A$-module'' holds.
In explicit terms, we have to show the equivalence of the following statements:
\begin{enumerate}
\item $\bigvee_{n \geq 0} \exists x_1,\ldots,x_n\?\F\_
\forall x\?\F\_ \exists a_1,\ldots,a_n\?\O_X\_ x = \sum_i i^\sharp(a_i) x_i$.
\item $\Box(\bigvee_{n \geq 0} \Box(\exists x_1,\ldots,x_n\?\F\_
\forall x\?\F\_ \Box(\exists b_1,\ldots,b_n\?\O_A\_ \Box(
x = \sum_i b_i x_i))))$.
\end{enumerate}
It is clear that the first statement implies the second. For the converse
direction, we just have to repeatedly use the observation that~$\Box\varphi$
implies~$\varphi \vee (\F = 0)$ (once for each occurrence of~$\Box$). So in each
step, we either obtain the statement we want or may assume
that~$\F$ is the trivial module, in which case any subclaim trivially follows. By
surjectivity of~$i^\sharp$, we may write any~$b\?\O_A$ as~$b =
i^\sharp(a)$ for some~$a\?\O_X$.
\end{proof}

\begin{lemma}\label{lemma:fp-hom-geometric}
Let~$X$ be a scheme (or a ringed space). Let~$\F$ and~$\G$ be~$\O_X$-modules. Let~$x
\in X$. Then $\HOM_{\O_X}(\F,\G)_x \cong \Hom_{\O_{X,x}}(\F_x,\G_x)$ if~$\F$ is
of finite presentation around~$x$.\end{lemma}
\begin{proof}It suffices to give an intuitionistic proof of the following fact:
The construction~$\Hom_R(M,\placeholder)$ is geometric if~$M$ is a finitely
presented~$R$-module. So assume that~$M$ is the cokernel of a presentation
matrix~$(a_{ij}) \? R^{n \times m}$. Then we can describe the Hom with
any~$R$-module~$N$ as
\[ \Hom_R(M,N) \cong \Bigl\{ x \? N^n \ \Big|\ \bigwedge_{j=1}^m \sum_{i=1}^n a_{ij}
x_i = 0 \? N \Bigr\}, \]
and this construction is patently geometric, as a set comprehension with respect to
a geometric formula.
\end{proof}

\begin{lemma}Let~$X$ be a scheme (or a ringed space). Let~$\F$ be an~$\O_X$-module of finite
presentation. Let~$x \in X$. Then the stalk~$\F_x$ is a finite
free~$\O_{X,x}$-module if and only if~$\F$ is finite locally free on some open
neighborhood of~$x$.\end{lemma}
\begin{proof}The internal statement that~$\F$ is a finite free module is not geometric:
\[ \bigvee_{n \geq 0}
\exists x_1,\ldots,x_n\?\F\_
\forall x\?\F\_
\exists! a_1,\ldots,a_n\?\O_X\_
x = \textstyle\sum_i a_i x_i. \]
But it can equivalently be reformulated as
\[ \bigvee_{n \geq 0}
\exists \alpha\?\HOM_{\O_X}(\F,\O_X^n)\_
\exists \beta\?\HOM_{\O_X}(\O_X^n,\F)\_
\alpha \circ \beta = \id \wedge \beta \circ \alpha = \id. \]
This reformulation is geometric, therefore it holds at~$x$ if and only if it
holds on some open neighborhood of~$x$. The claim follows since, by the
previous proposition, taking stalks commutes with
calculating~$\HOM_{\O_X}(\F,\placeholder)$ \resp~$\HOM_{\O_X}(\O_X^n,\placeholder)$;
thus the pulled back formula indeed expresses that~$\F_x$ is finite free as
\end{proof}

\begin{lemma}\label{lemma:torsion-module-generic-stalk}
Let~$X$ be an integral scheme with generic point~$\xi$. Let~$\F$
be a quasicoherent~$\O_X$-module. Then~$\F$ is a torsion module if and only if
its generic stalk~$\F_\xi$ vanishes.
\end{lemma}
\begin{proof}The generic stalk vanishes if and only if the internal
statement~``$(\F = 0)^{\neg\neg}$'' holds. Therefore it suffices to give an
intuitionistic proof of the following internal statement: The module~$\F$ is
torsion if and only if any element of~$\F$ is \notnot zero.

For the ``only if'' direction, let~$x\?\F$ be an arbitrary element. Since~$\F$
is a torsion module, there exists a regular element~$a\?\O_X$ such that~$ax =
0$. Since~$X$ is reduced, regularity is equivalent to not-not-invertibility.
Since we want to verify the~$\neg\neg$-stable statement~``$\neg\neg(x = 0)$'', we
may in fact assume that~$a$ is invertible. Then~$x = 0$ obviously follows.

For the ``if'' direction, let~$x\?\F$ be an arbitrary element; by assumption,~$x$
is \notnot zero. Since~$X$ is integral,
Lemma~\ref{lemma:dense-standard-reflection} is applicable. Therefore there
exists an element~$a\?\O_X$ such that~$a$ is \notnot invertible and such that
invertibility of~$a$ implies~$x = 0$. Since~$\F$ is quasicoherent, for some
natural number~$n$ it holds that~$a^n x = 0$ (Theorem~\ref{thm:qcoh-sheafchar}
below). Since~$a$ is \notnot invertible,
it is regular (see Lemma~\ref{lemma:regular-notnot-invertible} below for a short
and self-contained proof), and therefore~$a^n$ is regular. So~$x \in \F_\tors$.
\end{proof}

By simply using a different modal operator than~``\notnot'', we will -- without
any additional work -- obtain a more general form of this lemma, applicable to
non-integral schemes (see Lemma~\ref{lemma:torsion-module-generic-stalk-generalized}).

\section{Compactness and metaproperties}
\label{sect:compactness}

\subsection{Quasicompactness}

As stated in the introduction, quasicompactness of a space cannot be detected
by the internal language: There cannot exist a formula~$\varphi$ such that a
topological space is quasicompact if and only if~$\Sh(X) \models \varphi$,
since the latter is always a local property on~$X$ while quasicompactness is not.
However, quasicompactness can be characterized by a \emph{metaproperty} of the
internal language.

This result is best stated in a way which does not explicitly refer to a notion
of finiteness. So recall that quasicompactness of a topological space~$X$ can
be phrased in the following way: For any directed set~$I$ and any monotone
family~$(U_i)_{i \in I}$ of open subsets, if~$X = \bigcup_i U_i$ then~$X = U_i$
for some~$i \in I$. As usual, a \emph{directed set} is an inhabited partially
ordered set such that for any two elements there exists a common upper bound.
A family~$(U_i)_{i \in I}$ is \emph{monotone} if and only if~$i \preceq j$
implies~$U_i \subseteq U_j$.

\begin{prop}\label{prop:quasicompact-meta}
Let~$X$ be a topological space. Then~$X$ is quasicompact if and
only if the internal language of~$\Sh(X)$ has the following metaproperty:
For any directed set~$I$ and any monotone family~$(\varphi_i)_{i \in I}$ of
formulas over~$X$,
\[ \Sh(X) \models \bigvee_{i \in I} \varphi_i
\quad\text{implies}\quad
\text{for some~$i \in I$, $\Sh(X) \models \varphi_i$}. \]
The monotonicity condition means that~$\Sh(X) \models (\varphi_i \Rightarrow
\varphi_j)$ for any~$i \preceq j$ in~$I$.
\end{prop}

Stated more succinctly, a topological space~$X$ is quasicompact if and only
if~``$\Sh(X) \models$'' commutes with directed~``$\bigvee_{i \in I}$'''s.

\begin{proof}For the ``only if'' direction, let such a family of formulas be
given. Declare~$U_i$ to be the largest open subset of~$X$ where~$\varphi_i$
holds. Then by assumption, the sets~$U_i$ form a monotone family and cover~$X$. By
quasicompactness of~$X$, some single member~$U_i$ covers~$X$ as well, whereby the
corresponding formula~$\varphi_i$ holds on~$X$.

For the ``if'' direction, we observe that a monotone family~$(U_i)$ of open subsets
induces a monotone family of formulas by defining~$\varphi_i \defequiv U_i$,
employing the notational convention set out in
Section~\ref{sect:modalities-geometric-meaning}. This
correspondence is such that~$\Sh(X) \models \bigvee_i \varphi_i$ holds if and
only if~$X = \bigcup_i U_i$ and such that~$\Sh(X) \models \varphi_i$ if and
only if~$X = U_i$. With these observations the claim is obvious.
\end{proof}

\begin{ex}\label{ex:nilpotency-directed}
Let~$X$ be a quasicompact scheme (or quasicompact ringed space).
Let~$f \in \Gamma(X,\O_X)$ be a global function. Let the set of natural
numbers be endowed with the usual ordering. Then the family of formulas given by~$(f^n =
0)_{n \in \NN}$ is monotone. Thus, if it internally holds that~$f$ is
nilpotent, then~$f$ is nilpotent as an element of~$\Gamma(X,\O_X)$ as

\begin{prop}\label{prop:locally-qc}
Let~$X$ be a topological space. Let~$K \subseteq X$ be an open
subset which is \emph{locally quasicompact} in the sense that there exists an open
covering~$X = \bigcup_j U_j$ such that each~$K \cap U_j$ is quasicompact. Then the
internal language of~$\Sh(X)$ has the following metaproperty: For any
directed set~$I$ and any monotone family~$(\varphi_i)_{i \in I}$ of formulas
over~$X$ it holds that
\[ \Sh(X) \models \bigl(K \Rightarrow \bigvee_i \varphi_i\bigr)
\quad\text{implies}\quad
\Sh(X) \models \bigvee_i (K \Rightarrow \varphi_i). \]
If additionally for any open subset~$V \subseteq X$ the set~$K \cap V$ is
locally quasicompact in~$V\!$, the following stronger and purely internal
statement holds:
\[ \Sh(X) \models \bigl(K \Rightarrow \bigvee_i \varphi_i\bigr)
\Longrightarrow
\bigvee_i (K \Rightarrow \varphi_i). \]
\end{prop}
\begin{proof}Assume that~$\Sh(X) \models (K \Rightarrow \bigvee_i \varphi_i)$.
This is equivalent to~$K \models \bigvee_i \varphi_i$. By the locality of the
internal language, it follows that~$K \cap U_j \models \bigvee_i \varphi_i$ for each~$j$.
Since~$K \cap U_j$ is quasicompact, it follows by Proposition~\ref{prop:quasicompact-meta} that
there exists an index~$i_j \in I$ such that~$K \cap U_j \models \varphi_{i_j}$.
This is equivalent to~$U_j \models (K \Rightarrow \varphi_{i_j})$. In
particular, it holds that~$U_j \models \bigvee_i (K \Rightarrow \varphi_i)$.
Since this is true for any~$j$, it follows that~$X \models \bigvee_i (K
\Rightarrow \varphi_i)$, again by the locality of the internal language.

The second statement is a corollary of the first one.
\end{proof}

\begin{ex}Any retrocompact subset of a scheme is locally quasicompact in the
sense of Proposition~\ref{prop:locally-qc}.\end{ex}

\begin{ex}\label{ex:df-locally-compact}
Let~$X$ be a scheme and~$f \in \Gamma(X,\O_X)$ be a global function.
Then the open set~$D(f) = \{ x \in X \,|\, \text{$f_x$ is invertible in~$\O_{X,x}$}
\}$ is locally quasicompact in the sense of Proposition~\ref{prop:locally-qc}, even in the
stronger sense: Let~$V \subseteq X$ be any open set. Consider a covering~$V = \bigcup_i
U_i$ by open affine subsets~$U_i = \Spec A_i$. Then~$D(f) \cap U_i \cong \Spec
A_i[f^{-1}]$ is quasicompact.\end{ex}

From this example it will trivially follow that the nilradical~$\sqrt{(0)}
\subseteq \O_X$ of a scheme and indeed the radical of any quasicoherent
sheaf of ideals is quasicoherent (Example~\ref{ex:radical-qcoh}). This example is also
pivotal for giving a simple description of the quasicoherator
(Proposition~\ref{prop:quasicoherator-arbitrary-algebra}), which in turn is
needed for an internal understanding of the relative
spectrum (Section~\ref{sect:relative-spectrum}).

\begin{rem}In applications, the open set~$K$ of Proposition~\ref{prop:locally-qc} is often given
as the largest open subset on which some formula~$\psi$ holds. (For instance,
in Example~\ref{ex:df-locally-compact},~$K$ was given by the formula~$\speak{$f$
is invertible in $\O_X$}$.)
Then the conclusion of the proposition is that \emph{assuming that~$\psi$ holds commutes
with directed disjunctions}.\end{rem}

\subsection{Locality}

A stronger condition on a topological space~$X$ than quasicompactness is
locality: A topological space is \emph{local} if and only if for any open
covering~$X = \bigcup_i U_i$ (not necessarily directed) a certain single subset~$U_i$
covers~$X$ as well. For instance, the spectrum of a ring~$A$ is local if and only
if~$A$ is a local ring. Locality has the following characterization as a metaproperty

\begin{prop}\label{prop:local-meta}Let~$X$ be a topological space. Then~$X$ is local if and
only if the internal language of~$\Sh(X)$ has the following metaproperty:
For any set~$I$ and any family~$(\varphi_i)_{i \in I}$ of
formulas over~$X$, it holds that
\[ \Sh(X) \models \bigvee_{i \in I} \varphi_i
\quad\text{implies}\quad
\text{for some~$i \in I$, $\Sh(X) \models \varphi_i$}. \]
In this case, the internal language has additionally the following (weaker) metaproperty: For any
sheaf~$\F$ on~$X$ and any formula~$\varphi(s)$ containing a variable~$s\?\F$,
it holds that
\[ \Sh(X) \models \exists s\?\F\_ \varphi(s)
\quad\text{implies}\quad
\text{for some~$s \in \Gamma(X,\F)$, $\Sh(X) \models \varphi(s)$}. \]
\end{prop}
\begin{proof}The proof of the first part is very similar to the proof of
Proposition~\ref{prop:locally-qc}. For the ``only if'' direction of the second part, note
that the antecedent implies that there exist local sections~$s_i \in
\Gamma(U_i,\F)$ such that~$U_i \models \varphi(s_i)$ for some open covering~$X
= \bigcup_i U_i$. By locality of~$X$, one such~$U_i$ suffices to cover~$X$; so
the corresponding section~$s_i$ is actually a global section and verifies~$X
\models \varphi(s_i)$.
\end{proof}

\begin{rem}The second metaproperty stated in the proposition is indeed weaker
than the condition that~$X$ is local. For instance, let~$X$ be a space consisting
of two discrete points. Then~$\Sh(X)$ has the second metaproperty, but~$X$ is
not local.\end{rem}

\subsection{Irreducibility}

In intuitionistic logic, De Morgan's law~$\neg(\alpha \wedge \beta)
\Rightarrow \neg\alpha \vee \neg\beta$ is not generally justified; therefore we
can't use it when working internally to the topos of sheaves on a general scheme~$X$.
The following proposition demonstrates that if~$X$ is irreducible, the law
does hold.

\begin{prop}\label{prop:irreducibility-internally}
A topological space~$X$ is irreducible if and only if the internal
language of~$\Sh(X)$ has the following metaproperty: For any
formulas~$\varphi$ and~$\psi$
\[ \Sh(X) \models \neg(\varphi \wedge \psi)
\quad\text{implies}\quad
\Sh(X) \models \neg\varphi \text{ or }
\Sh(X) \models \neg\psi, \]
and not $\Sh(X) \models \bot$.
Furthermore, in this case the following internal logical principle holds:
\[ \Sh(X) \models \forall \alpha,\beta \? \Omega\_
\neg(\alpha \wedge \beta) \Rightarrow (\neg\alpha \vee \neg\beta). \]
\end{prop}
\begin{proof}The statement ``$\Sh(X) \models \neg(\varphi \wedge \psi)$'' means
that~$U \cap V = \emptyset$, where~$U$ and~$V$ are the largest open subsets on
which~$\varphi$ respectively~$\psi$ hold. The disjunction ``$\Sh(X) \models
\neg\varphi$ or $\Sh(X) \models \neg\psi$'' means that~$U = \emptyset$ or~$V =
\emptyset$. And ``$\Sh(X) \models \bot$'' is equivalent to~$X = \emptyset$.

Therefore, if~$X$ is irreducible, then the internal language has the claimed metaproperty. The converse
can be seen by instantiating~$\varphi$ and~$\psi$ with the formulas associated
to given open subsets having empty intersection. It then follows that one of
these formulas is false in the internal language; thus the associated subset is

The stated internal logical principle holds since nonempty open subsets of irreducible spaces are
\end{proof}

\subsection{Internal proofs of common lemmas}

\begin{lemma}Let~$X$ be an irreducible reduced scheme. Then all local
rings~$\O_{X,x}$ are integral domains.\end{lemma}
\begin{proof}It suffices to give a proof of the following statement: Let~$R$ be
a local ring such that elements which are not invertible are nilpotent. Furthermore
assume that~$R$ is reduced. Then~$R$ is an integral domain in the weak sense of

This proof may, additionally to the rules of intuitionistic logic, use the
classical axiom stated in Proposition~\ref{prop:irreducibility-internally}.

So let arbitrary elements~$x,y \? R$ with~$xy = 0$ be given. Then it is not the
case that~$x$ and~$y$ are both invertible: If they were, their product~$xy$
would be invertible as well, contradicting~$1 \neq 0$. By the classicality
principle, it follows that~$x$ is not invertible or that~$y$ is not invertible.
Thus~$x$ or~$y$ is nilpotent and therefore zero.
\end{proof}

\begin{lemma}Let~$X$ be a scheme (or a ringed space). Let~$(\E_i)_i$ be a
directed system of~$\O_X$-modules such that~$\E \defeq \colim_i \E_i$ is of
finite type. If~$X$ is quasicompact, there is an index~$i$ such that~$\E_i$ is
of finite type and such that the coprojection~$\E_i \to \E$ is an epimorphism
of sheaves of modules.
\end{lemma}

\begin{proof}Since the usual proof of the statement ``if a directed colimit of
modules~$(M_i)_i$ is finitely generated, then so is one of the modules and its
coprojection into~$\colim_i M_i$ is surjective'' is intuitionistic, it can be
applied in the internal universe of~$\Sh(X)$. Hence we have
\[ \Sh(X) \models \bigvee_i \speak{$\E_i$ is finitely generated and~$\E_i \to \E$
is surjective}. \]
Therefore we can conclude by Proposition~\ref{prop:finite-type-and-co} and
by Proposition~\ref{prop:quasicompact-meta}.
\end{proof}

\begin{caveat}There's a lemma stating that on a quasicompact and quasiseparated
scheme, every quasicoherent sheaf of modules is a filtered colimit of finitely
presented sheaves of modules~\stacksproject{07V9}. There's also the
corresponding statement for modules, whose standard proof is intuitionistic:
Any module~$M$ is a filtered colimit of finitely presented modules (namely the
finitely presented modules mapping to~$M$).

However, the stated lemma does not immediately follow by applying the statement
for modules in the internal universe. This only yields that any sheaf of
modules is an \emph{internal} filtered colimit; those are more
general.\footnote{Any small category~$\I$ induces a small
category~$\ul{\I}$ internal to~$\Sh(X)$ in such a way that the category of
diagrams over~$\I$ coincides with the category of internal diagrams
over~$\ul{\I}$ and the corresponding notions of limit and colimit agree.
However, not every internal small category is of the form~$\ul{\I}$. Therefore
internal limits and colimits are more flexible than external ones.

For instance, it's not true that any sheaf of sets is a colimit of a suitable
system of copies of the terminal sheaf. In contrast, internally, any set is a
colimit of a suitable system of copies of the singleton set.}
\end{caveat}

\section{Quasicoherent sheaves of modules}
\label{sect:qcoh}

Recall that an~$\O_X$-module~$\F$ on a ringed space~$X$ is \emph{quasicoherent}
if and only if there exists a covering of~$X$ by open subsets~$U$ such that on
each such set~$U$, there exists an exact sequence
\[ (\O_X|_U)^J \longrightarrow (\O_X|_U)^I \longrightarrow \F|_U \longrightarrow 0 \]
of~$\O_X|_U$-modules, where~$I$ and~$J$ are arbitrary sets (which may depend

If~$X$ is a scheme, quasicoherence can also be characterized in
terms of inclusions of distinguished open subsets of affines:
An~$\O_X$-module~$\F$ is quasicoherent if and only if for any open affine
subscheme~$U = \Spec A$ of~$X$ and any function~$f \in A$, the canonical map
\[ \Gamma(U,\F)[f^{-1}] \longrightarrow \Gamma(D(f),\F),\
\tfrac{s}{f^n} \longmapsto f^{-n} s|_{D(f)} \]
is an isomorphism of~$A[f^{-1}]$-modules. Here~$D(f) \subseteq U$ denotes the
standard open subset~$\{ \ppp \in \Spec A \,|\, f \not\in \ppp \}$. Both
conditions can be internalized.

\begin{prop}Let~$X$ be a ringed space. Let~$\F$ be an~$\O_X$-module. Then~$\F$
is quasicoherent if and only if
\[ \Sh(X) \models \exists I,J\ \mathrm{lc}\_ \speak{there exists an
exact sequence~$\O_X^J \to \O_X^I \to \F \to 0$}. \]
The ``\textnormal{lc}'' indicates that when interpreting this internal statement with the
Kripke--Joyal semantics,~$I$ and~$J$ should only be instantiated with
\emph{locally constant} sheaves.
\end{prop}
\begin{proof} We only sketch the proof.
The translation of the internal statement is that there exists a covering
of~$X$ by open subsets~$U$ such that for each such~$U$, there exist sets~$I,J$
and an exact sequence
\[ (\O_X|_U)^{\ul{J}} \longrightarrow (\O_X|_U)^{\ul{I}} \longrightarrow \F|_U
\longrightarrow 0 \]
where~$\ul{I}$ and~$\ul{J}$ are the constant sheaves associated to~$I$
respectively~$J$. The term~``$(\O_X|_U)^{\ul{I}}$'' refers to the internally
defined free~$\O_X$-module with basis the elements of~$\ul{I}$. By exploiting
that~$\ul{I}$ is a discrete set from the internal point of view (\ie any two
elements are either equal or not), one can show that this is the same
as~$(\O_X|_U)^I$; similarly for~$J$. With this observation, the statement
\end{proof}

\begin{rem}The restriction to locally constant sheaves is really necessary: The
internal statement~$\Sh(X) \models \exists I,J\_ \speak{there exists an
exact sequence~$\O_X^J \to \O_X^I \to \F \to 0$}$ is true for
\emph{any}~$\O_X$-module~$\F$. This is because the usual proof of the fact that
any module admits a resolution by (not necessarily finite) free modules is
intuitionistically valid and thus also valid in the internal

I don't know a useful internal characterization of
locally constant sheaves (but see Section~\ref{sect:lc-sheaves}). The
alternative internal condition given by the following
theorem does not need such a characterization.

\begin{thm}\label{thm:qcoh-sheafchar}
Let~$X$ be a scheme. Let~$\F$ be an~$\O_X$-module. Then~$\F$ is
quasicoherent if and only if, from the internal perspective, for any~$f\?\O_X$,
the localized module~$\F[f^{-1}]$ is a sheaf for the modal operator~$(\speak{$f$ \inv}
\Rightarrow \placeholder)$.
\end{thm}

In detail, the internal condition is that for any~$f\?\O_X$, it holds that
\[ \forall s\?\F[f^{-1}]\_
(\speak{$f$ \inv} \Rightarrow s = 0) \Longrightarrow s = 0 \]
and for any subsingleton~$\S \subseteq \F[f^{-1}]$ it holds that
\[ (\speak{$f$ \inv} \Rightarrow \speak{$\S$ inhabited}) \Longrightarrow
\exists s\?\F[f^{-1}]\_
(\speak{$f$ \inv} \Rightarrow s \in \S). \]
Unlike with the internalizations of finite type, finite presentation and
coherence, this condition is \emph{not} a standard condition of commutative
algebra. In fact, in classical logic, this condition is always satisfied --
for trivial logical reasons if~$f$ is invertible, and because~$\F[f^{-1}]$ is
the zero module if~$f$ is not invertible (since~$f$ is nilpotent then, by

That this condition in not known in commutative algebra is to be expected:
Quasicoherence is a condition on sheaves of modules, ensuring
that they are locally isomorphic to sheaves of the form~$M^\sim$,
where~$M$ is a plain module. But in commutative algebra, one \emph{only} studies plain
modules (and not sheaves of modules). The quasicoherence condition is imported
into the realm of commutative algebra only by the internal language.

We give the proof of Theorem~\ref{thm:qcoh-sheafchar} below, after first discussing some examples
and consequences. The proof will explain the origin of this condition.
The localized module~$\F[f^{-1}]$ appearing in the theorem
is externally a certain sheaf. If~$f \in \Gamma(U,\O_X)$, then it is the
sheafification of the presheaf on~$U$ given by~$V \mapsto
\Gamma(V,\F)[f^{-1}]$.

\begin{ex}The zero~$\O_X$-module is quasicoherent, since (it and) all
localizations of it are singleton sets from the internal perspective and
thus~$\Box$-sheaves for any modal operator~$\Box$
by Example~\ref{ex:special-sets-sheaves}.\end{ex}

\begin{cor}\label{cor:submodule-qcoh}
Let~$X$ be a scheme. Let~$\F$ be a quasicoherent~$\O_X$-module.
Let~$\G \subseteq \F$ be a submodule. Then~$\G$ is quasicoherent if and only
\[ \Sh(X) \models \forall f\?\O_X\_
\forall s\?\F\_
(\speak{$f$ \inv} \Rightarrow s \in \G) \Longrightarrow
\bigvee_{n \geq 0} f^n s \in \G. \]
\end{cor}