Re: Two constructivity questions

["Dr. P.T. Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>]

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