From mboxrd@z Thu Jan 1 00:00:00 1970
X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/58
Path: news.gmane.org!not-for-mail
From: "Prof. Peter Johnstone"
Newsgroups: gmane.science.mathematics.categories
Subject: Re: "Kantor dust"
Date: Mon, 9 Feb 2009 22:47:56 +0000 (GMT)
Message-ID:
Reply-To: "Prof. Peter Johnstone"
NNTP-Posting-Host: lo.gmane.org
Mime-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
X-Trace: ger.gmane.org 1234271586 25161 80.91.229.12 (10 Feb 2009 13:13:06 GMT)
X-Complaints-To: usenet@ger.gmane.org
NNTP-Posting-Date: Tue, 10 Feb 2009 13:13:06 +0000 (UTC)
To: Dusko Pavlovic ,
Original-X-From: categories@mta.ca Tue Feb 10 14:14:21 2009
Return-path:
Envelope-to: gsmc-categories@m.gmane.org
Original-Received: from mailserv.mta.ca ([138.73.1.1])
by lo.gmane.org with esmtp (Exim 4.50)
id 1LWsRP-0007fJ-Qn
for gsmc-categories@m.gmane.org; Tue, 10 Feb 2009 14:14:19 +0100
Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1LWrjN-0000Be-87
for categories-list@mta.ca; Tue, 10 Feb 2009 08:28:49 -0400
Original-Sender: categories@mta.ca
Precedence: bulk
Xref: news.gmane.org gmane.science.mathematics.categories:58
Archived-At:
On Mon, 9 Feb 2009, Dusko Pavlovic wrote:
> QUESTION 1: re peter johnstone's
>
>> > > In the topos of sheaves on the real line,
>> > > every function from [0,1) to N is constant,
>> > > yet there are obviously many other functions from N^N to N.
>> > > Thus N^N and [0,1) are not constructively isomorphic as sets,
>> > > so there is no way to give N^N the order type of [0,1)
>> > > constructively.
>
> are you claiming that this statement is true with respect to every base topos
> and every real line in it? (the discussion seems to have touched upon the
> various constructions of the various real lines. it would be nice to know
> where is the one, over which you build the topos, is coming from.)
>
That's actually a quote from Toby Bartels, not from me.
It's a statement about a topos built over the classical topos of sets;
the argument is a rather ad hoc one, and I'm not sure to what extent
it's possible to make it constructive. However, as I said elsewhere, I
prefer to work with the gros topos of spaces (i.e. sheaves on a suitable
full subcategory of spaces for the coverage consisting of jointly-
surjective families of open inclusions) and there it's quite clear
what you need: namely, Heine--Borel (equivalently, exponentiability
of R in your category of spaces). That's not true in all toposes;
you could try to get round it by basing your gros topos on locales
rather than spaces (the locale of formal reals being constructively
locally compact), but it's not clear (to me, at least) what the
result would actually mean if you based yourself on a topos where
the formal reals aren't spatial.
> QUESTION 2: is there a branch of constructivism that would reject as
> non-constructive the map N^N-->[0,1) obtained by interpreting the N^N as the
> coefficients of continued fractions?
>
I don't think there is any doubt that the map exists. The problem is that,
for most if not all schools of constructivism, it's wildly non-surjective.
Peter Johnstone