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

From: Andrej Bauer <[email-masked]>
Date: Wed, 07 Apr 2004 15:00:23 +0200

Thomas Streicher <[email-masked]> 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