From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/2050 Path: news.gmane.org!not-for-mail From: "Dr. P.T. Johnstone" Newsgroups: gmane.science.mathematics.categories Subject: Re: Two constructivity questions Date: Sat, 8 Dec 2001 10:22:52 +0000 (GMT) Message-ID: References: NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Trace: ger.gmane.org 1241018369 2201 80.91.229.2 (29 Apr 2009 15:19:29 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:19:29 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Sat Dec 8 09:51:26 2001 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 08 Dec 2001 09:51:26 -0400 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 3.33 #2) id 16Chnt-0008EN-00 for categories-list@mta.ca; Sat, 08 Dec 2001 09:46:09 -0400 In-Reply-To: X-Scanner: exiscan *16CedC-00027r-00*FVUNSPUXi7I* http://duncanthrax.net/exiscan/ Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 23 Original-Lines: 58 Xref: news.gmane.org gmane.science.mathematics.categories:2050 Archived-At: On Fri, 7 Dec 2001 S.J.Vickers@open.ac.uk wrote: > Does any one know the answers to these questions? > > 1. Is trigonometry valid in toposes? (I'll be astonished if it isn't.) > 2. Does a polynomial over the complex field C have only finitely many roots? > > More precisely: > > 1. Over any topos with nno, let R be the locale of "formal reals", i.e. the > classifier for the geometric theory of Dedekind sections. > > Do sin, cos, arctan, etc. : R -> R exist and satisfy the expected > properties? Are there general results (e.g. on power series) that say Yes, > of course they do? The space of Dedekind reals is Cauchy-complete, so any convergent power series such as sin or cos defines an endomorphism of it. Moreover, provided (as in this case) we can calculate a "modulus of convergense" for the power series explicitly from a bound for x, it's easy to see that the construction x |--> sin x commutes with inverse image functors, so it must be induced by an endomorphism of the classifying topos (that is, of the locale of formal reals). > > 2. Consider the space S of square roots of the generic complex number. > Working over C, it is the locale corresponding to the squaring map s: C -> > C, z |-> z^2. The fibre over w is the space of square roots of w. > > s is not a local homeomorphism, so S is not a discrete locale. Hence we > can't say S is even a set, let alone a finite set in any of the known > senses. I don't believe its discretization pt(S) is Kuratowski finite > either. If I've calculated it correctly, it is S except for having an empty > stalk over zero (oops!), and there is no neighbourhood of zero on which an > enumeration can be given of all the elements of pt(S). > > On the other hand, S is a Stone locale - one can easily construct the sheaf > of Boolean algebras that is its lattice of compact opens. That sheaf of > Boolean algebras is not Kuratowski finite, nor even, it seems to me, a > subsheaf of a Kuratowski finite sheaf. > > So is there any sense at all in which S is finite? > That's a good question. I've never thought about notionss of finiteness for non-discrete locales (someone should!). For the set of points of S, I believe it should be what Peter Freyd called "R-finite" ("R" for "Russell"): intuitively, this means that there is a bound on the size of its K-finite subsets. (However, I don't have a proof of this.) R-finiteness is quite a lot weaker than \tilde{K}-finiteness (being locally a subobject of a K-finite object), but it's still a reasonably well-behaved notion of finiteness (e.g. it is preserved by functors which preserve all finite limits and colimits). Peter Johnstone