From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/39 Path: news.gmane.org!not-for-mail From: Vaughan Pratt Newsgroups: gmane.science.mathematics.categories Subject: Re: "Kantor dust" Date: Mon, 02 Feb 2009 15:43:16 -0800 Message-ID: Reply-To: Vaughan Pratt NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1233673332 30183 80.91.229.12 (3 Feb 2009 15:02:12 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Tue, 3 Feb 2009 15:02:12 +0000 (UTC) To: categories list Original-X-From: categories@mta.ca Tue Feb 03 16:03:19 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 1LUMo0-0003bQ-2O for gsmc-categories@m.gmane.org; Tue, 03 Feb 2009 16:03:16 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LUM8p-0003RT-Dy for categories-list@mta.ca; Tue, 03 Feb 2009 10:20:43 -0400 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:39 Archived-At: Prof. Peter Johnstone wrote: > A topos with a Cantor set object (i.e. a final coalgebra for FX = X+X) > necessarily has a natural number object. Observe that the Cantor set K > necessarily has a point (since 1 has an F-coalgebra structure), so the > isomorphism K+K \cong K yields a monomorphism K \to K and a point > disjoint from its image. From there on, use Corollary D5.1.3 in the > Elephant. Oh, of course: pick a point out of one half and recurse on the other. Very plausible that that would work in any topos, but it's great to be able to stare at an actual proof. Thank you! How about the converse: does N entail K? In any topos with NNO N the underlying object of the final coalgebra of FX = X+X is presumably 2^N. Does the Elephant prove that 2^N can be made a final coalgebra of X+X? And if so, what other coalgebras are brought into existence by N? For example can N^N be made a doubly inductive (inductive-coinductive) coalgebra encoding the lexicographic order that gives N^N the order type of the nonnegative reals? That would give a pretty direct construction of the usual topology of the real line in any topos with NNO. (This is the one-dimensional conception of the continuum, as opposed to the zero-dimensional conception preferred by descriptive set theorists, who take the continuum to be N^N with the ordinary product topology.) Does \Omega^N as the final coalgebra for FX = \Omega x X ever arise in practical situations where \Omega is more than just a pointed version of 1+1 as in Set, e.g. graph theory? Vaughan Pratt