Status of the fundamental theorem of algebra for the locale of real numbers

Question

In constructive mathematics without any choice at all, it is well known that the fundamental theorem of algebra cannot be proven for the Dedekind real numbers. On the other hand, Wim Ruitenberg showed in his paper Constructing Roots of Polynomials over the Complex Numbers that the fundamental theorem of algebra can be proven without choice at all for the real numbers defined as a quotient of Cauchy sequences of rational numbers. What is the status in constructive mathematics of the fundamental theorem of algebra for the locale of real numbers? I wonder if the fact that the locale of real numbers is not spatial has any impact on the status of the fundamental theorem of algebra.

Answer 1

I can see two issues of non-constructivity here, but I feel that they are both noise rather than central to the mathematics:

The leading coefficient of the polynomial could fail to be apart from zero, so that even the degree is indeterminate. But conventionally we assume that the leading coefficient is 1.

Then there could be double or multiple roots that fail to be apart. For example $x^2-\epsilon=0$ has two real roots $\pm\sqrt\epsilon$ if $\epsilon\geq 0$ but imaginary ones $\pm i\sqrt{-\epsilon}$ of $\epsilon\lt 0$.

If we talk about "the fundamental theorem of algebra", we usually mean we're working in $\mathbb C$. But then these two cases are close together and vary continuously with $\epsilon$, so there is no constructivity issue.

Talking about the "localic reals" suggests you might be interested in $\mathbb R$ instead.

Clearing these objections aside, I suggest you look at Gauss's second proof, which I translated, along with the commentary by Martin Hyland and summary by me in Eureka 45.

This translates any polynomial of even degree $N=2^n(2m+1)$ without repeated roots into one of degree $N(N-1)/2=2^{n-1}(2m+1)(2^n(2 m+1)-1)$ that encodes pairs of roots of the original.

(I'm sorry, but I forget the details of this translation, so you'll need to look at the sources, but I assure you that it is "elementary" in the technical sense.)

Gauss does begin this paper by adapting the Euclidean algorithm to polynomials (I surmise that he was the first to do so, but someone might correct me) in order to find the highest common factor of the polynomial and its derivative, thereby dealing with the question of repeated roots.

Repeating the translation, we obtain a polynomial of (much higher) odd degree, along with a lot of quadratics.

The odd degree polynomial has a root by the Intermediate Value Theorem, where the root may be expressed as a Dedekind cut..

Yes, I know that the IVT is not constructive in general, because there are functions that "hover" or are "locally constant", but polynomials do not do this.

As for roots of quadratics, I am sure that any MO reader can recite the formula in their sleep.