# In the internal language of the topos of sheaves on a topological space, can we define locally constant real-valued functions?

For the purposes of this question, in a Grothendieck topos, we will call “definable” the objects and relations obtained from the terminal object, the natural numbers object and the subobject classifier, by taking finite products, finite coproducts, exponentials (internal homs) and taking subobjects defined by [edit 2021-02-16] finitary formulas in the internal language (using previously defined objects and relations). (I'm saying this a bit concisely in the hope that there are no major subtleties.)

In particular, if $$X$$ is a topological space and we consider the topos of sheaves on $$X$$, the sheaf of continuous functions with values in each one of the following is definable (along with its usual algebraic structure):

• $$\mathbb{N}$$ with the discrete topology (this is the natural numbers object),

• $$\mathbb{Z}$$ with the discrete topology (this is the Grothendieck group of the previous),

• $$\mathbb{Q}$$ with the discrete topology (this is the fraction field of the previous),

• $$\mathbb{R}$$ with the usual (Euclidean) topology (by Dedekind cuts).

Let us call $$\mathbf{N}, \mathbf{Z}, \mathbf{Q}, \mathbf{R}$$ the corresponding definable objects of the topos.

Now for a long time I thought one could not define the sheaf of continuous functions with values in

• $$\mathbb{Q}$$ with the usual (i.e. induced by $$\mathbb{R}$$) topology,

but I serendipitously realized that you can, namely it is given by the following object:

$$\{x\in\mathbf{R} : \forall y\in\mathbf{R}. ((\forall z\in\mathbf{Q}.(y\mathrel{\#}z)) \Rightarrow (x\mathrel{\#}y))\}$$

where $$x\mathrel{\#}y$$ stands for $$(xy)$$ or, equivalently, $$\exists z\in\mathbf{R}.(z\cdot(x-y)=1)$$.

(This is easy to see: first note that $$\{x\in\mathbf{R} : \forall y\in\mathbf{Q}. (x\mathrel{\#}y)\}$$ defines the sheaf of continuous functions with values in $$\mathbb{R}\setminus\mathbb{Q}$$ with the usual topology, then repeat the reasoning.)

So now I am curious to know whether the “converse” is possible:

• $$\mathbb{R}$$ with the discrete topology;

in other words:

Question: is the sheaf of locally constant real-valued functions on $$X$$ definable, uniformly in $$X$$, as a subobject of $$\mathbf{R}$$ in the topos of sheaves on $$X$$?

I imagine there is little hope of finding a good answer to the very general question “for which topological spaces $$Y$$ is the sheaf of continuous $$Y$$-valued functions on $$X$$ definable as an object in the topos?”, but of course, if someone wants a crack at it rather than the particular case above, by all means do!

• I was under the impression that the object of Cauchy reals (limits of Cauchy sequences of rationals) in a spatial topos gives you the locally constant real-valued functions. (But I don't think I ever checked that, and I don't immediately have a reference.) Jan 13, 2021 at 0:21
• See also Sketches of an Elephant, D.4.7.12. Jan 13, 2021 at 1:00
• No, that is only correct over a locally connected space. Jan 13, 2021 at 1:15
• A maybe easier questions that might shed some light on this is whether one can find a similar characterization locally constant functions to the power set of $\mathbb{N}$ as a subobject of the subobject classifier of $\mathbb{N}$. Jan 13, 2021 at 1:41
• To clarify my previous comment. As pointed out by Todd Trimble D.4.7.12(a) in sketches of an elephant indeed claim that if $X$ is locally connected, then in $Sh(X)$ the object of Cauchy real is the sheaf of locally constant functions. But D.4.7.12(b) gives a counted example to the claim in general : for any space X such that $Sh(X)$ satisfies CC (e.g. any second countable zero dimensional space) then the object of cauchy real in it is the sheaf of all continuous functions to $\mathbb{R}$. Jan 13, 2021 at 4:15

I can offer a helpful observation. Andrew Swan and I proved in Every metric space is separable in function realizability that in Kleene's function realizability topos every metric space is separable. One consequence of this is that in the internal language of a topos one cannot construct a non-separable metric space, or an uncountable set with decidable equality. Moreover, it is consistent to assume that every set with decidable equality is countable (Theorem 2.5, but see the comment following it.)

While this is not a complete answer to your question, it shows that if there is a definition of the discrete $$\mathbb{R}$$ in sheaves, we will not be able to prove intuitionistically that it is uncountable and has decidable equality.

• This sheaf of locally constant functions has (internally) decidable equality in every Grothendieck topos, but there are also some Grothendieck topos in which it is countable (take a boolean locale that collaps the cardinal $2^\omega$ to $\omega$), so you indeed can't prove that it is uncountable. Jul 16, 2021 at 17:48

It seems to me that for any set $$S$$ (e.g. $$S = \mathbb R$$), the classifying topos for locally-constant $$S$$-valued functions is the slice topos $$Set/S$$ of $$S$$-indexed sets, as this is equivalent to the topos of sheaves on $$S$$ regarded as a discrete topological space.

So because locally-constant $$S$$-valued functions admit a classifying topos, they can be axiomatized by a theory $$T_S$$ in geometric logic. I don't know what the axiomatization says, exactly, but one should be able to work it out from the literature. I don't know if a truly infinitary definition in geometric logic counts as "definable" for you, but I think this gives some form of positive answer.

If "locally constant $$\mathbb R$$-valued function" is supposed to mean something more closely related to the internal Dedekind reals $$\mathbf R$$ which doesn't agree with $$T_{\mathbb R}$$, then it's not clear to me what this distinct meaning is supposed to be. That is, if the theory $$T_{\mathbb R}$$ is not what you're looking for, then what is an example of a topos $$\mathcal E$$ where locally-constant $$\mathbf R$$-valued functions are not the same as models of $$T_{\mathbb R}$$?

• The geometric theory corresponding to $S$ is the one with propositional symbols $\phi_s$ labelled by $s \in S$ and axioms $\phi_s \land \phi_t \vdash \bot$ for $s \ne t$ and $\top \vdash \bigvee_{s \in S} \phi_s$. As you say, this is infinitary and takes $S$ as given. Feb 16, 2021 at 0:59
• I think the OP wants an object definable in an arbitrary elementary topos with NNO, such that when restricted to (say) spatial toposes one obtains the sheaf of locally constant real functions. For Grothendieck toposes there is an easy construction, obtained using infinite coproducts. Feb 16, 2021 at 1:08
• I agree with Zhen that the implied meaning of "internal language" is the finitary HOL, though it's not explicitly stated. I do think your observation is important and relevant enough to be an answer, though perhaps not the accepted answer. (-: Feb 16, 2021 at 3:19
• @TimCampion I don't quite understand your point. To me the question means we are looking for an object of the free topos (with a NNO and in these sense of logical functors). Such that its interpretation in any topos of the form Sh(X) is the sheaf (p^* R) of locally constant R-valued functions. We probably want this to be true not justs as sheaves, but with a bit of the structure of the real numbers (like ordered Q-algebra). I don't think this exists. But the question seems precise enough to admit a clear yes/no answer. Feb 16, 2021 at 16:22
• @TimCampion Yes, your characterization of the sheaf of locally constant $\mathbb{R}$-valued functions is correct, and I don't mean to say that it isn't. To put it differently, for $\mathcal{T}$ a Grothendieck topos there is a geometric morphism $p\colon \mathcal{T} \to \mathrm{Set}$ such that $p_*$ is the global sections functor and $p^*$ the constant sheaf construction, and the sheaf we are talking about is $p^*\mathbb{R}$. The question is whether it can be described internally without referring to $p$ (Simon Henry's formulation is probably the best). Feb 19, 2021 at 15:07