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