# Properties of the internal language of the category of sheaves.

Consider a simple case of sheaves on some topological space $X$, $\operatorname{Sh}(X)$ (recall that a sieve on $U$ is covering iff its $\operatorname{sup}$ is $U$). All of these are Grothendieck toposes but clearly not all of them are equivalent.

Is there an overview of what properties of $\operatorname{Sh}(X)$ are induced by the properties of $X$? The properties I am interested in are the logical principles that hold in the internal logic. Of course the properties must necessarily be the properties of the locale of opens $\mathcal{O}(X)$.

The elephant (Johnstone) has a list of some properties induced by the properties of $\mathcal{O}(X)$, but most of these are about the existence of geometric morphisms, which of course in some cases allow one to define some modalities in the internal language, but I would also like to know if there are some formulas of ordinary higher-order logic that are valid.

For example, suppose $X$ is compact. Is there a useful or interesting logical principle that holds in $\operatorname{Sh}(X)$ but does not hold in sheaves over non-compact spaces? Perhaps some form of choice?

A topological space (or locale) $X$ is local (i.e. in any covering of $X$ by open subsets at least one such subset is already equal to $X$) iff the internal language of $\mathrm{Sh}(X)$ fulfils the following disjunction property: If $(\phi_i)_{i \in I}$ is an arbitrary family of formulas and $\mathrm{Sh}(X) \models \bigvee_{i \in I} \phi_i$, then there exists an index $i \in I$ such that $\mathrm{Sh}(X) \models \phi_i$.

Also, if $X$ is local, the internal language fulfils the following existence property: If $\mathrm{Sh}(X) \models \exists x : \mathcal{F}. \phi(x)$, then there actually exists a global section $x \in \Gamma(X,\mathcal{F})$ such that $\mathrm{Sh}(X) \models \phi(x)$.

A topological space $X$ is compact iff the internal language of $\mathrm{Sh}(X)$ fulfils the following property: If $I$ is a directed set, $(\phi_i)_{i \in I}$ is a monotone family of formulas (meaning $\mathrm{Sh}(X) \models (\phi_i \Rightarrow \phi_j)$ for $i \preceq j$) and $\mathrm{Sh}(X) \models \bigvee_{i \in I} \phi_i$, then there exists an index $i \in I$ such that $\mathrm{Sh}(X) \models \phi_i$. This follows directly from the order-theoretic characterization of compactness (a space $X$ being compact iff for any monotone family $(U_i)_{i \in I}$ of open sets with $X = \bigcup_i U_i$, there exists $i \in I$ such that $X = U_i$).

As an example, you can use the latter characterization to give an internal proof of lemma 01BB in the Stacks Project (saying that if a filtered colimit $\mathcal{F} = \mathrm{colim}_i \mathcal{F}_i$ of $\mathcal{O}_X$-modules is of finite type on a quasi-compact scheme $X$, then one of the maps $\mathcal{F}_i \to \mathcal{F}$ is an epimorphism) by reducing to the following familiar fact of constructive linear algebra: If a filtered colimit $A = \mathrm{colim}_i A_i$ is finitely generated, one of the maps $A_i \to A$ is surjective.

Unfortunately, the logical principles above are meta properties of the internal language, so I'm not sure this answers your question.

Addendum: An intrinsic characterization of compactness is not possible, i.e. there cannot exist a formula $\phi$ such that the internal language of the sheaf topos of a topological space satisfies $\phi$ iff the space is compact: If a topological space $X$ can be covered by compact subspaces $U_i$, the formula $\phi$ would be satisfied on each $U_i$ and hence, by the local character of the internal language, on $X$ as well. If $X$ itself is not compact, this is a contradiction.

• Is there any reference with more characterizations like this? As you say these are meta properties. I would have liked internal principles much more. – Aleš Bizjak Nov 27 '13 at 18:11
• I don't know of any such references. You might be interested in Moerdijk's and Vermeulen's Proper Maps of Toposes, in which they give an internal characterization of proper maps. (You need an extension of the internal language which can talk about locally internal categories if you want the translation to be completely mechanical. Details are only available in German, unfortunately.) See addendum, there is a trivial obstruction to internal characterizability. – Ingo Blechschmidt Nov 29 '13 at 9:52
• And I guess the same trivial restriction shows that a lot of other properties cannot be characterized internally. Thank you. – Aleš Bizjak Nov 29 '13 at 18:30