From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/2128 Path: news.gmane.org!not-for-mail From: "Prof. Peter Johnstone" Newsgroups: gmane.science.mathematics.categories Subject: Re: Cauchy completeness of Cauchy reals Date: Sat, 25 Jan 2003 16:24:37 +0000 (GMT) Message-ID: References: <3E31F48C.90308@kestrel.edu> NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Trace: ger.gmane.org 1241018431 2621 80.91.229.2 (29 Apr 2009 15:20:31 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:20:31 +0000 (UTC) To: CATEGORIES LIST Original-X-From: rrosebru@mta.ca Sat Jan 25 16:54:15 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 25 Jan 2003 16:54:15 -0400 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18cX0i-0000T9-00 for categories-list@mta.ca; Sat, 25 Jan 2003 16:34:40 -0400 In-Reply-To: <3E31F48C.90308@kestrel.edu> X-Scanner: exiscan for exim4 (http://duncanthrax.net/exiscan/) *18cT6k-0003uj-00*vPtaD.U54TA* Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 53 Original-Lines: 44 Xref: news.gmane.org gmane.science.mathematics.categories:2128 Archived-At: On Fri, 24 Jan 2003, Dusko Pavlovic wrote: > > > > > >Set. Do you think your construction works in any topos? > > > the coalgebraic structures are defined using just arithmetic. in the > first one, there is the "no infinite sequences of 1s" condition, which i > am reminded depends on markov's principle; but that is just used in the > explanation. i don't think there are other constraints. > > >If so, what > >would "Cauchy reals" mean precisely in this general context? > > > it means fundamental sequence, with the equivalence relation in the > "lazy" mode, a la bishop, as described in andrej bauer's message. > I'm sorry, but this won't do. In a topos, equality is equality; you can't treat it "lazily". So a Cauchy real has to be an equivalence class of Cauchy sequences, and there is in general no way of choosing a canonical representative for it. Markov's principle would, I think (I haven't checked the details), suffice to give a canonical representation as a binary expansion with no infinite sequence of 1's, and then Dusko's argument would suffice to show that the Cauchy reals are Cauchy complete. But there are many toposes where Markov's principle fails. I doubt very much whether the Cauchy reals occur as a final coalgebra for anything, in any topos where they fail to coincide with the Dedekind reals, simply because the Dedekind reals are likely to be a coalgebra for the same endofunctor (and they're more "final" than the Cauchy reals). Incidentally, Peter Freyd and I worked out how to do his coalgebra construction constructively, and I showed that its final coalgebra is the Dedekind interval in any topos -- the proof is in the Elephant, at the end of section D4.7. Peter Johnstone