Return to Answer

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

You can then define the locale $\mathbb{Q}_p$ as $\bigcup \frac{1}{p^k} \mathbb{Z}_p$ (this a sequence of space where each space is open in the next so everything goes well...) and interally, the ring of continuous function with value 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 coincide 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 any way 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...

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...

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

You can then define the locale $\mathbb{Q}_p$ as $\bigcup \frac{1}{p^k} \mathbb{Z}_p$ (this a sequence of space where each space is open in the next so everything goes well...) and interally, the ring of continuous function with value 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 coincide 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 function, but on a locally connected space, continuous functions with value in $\mathbb{Z}_p$ corresponds to locally constant functions any way...

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 (and every time it makes sense to say something like this, the points of this locale obviously corresponds to continuous function, just because there are classified by a locale...).

So a general consequence to remember is that "completion by Cauchy filter 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 is equivalent and a bit more sequential)

Ref 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...

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

You can then define the locale $\mathbb{Q}_p$ as $\bigcup \frac{1}{p^k} \mathbb{Z}_p$ (this a sequence of space where each space is open in the next so everything goes well...) and interally, the ring of continuous function with value 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 coincide 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 any way 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...

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

You can then define the locale $\mathbb{Q}_p$ as $\bigcup \frac{1}{p^k} \mathbb{Z}_p$ (this a sequence of space where each space is open in the next so everything goes well...) and interally, the ring of continuous function with value 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 coincide 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 function, but on a locally connected space, continuous functions with value in $\mathbb{Z}_p$ corresponds to locally constant functions any way...

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 (and every time it makes sense to say something like this, the points of this locale obviously corresponds to continuous function, just because there are classified by a locale...).

So a general consequence to remember is that "completion by Cauchy filter 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 is equivalent and a bit more sequential)

PS:I will add a few references in a minute.

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

You can then define the locale $\mathbb{Q}_p$ as $\bigcup \frac{1}{p^k} \mathbb{Z}_p$ (this a sequence of space where each space is open in the next so everything goes well...) and interally, the ring of continuous function with value 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 coincide 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 function, but on a locally connected space, continuous functions with value in $\mathbb{Z}_p$ corresponds to locally constant functions any way...

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 (and every time it makes sense to say something like this, the points of this locale obviously corresponds to continuous function, just because there are classified by a locale...).

So a general consequence to remember is that "completion by Cauchy filter 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 is equivalent and a bit more sequential)

Ref 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...