Re: Two constructivity questions

[S Vickers <s.j.vickers@open.ac.uk>]

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.