# 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.) – Andreas Blass Jan 13 at 0:21
• See also Sketches of an Elephant, D.4.7.12. – Todd Trimble Jan 13 at 1:00
• No, that is only correct over a locally connected space. – Simon Henry Jan 13 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}$. – Simon Henry Jan 13 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}$. – Simon Henry Jan 13 at 4:15

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. – Zhen Lin Feb 16 at 0:59
• @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). – Gro-Tsen Feb 19 at 15:07