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