Two constructivity questions

Two constructivity questions

[S.J.Vickers]

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

Re: Two constructivity questions

[Dr. P.T. Johnstone]

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

Re: Two constructivity questions

[S Vickers]

As before, let S be the Stone locale of square roots of the generic complex
number. The question is, In what sense can S be considered finite?

Here is one idea that occurs to me.

If a set is acted on transitively by a finite group, then classically it
must be finite (and I dare say some constructive statement of this is also
true).

S is acted on by the discrete group {+1, -1} (by multiplication in C).
Hence if that action can be considered transitive in some way, that would
be a finiteness property of S (or, rather, finiteness _structure_ on S).

If a: S x {+1, -1}  -> S is the action, then I believe I can prove (by
techniques involving the upper powerlocale) that

   <fst, a> : S x {+1, -1}  -> S x S

is a proper surjection. This would seem to be a natural way to capture
transitivity of a and hence a finiteness property of S.

More generally, if an action on a locale by a finite group has only
finitely many orbits (using the above idea to specify transitivity on the
orbits), then that would be a finiteness property of the locale.

One might ask whether, by Galois theory, this can be applied to arbitrary
polynomials over C.

Steve Vickers.