Two constructivity questions

[S.J.Vickers@open.ac.uk]

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?

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?

Steve Vickers
Department of Pure Maths
Faculty of Maths and Computing
The Open University
-----------
Tel: 01908-653144
Fax: 01908-652140
Web: http://mcs.open.ac.uk/sjv22