arithmetical and geometric reals in (models of) SDG

arithmetical and geometric reals in (models of) SDG

[Thomas Streicher]

Recently I was asking myself what is the relation between the arithmetical
(Dedekind) reals in a topos and a ring R satisfying the usual SDG axioms
(i.e. at least the Kock-Lawvere) axiom.

>From the few things I know about models of SDG it seems to me as if in the
usual sheaf models (over a site Loc of `loci') the Dedekind reals form a
subring of R = y(\Re) (where \Re is the locus corresponding to the reals).
As long as one considers just presheaves that's clear as the Dedekind reals
are given by \Delta(\Re).
Probably taking sheaves that situation isn't changed dramatically?

So my impression is that in the usual sheaf models of SDG the real line R
carries the structure of an algebra over the Dedekind reals. However, I don't
see how to construct such an embedding of Dedekind reals into R based only
on the usual axioms of SDG. Of course, when given an order on R and R is
assumed as a Q-algebra then one has a good candidate for a function from R
to R_D sending x \in R to {q \in Q | q.1 \leq x}. But how to define purely
logically an embedding of R_D into R remains mysterious (to me).

I am fully aware of the fact that my question is a bit `against the strain'
of SDG but we know that both kinds of reals do coexist in topos models.
But is this coexistence only peaceful or rather more collaborative?

I am certain that people must have thought about this but I couldn't find
anything at the usual places where to look. So I would be grateful for
comments (on the correctness of my above speculations) or pointers to
existing literature or folklore.

Best, Thomas Streicher

Re: arithmetical and geometric reals in (models of) SDG

[Andrej Bauer]

Thomas Streicher <streicher@mathematik.tu-darmstadt.de> writes:
>
> Recently I was asking myself what is the relation between the arithmetical
> (Dedekind) reals in a topos and a ring R satisfying the usual SDG axioms
> (i.e. at least the Kock-Lawvere) axiom.

Perhaps it is worth mentioning that in the ring of smooth reals R the
sequence a_k = 2^(-k) is Cauchy but has many "limits" because every
infinitesimal dx satisfies the condition "dx is the limit of a_k".
This shows that R is not Cauchy complete, not because limits of Cauchy
sequences are missing but because there are too many.

I once thought the above observation implied there can be no isometric
embedding of a Cauchy-complete field (e.g. the Dedekind reals) into R,
but now I am not convinced anymore.

Andrej Bauer

Department of Mathematics and Physics
University of Ljubljana
http://andrej.com