Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I wrote out a proof which uses very little machinery at fundamental theorem of algebra. It is just about at the point where it is not only short and rigorous, but could be understood by an eighteenth-century mathematician. (Nothing important, just fun!)
Thanks, I added a bit about the theorem’s status in constructive mathematics.
This led me to write square root, which is where the constructive difficulties in both the FTA and the quadratic formula lie.
Added link to root to fundamental theorem of algebra and added a stub. But Toby will want to go over it.
How do you define the absolute value constructively? I guess I can see how to do it for real numbers as constructed in terms of rational numbers, since we know what the absolute value of a rational number is, but did you have anything more general in mind?
In general, there’s no constructive way to define absolute value in a linearly ordered field. (At least, I don’t see how to do it, although I don’t actually know any counterexamples.) That why at one point I include the existence of an absolute value in the hypothesis of a statement on square root. (Perhaps the existence of an absolute value should be an extra hypothesis in the constructive definition of a linearly ordered field? I haven’t thought about this very much.)
However, in a real-closed field (which is what matters for the FTA), you can define absolute value as and prove the usual properties. At one point I had the existence of an absolute value as a redundant condition on a real-closed field somewhere on one of these pages, but I think I removed this quickly enough that it doesn’t even show up in the history.
There is something wrong with constructive mathematics if it can’t prove the quadratic formula =.
Harry, as I understand it, the problem is choosing a square root. Paul Taylor puts it well in his Practical Foundations of Mathematics: in for example the topos of sheaves over , there is a torsor given by the squaring map . This is epi, so that in the internal logic the proposition “each element of has a square root” is true, but insofar as there is no global section of the squaring map, you can’t “choose a square root” (in the sheaf context the choosing is continuous choice). Taylor refers to Buridan’s ass here, saying here are two square roots that look equally inviting to the donkey, and he cannot choose between them.
Let’s put that example somewhere into an Lab entry.
I think with the comparatively huge amount of remarks on constructive math that we do have on the Lab, it would be very good to have a page or two that spells out plenty of examples of for what this is good for . Lots of examples where one wants to work in a topos by ordinary reasoning but has to stick to constructive arguments. I think such a list of examples will add considerable value to what we already have (thanks mostly to Toby).
Let’s put that example somewhere into an Lab entry.
There’s already an example at square root, which is the topos of sheaves on the real line, although without any of Taylor’s poetic language about Buridan’s ass.
However, I’m afraid that I’ve never understood Taylor’s example (crappy online version). Taylor seems to argue that because there is no function in constructive mathematics (which is true), there is no proof of in constructive, and this I cannot accept (since it can be proved in the language of the free pretopos with NNO, which is the basic non-finitist variety of constructive mathematics). What is true is that there is no proof of in constructive mathematics (and in particular in the internal language of the sheaf topos over the real line), but this is evidently not what he’s talking about, since he mentions only and not . His main point seems to be a philosophical one about the difference between mathematical objects and their codings (which can be resolved by passing from a category of presets to a pretopos of sets).
That you cannot prove (without the LLPO) seems more like Buridan’s ass to me. That you cannot prove , on the other hand, seems unlike Buridan’s ass; it is inherently -dimensional. (Recall that you can prove ; in fact, you can even prove the existence of a function .) The failure is not that you are being pulled in two directions, but rather that you are always spinning in circles.
As far as the relevance of continuous functions goes, it’s immaterial that there is no continuous section of the squaring map or ; what matters is whether there is a continuous partial section on any sufficiently small open set. (After all, we’re talking about sheaves here!) For , there is one on any proper open subset; for , there is none on any neighbourhood of , and that is where the problem lies.
The failure is not that you are being pulled in two directions, but rather that you are always spinning in circles.
Yes, I agree with you now that the Buridan’s ass metaphor is not very apt.
For , there is one on any proper open subset; for , there is none on any neighbourhood of 0, and that is where the problem lies.
Ah! Thanks for clarifying that; the issue is that the squaring map on the complex numbers is ramified at .
the issue is that the squaring map on the complex numbers is ramified at
Yes, exactly, although I’m not fluent in algebraic geometry, so I don’t think to say it that way.
I’ve edited #10 to better reflect what Taylor wrote, although it mostly affects the bits in parentheses.
@ Harry
There is something wrong with constructive mathematics if it can’t prove the quadratic formula =.
It can prove the quadratic formula; the question is whether one can prove that it always applies, that is whether one can prove that every complex number has a complex square root. Most schools of constructive mathematics can prove this, but Fred Richman’s school cannot; there is something wrong with it.
And there is something wrong with classical mathematics too, since it can’t prove that every subset of the real line is measurable, that every function from the unit interval to the real line is uniformly continuous, etc etc etc. You can’t have everything.
@Toby:
Every function from the unit interval to the real line is uniformly continuous
That isn’t even intuitively true. (Heaviside step function)
Every subset of the real line is measurable
Why should this be true? It seems pretty unintuitive to me, but I also have some harsh opinions of measure theory in general (i.e. that it’s not the canonical “right” notion).
Harry, I hope you’re not doubting that Toby knows what he’s talking about with regard to constructive mathematics! “Every function from the unit interval to the real line is uniformly continuous” is meant to be interpreted in certain constructive frameworks, such as a suitable world for doing synthetic differential geometry.
@Todd: Sure, but I’m saying that such a conclusion is not at all intuitive, while the quadratic formula is intuitively true as a result of plane geometry as related to completing the square.
What I was talking about in my original post was that if there is some proposed system of axioms for doing mathematics in general, it should at least be able to prove results that are intuitively true (wasn’t this Brouwer’s original reason for coming up with it?).
I was using “should be true” to mean “should be true in any reasonably useful system of axioms”.
Brouwer found the facts cited by Toby (at least, the first one; I don’t know whether he knew any measure theory) to be intuitively true. The problem with the Heaviside step function is that it is not defined on the whole real line. Consider the real number with decimal expansion , where is if is a sum of two primes, and otherwise. What is ? (Or, if your convention for makes that an easy question, what is ?) I’ll be very impressed if you can give a definite answer.
For the other, the existence of nonmeasurable sets has many consequences that many people find unintuitive, such as the Banach-Tarski paradox and the behavior of probability on infinite domains.
(That said, I personally still do think the most convincing argument for using constructive reasoning is that it stays valid when you move into an arbitrary topos. I’m just saying that different people might have different “intuitions” from you.)
I’ll let Toby respond. “Intuitively true” depends on the intuitions one has.
@Mike: Are we thinking of the same Heaviside step function? I don’t understand what you’re getting at.
Harry, a more basic point that should be borne in mind is that is not constructively true, since we do not assume excluded middle. So the Heaviside function is not definable in a typical constructive context such as the internal logic of a topos.
This relates to Mike’s example because in intuitionism or constructive mathematics, existence is established by exhibiting a witness or witnessing proof. There is not (as yet) a witnessing proof of Goldbach’s conjecture.
So the constructive reals don’t satisfy trichotomy (and are therefore not an ordered field)?
@Harry: field
If you look at the category of (pre?)sheaves on a category with a terminal object, aren’t all fields discrete?
Doesn’t that cover basically every interesting case?
For instance, in simplicial rings, every simplicial ideal is contained in a maximal ideal (every SCR surjects onto a simplicial field), and all simplicial fields are discrete.
But the reals as usually realised (Dedekind or Cauchy, say) are not discrete. For me, Heyting fields (if I was pushed to make a stab at a useful internalised concept) are the most useful concept. To quote from field,
A residue field is a Heyting field if and only if it is a local ring. Furthermore, the quotient ring (or ‘residue ring’) of any local ring by its ideal of noninvertible elements is a Heyting field; in particular, it is a residue field (hence that name). On the other hand, not every residue field is even a local ring (the MacNeille reals are not), so not every residue field is the residue ring of any local ring.
Since local rings are such a useful concept, I would like my fields to be local rings. Note that the Dedekind reals form a Heyting field.
At field there is also the statement
another disadvantage is that this is not a coherent axiom and so cannot be internalized in as many categories.
but it doesn’t say what is needed of a category to internalise the definition of Heyting field. Presumably one needs an internal apartness relation…
A field is an injective ring or something (a ring such that every morphism is injective). Recall that the rings of a topos are classified by geometric morphisms into , the topos of presheaves on affine schemes of finite type over spec Z.
Surely the correct way to define algebraic notions is to resort to descriptions of objects by their morphisms, rather than by their elements, no?
If you look at the category of (pre?)sheaves on a category with a terminal object, aren’t all fields discrete?
Definitely not. Look at the category of sheaves on say , and take the sheaf of Dedekind reals (= sheaf of continuous sections of the projection ). If broke up as a coproduct consisting of a zero part and a nonzero part, then the pullback of this coproduct along any global section would give a coproduct decomposition of . Now there is no nontrivial coproduct decomposition of the terminal 1 since nontrivial subobjects of 1 are open subobjects and the space is connected. We would thus infer that any continuous section is either nonzero everywhere or zero everywhere, but that’s obviously false.
Oh, then why do simplicial sets work?
I believe the object of Dedekind reals in presheaf toposes are indeed discrete in the sense we are talking about, because they are given by the constant presheaf , where is the diagonal map. Since the classical reals in admit the coproduct decomposition into a zero and invertible part, and since preserves coproducts, we get a coproduct decomposition for in .
Every function from the unit interval to the real line is uniformly continuous
That isn’t even intuitively true. (Heaviside step function)
Well, that depends on your intuition! There are certainly people who would find it intuitively true, possibly including such non-idiots as Richard Feynman. (I’m having trouble finding this anecdote online, so I can’t tell you just how convoluted a function it was that violated Feynman’s intuition.) In the 19th century, there was a lot of debate over what constitutes a function, with even some uniformly continuous ones coming under fire. While the modern notion of function is obviously the correct notion of something, it’s not clear that it really captures the original intuition (of Leibniz et al) of what a function is.
In any case, constructive mathematicians today would agree that defines a dandy partial function; the question is whether it extends to a total function.
A more interesting question is whether the Heaviside step function (which is certainly an important mathematical object, regardless of whether it is technically a function) is best understood as an almost-everywhere-defined measurable function or as a distribution (one whose derivative is the Dirac delta function, which is not technically a function). Both can be done constructively; even classically, there is no need to worry about exactly how to define , which irrelevant to the point of the thing.
Every subset of the real line is measurable
Why should this be true? It seems pretty unintuitive to me, but I also have some harsh opinions of measure theory in general (i.e. that it’s not the canonical “right” notion).
The main reason why it should be true is that it makes the theory of the Lebesgue integral much nicer. Classical mathematics is almost as bad as constructive mathematics, insisting on piddling details like checking whether a set is measurable. Much as you need to know about metric spaces to understand Fred Richman’s version of the fundamental theorem of algebra, so you have to know about -algebras to understand classical measure theory on the real line. It’s so much easier not to bother with such complications.
It also is intuitive to a lot of people, certainly all those people who find the Banach–Tarski paradox paradoxical. There was even an article in the American Mathematical Monthly about 10 years ago advocating that an undergraduate course be taught in dream mathematics, a style of mathematics that makes this assumption.
Note that dream mathematics is not constructive; although I think that its two big nonclassical axioms (this one and a similar one about the Borel property) can be phrased in such a way as to make it compatible with constructive mathematics, they are still in themselves rather nonconstructive axioms. The reasons to prefer classical analysis over constructive analysis are also reasons to prefer dream analysis over classical analysis: things that 19th-century analysts expected to be true (and which many students today expect until, if ever, they learn otherwise) can in fact be proved.
@Toby - what exactly do you need for an internal Heyting field object?
@ David
I believe that the answer is that you really shouldn’t bother with them; you should just use internal local ring objects. (So you need only coherent logic.)
Every local ring comes with an apartness relation: iff is invertible (which can be stated in coherent logic); we simply don’t have that if this fails (assuming that our logic is strong enough even to say this). But if we define a ‘field’ to be a local ring and a ‘field homomorphism’ to be ring homomorphism that reflects (which can also be stated in coherent logic), then the resulting category is equivalent (in any Heyting pretopos, say) to the category of Heyting fields. So if our logic is too weak to define a field directly, then we can just use this category of local rings and -reflecting homomorphisms.
Or something like that; having written this, I now see some problems with it, but I think that they can be overcome.
A field is an injective ring or something (a ring such that every morphism is injective).
I’m not sure what theorem you really mean here, since neither of what you say above is quite correct and I can’t figure out quite how to fix them, but I wouldn’t be surprised if it’s constructively valid.
I know this theorem: If is a field and is a nontrivial ring, then every ring homomorphism from to is an injection. The proof that immediately comes to me is constructive (although that may be because I’m used to thinking constructively first), if by ‘field’ we mean a Heyting field and by ‘nontrivial’ we mean that it is false that (which the weakest way of saying this, constructively, so the strongest possible theorem).
So the constructive reals don’t satisfy trichotomy (and are therefore not an ordered field)?
@Harry: field
And more specifically: ordered field (which references also linear order).
@Toby: I’m saying that regardless of how you want to state the definition of a field object internally, we can define a field object externally to be a nontrivial ring object such that given any other nontrivial ring object , any map is injective. At least in a Grothendieck topos (which appears to be the only case that non-constructivists/non-logicians really have any interest), what’s wrong with this definition?
I was using “should be true” to mean “should be true in any reasonably useful system of axioms”.
And what does that mean!?
In my opinion, both of these statements should be true:
Unfortunately, they cannot both be true, on pain of contradiction. That is why there are different varieties of mathematics (even though most mathematicians are still taught that only one variety is true, as if that meant anything).
what’s wrong with this definition?
It’s not quite anything that you said before.
It looks like a fine definition to me, although there may be some subtleties about what ‘nontrivial’ means. However, I haven’t yet checked the converse condition (that any ring with this property must be a field). The field of real numbers certainly satisfies it (constructively, in particular in any Grothendieck topos).
At least in a Grothendieck topos (which appears to be the only case that non-constructivists/non-logicians really have any interest)
If you mean that Grothendieck toposes are the only context where anybody other than a constructivist or a logician uses intuitionistic logic, then that’s definitely not true! What about synthetic differential geometry? What about David Roberts’s (and my) work on gerbe theory as doing things internal to a category such as (although fields don’t seem to come up there)? There’s a lot more to internalization than Grothendieck toposes.
…we can define a field object externally to be a nontrivial ring object such that given any other nontrivial ring object , any map is injective. At least in a Grothendieck topos (which appears to be the only case that non-constructivists/non-logicians really have any interest), what’s wrong with this definition?
What do you mean when you say a map is injective in an general category (say with finite limits)? Do you mean something like the opposite of projective, or a monomorphism?
Monomorphism should work here; it corresponds to set-theoretically injective in .
Yes, that would make sense given the ’external’ point of view.
I thought synthetic differential geometry was usually done in a Grothendieck topos of sheaves on a site of smooth loci. In fact, I don’t think I’ve ever seen any other model for it. Of course you can write down a list of axioms and not bother about models, but if you are someone like Harry, then you may always want to think in terms of models.
I agree with the general point that there’s more to internalization that Grothendieck toposes, though. As another example, computer scientists are interested in “realizability” toposes like the effective topos, which are not Grothendieck. And (at least some of) nonstandard analysis can be viewed as taking place in a filterquotient topos, also not Grothendieck. The constructible universe can be regarded as another non-Grothendieck topos that at least set-theorists are interested in. And what about FinSet, where certainly much of combinatorics takes place?
Toby may have meant Diff in the sense of manifolds (long shot, I know) - I’ve always kept in mind non-finitely complete ambient categories for this very reason, to connect with classical theory.
@ Mike:
Yes, I was just thinking of the axioms, but you’re right that the models are usually Grothendieck toposes, so that’s not a counterexample to Harry’s claim.
@ David:
Yes, by I meant what the Lab calls Diff, the category of manifolds that one learns about in undergraduate courses. I like that building internal groupoid theory even within that ill behaved category recreates all of the generality of differentiable stacks.
Colin: yes, this is part of the general threory of real closed fields. In fact, it doesn’t even have to be degree 2; that’s a bonus result even if we assume the a priori weaker hypothesis of finite degree. A good search term is “Artin-Schreier theorem”. There’s an exposition in Lang’s Algebra.
@Toby: I am late to the discussion :-), but what problems do you see with your #32? I didn’t know it before, but it looks perfectly fine to me.
A small remark: Homomorphisms between local rings which reflect the apartness relation defined by iff is invertible also go by the name “local homomorphism”, of course.
@Ingo: I no longer remember the problems, and I can no longer find them! Perhaps they don't exist after all.
@Colin: In the last line of the proof of the Theorem, we have ‘But has no nontrivial quadratic extensions by the lemma that follows’, so it's used there.
@Toby: As I was just about to add the observation to local ring, I noticed where the problem might hide: Apparently, some people require that the apartness relation of a Heyting field is tight (for instance Richman et at. in their book, and you when you created the entry :-), but not the nLab at field); but the natural apartness relation on a local ring is not tight in general (it is if and only if the local ring is even a residue field). I don’t know what the consensus is.
The definition of Heyting field is supposed to require it to be tight (so I just edited it). But that's in a context where we have full (intuitionistic) logic at our disposal. If we only have coherent logic, then we can stick to local rings, but we have to count two local rings as equivalent if their residue fields are the same (which can be expressed using only coherent logic without explicit reference to these residue fields).
Now I think that I found the problem: it's tricky to define properly what a morphism of fields is when using local rings. We have to specify the information that would define a ring homomorphism between the local rings' residue fields without direct reference to these residue fields (or otherwise using non-coherent logic). Probably I should try to write that up at local ring.
added a history section and some historical references, by copying-and-slightly-editing what David Roberts compiled here but is too shy to add to the Lab himself.
Urs - I was going to add it tomorrow (I should be offline now, in any case). That said, as a history it is hopelessly biased and incomplete, centered purely on the elementariness of Gauss’ second proof.
I’ve been adding a few glosses to the proof via advanced calculus. From reading around a little, it looks like this may be close to the proof given by Argand in 1814 (which apparently is often considered the first rigorous proof, pace Gauss – I may add to the history section at some point). I have my doubts I can make the proof much more elementary than it is currently. Meanwhile, David Roberts is asking about the reverse mathematics of FTA at MO, which I don’t know about.
Apparently FTA is provable in .
EDIT: I’ve added this at http://ncatlab.org/nlab/show/fundamental+theorem+of+algebra#in_weak_foundations
Great! Thanks for looking into this.
Wrong!! Please look up the definition of “real closed”. In particular, is not real closed. I am rolling back.
I didn’t claim it’s “most likely wrong”. I didn’t think it was provable constructively for any kind of real numbers, but I could easily be misremembering.
But if it is true, it would be good to have a citation. And also for the claim earlier that the usage of problematic results “in this proof is fine”.
Unrelated, but the webpage for Allen Hatcher’s Algebraic Topology textbook which has a classical proof of the fundamental theorem of algebra and linked in the mathoverflow is no longer available. One could still access the textbook though the Wayback Machine for that website https://web.archive.org/web/20140623021228/https://math.cornell.edu/~hatcher/AT/ATpage.html
Re #63: It is available: https://pi.math.cornell.edu/~hatcher/AT/ATpage.html
Some helpful people on the HoTT Zulip have provided some references. When editing is possible again, we should add them to the lab.
Why being so vague (unnamed people on an unlinked webpage have provided unspecified references): If you just record the reference here in the nForum thread, then there is a better chance that somebody recovers them in the future.
Wim Ruitenberg, Constructing Roots of Polynomials over the Complex Numbers, Computational Aspects of Lie Group Representations and Related Topics, CWI Tract, Vol. 84, Centre for Mathematics and Computer Science, Amsterdam, 1991, pp. 107–128.
That polynomial functions satisfy the exact intermediate value only when weak countable choice is valid.
Anonymous
Toby Bartels says
In general, there’s no constructive way to define absolute value in a linearly ordered field.
There is, by using subtraction and the maximum/join based upon the inherent l-group structure on the linearly ordered field. Otherwise, one wouldn’t be able to define Cauchy sequences in Archimedean ordered fields, necessary to construct i.e. the Cauchy real numbers.
However, in a real-closed field (which is what matters for the FTA), you can define absolute value as and prove the usual properties.
This has issues in constructive mathematics: 1. What is a good definition of a real-closed field, and 2. could you prove that your set of real numbers is a real-closed field based upon your definition of a real-closed field?
Wim Ruitenberg’s paper proves a different “Fundamental Theorem of Algebra” (theorem 3.13) than the one usually proven in classical mathematics (the complex numbers are algebraically closed or integrally closed). Ruitenberg states that:
Theorem 3.13 does not extend to all of : We cannot find a continuous solution to the equation when is near .
But the classical FTA does extend to all of .
The problem is that all notions of in constructive mathematics, whether the modulated Cauchy real numbers talked about in this article, or the Dedekind real numbers, are only Heyting fields, not discrete fields. The equation has a solution when or , but because is not discrete, one cannot show that or for all .
In the section titled “in constructive mathematics” the following sentence appears:
In fact, this fails in certain topoi, such as sheaves over , because that the complex numbers have a continuous square root over can only be proven in the presence of weak countable choice.
For the Cauchy complex numbers, surely one just needs the limited principle of omniscience, which implies that both the Cauchy real numbers and the Cauchy complex numbers are discrete fields.
The link to Fred Richman’s website in the reference
doesn’t work anymore.
Anonymouse
Found the doi and pdf for the Fred Richman paper:
Anonymouse
added also pointer to:
The statement that “A proof that Cauchy sequences of rational numbers satisfy the fundamental theorem of algebra:” which appeared in the references section above the Richman paper on the FTA doesn’t actually apply to Richman’s paper. Fred Richman used the Dedekind real numbers throughout the paper and gave multiple reasons why Cauchy sequences of rational numbers are unsuitable for constructive analysis without choice.
Anonymouse
changed higher algebra - contents to algebra - contents in context sidebar
Anonymouse
1 to 79 of 79