The real numbers can be defined in two ways (well, more than two, but let's stick to these for now): as the Cauchy completion of the metric space $\mathbb{Q}$ with its usual absolute value, or as the Dedekind completion of the ordered set $\mathbb{Q}$ with its usual ordering.

When these two constructions are performed internally in a topos, they generally yield different results, and often it is the Dedekind construction that gives a more useful answer. In particular, for any topological space $X$, the Dedekind real number object in $\mathrm{Sh}(X)$ is the sheaf of continuous $\mathbb{R}$-valued functions on $X$, where $\mathbb{R}$ has its usual topology. (And this generalizes to some big toposes too.) Roughly, this is because the definition of "a Dedekind real number" is constructively equivalent to "a point of the locale of formal real numbers", where the latter locale can be defined constructively, and classically turns out to be equivalent to the usual topological space $\mathbb{R}$.

However, the Cauchy definition of $\mathbb{R}$ has other generalizations: we can complete with respect to a non-Archimedean absolute value instead, obtaining the $p$-adic numbers $\mathbb{Q}_p$. We can do this internally in a topos too, but as with $\mathbb{R}$, in general we will not get the "right" answer. My question is, is there any way to construct "the $p$-adic numbers" constructively which, when interpreted in $\mathrm{Sh}(X)$, will yield the sheaf of continuous $\mathbb{Q}_p$-valued functions on $X$, where $\mathbb{Q}_p$ has its usual topology? In particular, is there a "locale of formal $p$-adic numbers" that can be defined constructively and that classically is equivalent to the usual topological space $\mathbb{Q}_p$?

• One should perhaps mention the formalisation of p-adic numbers in UniMath arxiv.org/abs/1302.1207, github.com/vladimirias/UniMath/tree/master/UniMath/PAdics, but I don't know which approach they take aside from the fact they get a Heyting field, as the field of fractions of the p-adic integers. – David Roberts Aug 13 '15 at 1:24
• @DavidRoberts I've never read Coq before, but it looks like they simply define $p$-adic integers as infinite sequences of integers between 0 and p-1, equipped with an add-with-carry rule. – S. Carnahan Aug 13 '15 at 5:18

Yes there is: the formal locale of p-adic integer is simply defined as the projective limit of the $\mathbb{Z}/p^k\mathbb{Z}$ (as a pro-finite locale). So internally in any topos a continuous function with values in $\mathbb{Z}_p$ corresponds to an element of the projective limit of the $\mathbb{Z}/p^k\mathbb{Z}$ (as a set this time)

You can then define the locale $\mathbb{Q}_p$ as $\bigcup \frac{1}{p^k} \mathbb{Z}_p$ (this is a sequence of spaces where each space is open in the next so everything goes well...) and internally, the ring of continuous functions with values in $\mathbb{Q}_p$ is just $\mathbb{Z}_p [1/p]$ for the previously defined $\mathbb{Z}_p$.

It turns out that, in this precise case, this coincides with the sequential completion (easy to see from the projective limit description...).

This is a strange coincidence, but you can relate this to the fact that on a locally connected space the sequential completion corresponds to locally constant functions, but on a locally connected space, continuous functions with values in $\mathbb{Z}_p$ or $\mathbb{Q}_p$ are locally constant functions anyway because of the total disconnectedness.

There is in fact way more to it:

Steve Vickers has show how to define more generally the localic completion of a metric set (a set with a distance), and at least when the distance is symmetric this locale is essentially the Classifying space for the theory of regular Cauchy filter. Moreover it appears that this completion is stable under pullback along geometric morphism (this is not completely trivial, I prove it in my paper linked below) and because of this you will trivially have that if your metric set is the pullback of a metric set in the base topos then the points of its localic completion will be exactly the continuous function with values in the localic completion computed in the base topos.

So a general consequence to remember is that (constructively) "completion by Cauchy filters always give you the correct set of points" so in any case if you have any valuation on a fields (note that over a non boolean topos even if the fields is $\mathbb{Q}$ it might not be equivalent to $|\_ |_p$ for some $p$) the "correct" completion (the one corresponding to the Dedekind completion) is the Cauchy filter completion. For metric space there is also a notion of "Cauchy approximation" which gives the same completion and is a bit more 'sequential': they are decreasing sequences of open ball whose diameter goes to zero at a controlled speed.

References for localic completion:

• Vickers wrote several paper on the subject, the more relevant is I think "Localic completion of quasimetric spaces" and after that there is two other on the non-symmetric case "Localic completion of generalized metric spaces" I & II. His presentation is rather different from what I add in mind, so I will look if there is something older more simple.

• This paper of mine where I define the completion of a symmetric metric locale and study all the geometricity properties (stability under pull-back) in section 3.3 . It is exactly what you need but because it deals with metric locales instead of metric sets there is some annoying additional complication...

• Thanks, Simon. I had a feeling that the functions would be locally constant, but couldn't any way prove it. – David Roberts Aug 13 '15 at 7:49
• You mean for the sequential construction of real numbers ? I've learned this from Peter Johnstone's Elephant (example D4.7.12). The argument is fairly general and I think work for any sequential completion of a metric set. – Simon Henry Aug 13 '15 at 7:55
• No, I meant continuous functions with values in Q_p. But that is, I see, only the case for locally connected spaces. In general one can have nasty spaces (but perhaps using locales things are tempered somewhat). – David Roberts Aug 13 '15 at 7:59
• Well the identify map from the locale $\mathbb{Q}_p$ to the locale $\mathbb{Q}_p$ will not be locally constant. My paragraph about locally constant function only works for locally connected locales and was there only to show that it is not absurd that the sequential completion coincide with the sheaf of continuous functions. – Simon Henry Aug 13 '15 at 8:02
• Yes, and I'm pleasantly surprised the sequential completion is the right thing in general, and youtu.be/RK5n-X-Jlbk?t=2m1s :-) – David Roberts Aug 13 '15 at 9:18

Localic completion is awesome and is the way to answer your question as asked (which requests a locale).

However, a simpler answer for getting the correct (internal) set of $p$-adic numbers (the one whose points are, externally, the $p$-adic valued continuous maps) is simply to complete using all Cauchy nets (or filters) rather than only the sequences (or sequential filters). Simon has stated as much already, but I wanted to extract that fact.

It is just not true in constructive mathematics that metric spaces are sequential spaces, so one must always work with all nets and not just restrict to sequences. (Predicative constructivists may have some difficulty with this, of course, although fortunately they can still deal with the locale via a prosite for it.)

• I highly agree, I only talked about localic completion to explain why it gives function into $\mathbb{Q}_p$. but I want to add something : if you want to use nets rather than filter I think you need nets indexed by pre-ordered set and not just ordered set (so that you can turn a Filter $\mathcal{F}$ into the nets $\{f \in \mathcal{F}, x \in f \}$ ordered by the first component. Otherwise I think the two notion are not equivalent. – Simon Henry Aug 29 '15 at 17:14
• Good point. But is there a way to complete using nets (without mentioning filters) that clearly gives a set (rather than a proper class)? – Mike Shulman Aug 29 '15 at 21:38
• @SimonHenry: I've always seen preorders specified in the definition of a net, so that should be no problem. That said, every net is equivalent to one whose domain is a partial order, if for some reason you want to make this restriction, using an NNO (which we have in this discussion). The construction is given in Section 7.12 of Eric Schechter's Handbook of Analysis and its Foundations (although this requires a trivial modification to be constructive). I consider this a fact of amusement only, however; I don't see any purpose in doing this. – Toby Bartels Aug 30 '15 at 5:04
• @MikeShulman: Yes, given a set $X$, every net in $X$ is equivalent to one whose domain is a subset of $\mathcal{P}X \times X$, for reasons hinted at in Simon's comment, (or a subset of $\mathcal{P}X \times \mathbb{N} \times X$ if you want the domain to be a partial order, for reasons hinted at in my previous comment). Of course, it's simpler just to talk about filters; nets are useful pedagogically for people who are only familiar with sequences, but otherwise they're only important as a way to get filters (if that). – Toby Bartels Aug 30 '15 at 5:18
• @TobyBartels I consider that equivalence to be "mentioning filters". (-: – Mike Shulman Aug 30 '15 at 5:34