# Brouwer's theorem for the Cauchy reals

Brouwer famously proved, using principles motivated by intuitionistic choice sequences, that every function $\mathbb{R}\to \mathbb{R}$ is continuous. In Sheaves in geometry and logic (section VI.9), MacLane and Moerdijk exhibit a topos (the topos of sheaves on any sufficiently nice small full subcategory $\mathbf{T}\subseteq\mathrm{Top}$) in which this theorem holds in the internal logic. However, their proof is about the Dedekind real numbers. Can anyone point to a topos in which Brouwer's theorem holds for the Cauchy real numbers?

Of course it would suffice to give a topos in which Brouwer's theorem holds and in which the Cauchy and Dedekind real numbers coincide (e.g. if countable choice holds). This is not the case for MacLane and Moerdijk's example, in which $\mathbf{R}_D$ is the sheaf of continuous $\mathbb{R}$-valued functions while (at least if all spaces in $\mathbf{T}$ are locally connected) $\mathbf{R}_C$ is the sheaf of locally constant $\mathbb{R}$-valued functions. Moreover, it is easy to see that in this case there do exist discontinuous functions $\mathbf{R}_C \to \mathbf{R}_C$; so a different example is needed.

• First place that comes to my mind is Johnstone's topological topos but I never looked at Cauchy reals there – მამუკა ჯიბლაძე Aug 28 '15 at 5:51
• Another related thought: as I first learned from Escardó & Simpson's "A Universal Characterization of the Closed Euclidean Interval", there is actually no reason to expect $\mathbf R_C$ to be Cauchy complete. They point out that the "correct" guy in this respect is what they call Euclidean reals - the Cauchy complete envelope of rationals. By the time of loc. cit. they did not know whether this might ever differ from $\mathbf R_C$. Does anybody have an update on that? – მამუკა ჯიბლაძე Aug 28 '15 at 8:58
• I believe the effective topos is an example where every function on the Cauchy reals is continuous. – aws Aug 28 '15 at 12:58
• @aws ah, indeed, thanks! You should post that as an answer. – Mike Shulman Aug 28 '15 at 15:03

Following Mike's suggestion, I post my comment as an answer.

Brouwer's theorem that all functions $\mathbb{R} \rightarrow \mathbb{R}$ are continuous holds in the effective topos. For example, this appears as Theorem 3.3.8 in van Oosten, Realizability: An Introduction to its Categorical Side. In fact it follows as a theorem from Markov's Principle and extended Church's thesis, which was apparently first discovered by Tsejtin.

• You didn't mention that in the effective topos the Cauchy and Dedekind reals coincide, because countable choice holds. But I'm glad you gave another citation, because Hyland's original paper omits the proof of Brouwer's theorem. – Mike Shulman Aug 28 '15 at 15:56

The notion of "Cauchy real" is always a bit ambiguous: it depends on what you call a Cauchy sequence. For the argument that follow I need a notion of Cauchy sequence that is geometric (is classified by a locale). Two such examples (defining two different spaces of Cauchy Real) are:

• A Cauchy sequence is a sequence of rational that converge (with just existential quantifier) in the space of Dedekind real.

• A Cauchy sequence is a sequence of rational such that $|x_n - x_{n+1} |<1/n^2$ for all $n$.

The point is that with such a definition, the theory of Cauchy sequences is classified by a locale $K$ which is endowed with a map "limit" to the locale $\mathbb{R}$.

I claim that the map from $K$ to $\mathbb{R}$ is a really nice surjection. It might not be an open surjection by itself (and it is clearly not proper), but there is an open surjection $X \rightarrow \mathbb{R}$ that factors into $K$ (see below), hence $K \rightarrow \mathbb{R}$ is an effective descent morphism and in particular a stably regular epimorphism of locales.

Let $\mathcal{L}$ be a class of locales which contains both $K$ and $\mathbb{R}$ and is stable under open subspace and fiber product. And put a Grothendieck topology on it which is subcanonical and contain our surjection $K \rightarrow \mathbb{R}$ as well as the ope covering (the topology generated by open surjection, the canonical topology of $\mathcal{L}$, the canonical topology of the category of locale or the topology of effective descent morphism of locales are all acceptable solutions). let $\mathcal{T}$ be the resulting Grothendieck topos of sheaves.

It might not be true that the object of Dedekind real is represented by the locale $\mathbb{R}$. But if $X$ is a pro-discrete locale in $\mathcal{L}$ then the object of points of $X$ in $\mathcal{T}$ is represented by $X$ : Indeed this is clearly true if $X$ is a discrete locale and it pass to projective limit. Also it appears (see $C)$ below) that this is also true when $X$ is just a sub-locale of a pro-discrete locale. The locale for Cauchy sequences given above is pro-discrete so this apply to it, so the object of Cauchy sequences in $\mathcal{T}$ is represented by $K \in \mathcal{L}$.

The space of Cauchy real is in any topos described as the quotient of the object of points of $K$ by the equivalence relation of points of $K \times_{\mathbb{R}} K$ which is also a sublocale of a pro-discrete locale. The the object of Cauchy real is the quotient in $\mathcal{T}$ of the object represented by $K$ by the equivalence relation represented by $K \times_{\mathbb{R}} K$ but as we have chose the topology so that $K \rightarrow \mathbb{R}$ is a covering this quotient is the object represented by $\mathbb{R}$.

The object of endomorphisms of the object of Cauchy reals is then just the sheaf which to any locale $A \in \mathcal{L}$ associate the set of continuous functions from $A \times \mathbb{R} \rightarrow \mathbb{R}$ and they are internally continuous (to be honest, I havn't checked that last claim yet, but that sound reasonable).

Appendix: here are some clarification.

A) The open surjection $X \rightarrow K \rightarrow \mathbb{R}$.

We work internally in $\mathbb{R}$. One has the universal Dedekind real number $x$ corresponding to the identity $\mathbb{R} \rightarrow \mathbb{R}$.

For each positive integer $n$ the set $A_n$ of rational numbers $q$ such that $|x-q|<2^{-n}$ is inhabited (this is one of the characterization Dedekind numbers). you can then define the locale $X$ (still internally in $\mathbb{R}$) as $X =\prod_{n \in \mathbb{N}} A_n$. An inhabited set is in particular an open surjection to the point and it is a classical lemma in constructive locale theory that a product indexed by a decidable set of locales with an open surjection to the point also have an open surjection to the point (this is a kind of dual version of the Tychonov theorem for locales).

So we have constructed a locale $X$ with an open surjection to $\mathbb{R}$. You can check that the definition of the $A_n$ is geometric and hence stable under inverse image functor and that product of locales are stable under inverse image functors (obviously because inverse image functor are pullback in the category of locales). Hence, (externally now) $X$ classifies the theory whose model is the data of a real number $r$ together with a sequence of rational numbers $a_n$ such that for all $n$ $|a_n - r| < 2^{-n}$, the map to $\mathbb{R}$ just forgetting the sequence. The sequence of $a_n$ will then give you a Cauchy sequence converging to $r$ and hence you have a map from this locale to the locale $K$. (in fact depending on your definition of $K$ you might be able to prove this way that $K \rightarrow X$ itself is an open surjection.

B) The precise definiton of the locale $K$ for the two examples of definition of Cauchy sequences I gave above:

For the first one $K$ is the fiber product for $[\mathbb{N},\mathbb{Q}]$ and $[\mathbb{N}^{\infty},\mathbb{R}]$ over $[\mathbb{N},\mathbb{R}]$, where $\mathbb{Q}$ has the discrete topology and $\mathbb{N}^{\infty}$ is still the compact space with a sequence of points and its limit.

For the second definition, $K$ is just a (closed) subspace of the exponential locale $[\mathbb{N},\mathbb{Q}]$ defined by the inequalities in the definition.

C) For any sub-locale $X$ of a pro-discrete locale in $\mathcal{L}$ The object of $\mathcal{T}$-point of $X$ is the sheaves represented by $X$.

Let $U$ be an open subspace of $X$ a pro-discrete locale. Then it is still true that the space of points of $U$ in $\mathcal{T}$ is represented by $U$: indeed if $U$ is a basic open then $U$ is itself a pro-discrete locale, and otherwise $U$ is a union of basic open and this properties also passes to union as soon as we assume that the topology on $\mathcal{L}$ contains open covering. Now because a pro-discrete locale is regular, any sublocale is an intersection of open sublocale and so can be written as a projective limit of locales which satisfies this properties.

D) What happen to Dedekind reals in $\mathcal{T}$ ?

SO this topos $\mathcal{T}$ as an object $\Omega'$ classified by the Sierpinski locale (whether it is in $\mathcal{L}$ or not) which is a subobject of the sub-object classifier. Because of that one dispose internally of a notion of "nice subobject" or "open subobject": by definition the sub-objects whose classifying map land in $\Omega'$, and hence internally $\Omega'$ si the object of nice subobject of $\{*\}$. One can easily see that $\mathbb{R}$ is exactly the object of "nice Dedekind real",that is of two sided dedekind cut, such that the two cut are nice subobject of $\mathbb{Q}$. But I don't see any reason for any two sidded dedekind cut to be "nice". In fact when we enlarge $\mathcal{L}$ the subobject classifier become larger and larger while $\Omega'$ stay roughly the same, hence one can image that the situation become worst and worst... but I havn't been able to find an example of a non nice Dedekind real, moreover the fact that the exact same discussion apply when the topology is just the topology of open covering and that in this case there is no "non nice" dedekind real suggest that one can still hope that the Dedekind real and the Cauchy real are the same.

• I don't see how you can get a locale classifying infinite sequences of any sort, since inverse image functors need not preserve exponentials. – Mike Shulman Aug 28 '15 at 14:56
• Indeed, but I am sorry I don't see why that could be a problem: If you have a locale $X$ then the locale $X^{\mathbb{N}}$ (which exists either because $\mathbb{N}$ is locally compact or because the category of locales have arbitrary product) classify the sequence of points of $X$ for rather tautological reason: a morphism from $Y$ to $X^{\mathbb{N}}$ is a sequence indexed by $\mathbb{N}$ of morphisms from $Y$ to $X$. which is the same as internally in $Y$ a $\mathbb{N}$-indexed familly of points of $X$ (for $\mathbb{N}$ the NNO of $Y$ this time) – Simon Henry Aug 28 '15 at 15:11
• The fact that exponential are not preserved by inverse image functors only say that classifying spaces for sequences are not discrete. – Simon Henry Aug 28 '15 at 15:14
• Hmm... okay. Apparently there are things you can do with geometric logic that I didn't realize. Can you explain why your two notions of Cauchy sequence are different (are they only different as locales? They sure seem to be the same as sets) and where your open surjection $X\to \mathbb{R}$ comes from that factors through $K$? – Mike Shulman Aug 28 '15 at 15:55
• They are different beceause of the failure of the axiom of countable (dependant ? ) choice. I've added the rest in an edit. – Simon Henry Aug 28 '15 at 16:26

Historically the first model with validity of the Brouwer 'theorem' was the topos $\mathrm{Sh}(N^N)$ of sheaves on Baire space. This goes apparently back to Dana Scott here:

Scott, Extending the topological interpretation to intuitionistic analysis II , pp.235-255 in Myhill,Kino,Vesley (eds.) Intuitionism and proof theory, North-Holland 1970. (pay-walled here)

The first installment of Scott is probably also of interest in the wider context and available from numdam

According to an exercise in Moerdijk- Mac Lane (p.345) $\mathrm{Sh}(N^N)$ has dependent choice as well, so it should fit your bill.

The question of validity of the Brouwer theorem was studied by Martin Hyland in the early seventies, relevant references are the following in the 'applications of sheaves' LNM, in particular the second:

Fourman, Hyland, Sheaf models of analyis, pp.280-301 LNM 753 Springer Heidelberg 1979. (PDF)

Hyland, Continuity in spatial toposes, pp.442-465 LNM 753 Springer Heidelberg 1979. (pay-walled from springer page)

It seems the question then is, can $R_C$ satify the Brouwer thm with coinciding with $R_D$ ?