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