Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics comma complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorTodd_Trimble
    • CommentTimeNov 27th 2010

    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!)

    • CommentRowNumber2.
    • CommentAuthorTobyBartels
    • CommentTimeNov 28th 2010

    Thanks, I added a bit about the theorem’s status in constructive mathematics.

    • CommentRowNumber3.
    • CommentAuthorTobyBartels
    • CommentTimeNov 29th 2010

    This led me to write square root, which is where the constructive difficulties in both the FTA and the quadratic formula lie.

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeNov 29th 2010

    Added link to root to fundamental theorem of algebra and added a stub. But Toby will want to go over it.

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeNov 29th 2010

    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?

    • CommentRowNumber6.
    • CommentAuthorTobyBartels
    • CommentTimeNov 30th 2010

    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 |x|x 2{|x|} \coloneqq \sqrt{x^2} 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.

    • CommentRowNumber7.
    • CommentAuthorHarry Gindi
    • CommentTimeNov 30th 2010

    There is something wrong with constructive mathematics if it can’t prove the quadratic formula =.

    • CommentRowNumber8.
    • CommentAuthorTodd_Trimble
    • CommentTimeNov 30th 2010

    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 S 1S^1, there is a 2\mathbb{Z}_2 torsor given by the squaring map S 1S 1S^1 \to S^1. This is epi, so that in the internal logic the proposition “each element of S 1S^1 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.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeNov 30th 2010

    Let’s put that example somewhere into an nnLab entry.

    I think with the comparatively huge amount of remarks on constructive math that we do have on the nnLab, 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).

    • CommentRowNumber10.
    • CommentAuthorTobyBartels
    • CommentTimeDec 1st 2010
    • (edited Dec 4th 2010)

    Let’s put that example somewhere into an nnLab 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 :S 1S 1\sqrt{}\colon S^1 \to S^1 in constructive mathematics (which is true), there is no proof of y:S 1,x:S 1,y=x 2\forall y\colon S^1,\; \exists x\colon S^1,\; y = x^2 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 y:,x:,y=x 2\forall y\colon \mathbb{C},\; \exists x\colon \mathbb{C},\; y = x^2 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 S 1S^1 and not \mathbb{C}. 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 x 2=xx 2=x\sqrt{x^2} = x \;\vee\; \sqrt{x^2} = -x (without the LLPO) seems more like Buridan’s ass to me. That you cannot prove y:,x:,y=x 2\forall y\colon \mathbb{C},\; \exists x\colon \mathbb{C},\; y = x^2, on the other hand, seems unlike Buridan’s ass; it is inherently 22-dimensional. (Recall that you can prove y:,x:,y=x 2\forall y\colon \mathbb{R},\; \exists x\colon \mathbb{C},\; y = x^2; in fact, you can even prove the existence of a function :\sqrt{}\colon \mathbb{R} \to \mathbb{C}.) 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 S 1S 1S^1 \to S^1 or \mathbb{C} \to \mathbb{C}; 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 S 1S 1S^1 \to S^1, there is one on any proper open subset; for \mathbb{C} \to \mathbb{C}, there is none on any neighbourhood of 00, and that is where the problem lies.

    • CommentRowNumber11.
    • CommentAuthorTodd_Trimble
    • CommentTimeDec 1st 2010
    • (edited Dec 1st 2010)

    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 S 1S 1S^1 \to S^1, there is one on any proper open subset; for \mathbb{C} \to \mathbb{C}, 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 00.

    • CommentRowNumber12.
    • CommentAuthorTobyBartels
    • CommentTimeDec 3rd 2010

    the issue is that the squaring map on the complex numbers is ramified at 00

    Yes, exactly, although I’m not fluent in algebraic geometry, so I don’t think to say it that way.

    • CommentRowNumber13.
    • CommentAuthorTobyBartels
    • CommentTimeDec 4th 2010

    I’ve edited #10 to better reflect what Taylor wrote, although it mostly affects the bits in parentheses.

    • CommentRowNumber14.
    • CommentAuthorTobyBartels
    • CommentTimeDec 4th 2010

    @ 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.

    • CommentRowNumber15.
    • CommentAuthorHarry Gindi
    • CommentTimeDec 5th 2010
    • (edited Dec 5th 2010)

    @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).

    • CommentRowNumber16.
    • CommentAuthorTodd_Trimble
    • CommentTimeDec 5th 2010

    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.

    • CommentRowNumber17.
    • CommentAuthorHarry Gindi
    • CommentTimeDec 5th 2010
    • (edited Dec 5th 2010)

    @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”.

    • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeDec 5th 2010

    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 HH is that it is not defined on the whole real line. Consider the real number xx with decimal expansion 0.x 1x 2x 3x 40.x_1 x_2 x_3 x_4 \dots, where x nx_n is 00 if 2n+22n+2 is a sum of two primes, and 11 otherwise. What is H(x)H(x)? (Or, if your convention for H(0)H(0) makes that an easy question, what is H(x)H(-x)?) 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.)

    • CommentRowNumber19.
    • CommentAuthorTodd_Trimble
    • CommentTimeDec 5th 2010

    I’ll let Toby respond. “Intuitively true” depends on the intuitions one has.

    • CommentRowNumber20.
    • CommentAuthorHarry Gindi
    • CommentTimeDec 5th 2010
    • (edited Dec 5th 2010)

    @Mike: Are we thinking of the same Heaviside step function? I don’t understand what you’re getting at.

    • CommentRowNumber21.
    • CommentAuthorTodd_Trimble
    • CommentTimeDec 5th 2010

    Harry, a more basic point that should be borne in mind is that x0x<0x \geq 0 \vee x \lt 0 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.

    • CommentRowNumber22.
    • CommentAuthorHarry Gindi
    • CommentTimeDec 5th 2010
    • (edited Dec 5th 2010)

    So the constructive reals don’t satisfy trichotomy (and are therefore not an ordered field)?

    • CommentRowNumber23.
    • CommentAuthorDavidRoberts
    • CommentTimeDec 5th 2010

    @Harry: field

    • CommentRowNumber24.
    • CommentAuthorHarry Gindi
    • CommentTimeDec 5th 2010
    • (edited Dec 5th 2010)

    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.

    • CommentRowNumber25.
    • CommentAuthorDavidRoberts
    • CommentTimeDec 6th 2010
    • (edited Dec 6th 2010)

    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

    • CommentRowNumber26.
    • CommentAuthorHarry Gindi
    • CommentTimeDec 6th 2010
    • (edited Dec 6th 2010)

    A field is an injective ring or something (a ring kk such that every morphism kRk\to R is injective). Recall that the rings of a topos are classified by geometric morphisms into 𝔖\mathfrak{S}, 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?

    • CommentRowNumber27.
    • CommentAuthorTodd_Trimble
    • CommentTimeDec 6th 2010
    • (edited Dec 6th 2010)

    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 [0,1][0, 1], and take the sheaf RR of Dedekind reals (= sheaf of continuous sections of the projection ×[0,1][0,1]\mathbb{R} \times [0, 1] \to [0, 1]). If RR broke up as a coproduct consisting of a zero part and a nonzero part, then the pullback of this coproduct along any global section 1R1 \to R would give a coproduct decomposition of 11. Now there is no nontrivial coproduct decomposition of the terminal 1 since nontrivial subobjects of 1 are open subobjects and the space [0,1][0, 1] is connected. We would thus infer that any continuous section is either nonzero everywhere or zero everywhere, but that’s obviously false.

    • CommentRowNumber28.
    • CommentAuthorHarry Gindi
    • CommentTimeDec 6th 2010

    Oh, then why do simplicial sets work?

    • CommentRowNumber29.
    • CommentAuthorTodd_Trimble
    • CommentTimeDec 6th 2010

    I believe the object of Dedekind reals RR in presheaf toposes Set C opSet^{C^{op}} are indeed discrete in the sense we are talking about, because they are given by the constant presheaf Δ()\Delta(\mathbb{R}), where Δ:SetSet C op\Delta: Set \to Set^{C^{op}} is the diagonal map. Since the classical reals in SetSet admit the coproduct decomposition into a zero and invertible part, and since Δ\Delta preserves coproducts, we get a coproduct decomposition for RR in Set C opSet^{C^{op}}.

    • CommentRowNumber30.
    • CommentAuthorTobyBartels
    • CommentTimeDec 6th 2010

    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 H(x){0 x<0 1 x>0H(x) \coloneqq \left\{\array{0 & x \lt 0 \\ 1 & x \gt 0}\right. 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 H(0)H(0), 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 σ\sigma-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.

    • CommentRowNumber31.
    • CommentAuthorDavidRoberts
    • CommentTimeDec 6th 2010

    @Toby - what exactly do you need for an internal Heyting field object?

    • CommentRowNumber32.
    • CommentAuthorTobyBartels
    • CommentTimeDec 6th 2010
    • (edited Dec 6th 2010)

    @ 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: x#yx \# y iff xyx - y is invertible (which can be stated in coherent logic); we simply don’t have that x=yx = y 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.

    • CommentRowNumber33.
    • CommentAuthorTobyBartels
    • CommentTimeDec 6th 2010
    • (edited Dec 6th 2010)

    A field is an injective ring or something (a ring kk such that every morphism kRk\to R 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 KK is a field and RR is a nontrivial ring, then every ring homomorphism from KK to RR 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 0=10 = 1 (which the weakest way of saying this, constructively, so the strongest possible theorem).

    • CommentRowNumber34.
    • CommentAuthorTobyBartels
    • CommentTimeDec 6th 2010

    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).

    • CommentRowNumber35.
    • CommentAuthorHarry Gindi
    • CommentTimeDec 6th 2010

    @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 kk such that given any other nontrivial ring object RR, any map kRk\to R 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?

    • CommentRowNumber36.
    • CommentAuthorTobyBartels
    • CommentTimeDec 6th 2010

    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:

    • Any partial function from the unit interval to the real line (indeed, from any set to any inhabited set) can be extended to a function.
    • Any function from the unit interval to the real line (indeed, from any compact space to any complete space) is uniformly continuous.

    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).

    • CommentRowNumber37.
    • CommentAuthorTobyBartels
    • CommentTimeDec 6th 2010

    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 DiffDiff (although fields don’t seem to come up there)? There’s a lot more to internalization than Grothendieck toposes.

    • CommentRowNumber38.
    • CommentAuthorDavidRoberts
    • CommentTimeDec 6th 2010

    …we can define a field object externally to be a nontrivial ring object kk such that given any other nontrivial ring object RR, any map kRk\to R 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?

    • CommentRowNumber39.
    • CommentAuthorTobyBartels
    • CommentTimeDec 6th 2010

    Monomorphism should work here; it corresponds to set-theoretically injective in RingRing.

    • CommentRowNumber40.
    • CommentAuthorDavidRoberts
    • CommentTimeDec 6th 2010

    Yes, that would make sense given the ’external’ point of view.

    • CommentRowNumber41.
    • CommentAuthorMike Shulman
    • CommentTimeDec 6th 2010

    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?

    • CommentRowNumber42.
    • CommentAuthorDavidRoberts
    • CommentTimeDec 7th 2010

    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.

    • CommentRowNumber43.
    • CommentAuthorTobyBartels
    • CommentTimeDec 7th 2010

    @ 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 DiffDiff 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.

    • CommentRowNumber44.
    • CommentAuthorColin Tan
    • CommentTimeDec 19th 2013
    I like the proof that the extension of a real closed field by i is algebraically closed. Is there a converse to this statement? Such as, if K/L is a Galois field extension of degree 2 and K is algebraically closed of characteristic 0, then L is real closed?
    • CommentRowNumber45.
    • CommentAuthorTodd_Trimble
    • CommentTimeDec 19th 2013

    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.

  1. @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 x#yx # y iff xyx-y is invertible also go by the name “local homomorphism”, of course.

    • CommentRowNumber47.
    • CommentAuthorColin Tan
    • CommentTimeDec 21st 2013
    I'm reading the section which gives an algebraic proof via real closed fields. I'm wondering: is Lemma 1 used to prove the Theorem?
    • CommentRowNumber48.
    • CommentAuthorTobyBartels
    • CommentTimeDec 21st 2013

    @Ingo: I no longer remember the problems, and I can no longer find them! Perhaps they don't exist after all.

    • CommentRowNumber49.
    • CommentAuthorTobyBartels
    • CommentTimeDec 21st 2013

    @Colin: In the last line of the proof of the Theorem, we have ‘But KK has no nontrivial quadratic extensions by the lemma that follows’, so it's used there.

  2. @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.

    • CommentRowNumber51.
    • CommentAuthorTobyBartels
    • CommentTimeDec 24th 2013

    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.

    • CommentRowNumber52.
    • CommentAuthorUrs
    • CommentTimeMay 5th 2014
    • (edited May 5th 2014)

    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 nnLab himself.

    • CommentRowNumber53.
    • CommentAuthorDavidRoberts
    • CommentTimeMay 5th 2014

    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.

    • CommentRowNumber54.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 29th 2015
    • (edited Jun 29th 2015)

    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.

    • CommentRowNumber55.
    • CommentAuthorDavidRoberts
    • CommentTimeJun 30th 2015
    • (edited Jun 30th 2015)
    • CommentRowNumber56.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 30th 2015

    Great! Thanks for looking into this.

  3. Change the wording a bit on x 2+1x^2 + 1, so that it “need not” have a root, rather than “does not”, as C is certainly real closed.

    Anonymous

    diff, v25, current

    • CommentRowNumber58.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 22nd 2019

    Wrong!! Please look up the definition of “real closed”. In particular, \mathbb{C} is not real closed. I am rolling back.

    • CommentRowNumber59.
    • CommentAuthorMike Shulman
    • CommentTimeOct 22nd 2019

    I added a brief explanation of why x 2+1x^2+1 does not have a root in a real-closed field, or indeed any ordered field.

    diff, v27, current

    • CommentRowNumber60.
    • CommentAuthorGuest
    • CommentTimeMar 15th 2022
    Mike Shulman pointed out on the HoTT Zulip that the statement "A fully choice-free constructive proof also exists for the Cauchy complex numbers" in the Weak Foundations section is unsourced and most likely wrong.
    • CommentRowNumber61.
    • CommentAuthorMike Shulman
    • CommentTimeMar 15th 2022

    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.

    • CommentRowNumber62.
    • CommentAuthorMike Shulman
    • CommentTimeMar 15th 2022

    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”.

    • CommentRowNumber63.
    • CommentAuthorGuest
    • CommentTimeMar 15th 2022

    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

    • CommentRowNumber64.
    • CommentAuthorDmitri Pavlov
    • CommentTimeMar 15th 2022
    • CommentRowNumber65.
    • CommentAuthorMike Shulman
    • CommentTimeMar 18th 2022

    Some helpful people on the HoTT Zulip have provided some references. When editing is possible again, we should add them to the lab.

    • CommentRowNumber66.
    • CommentAuthorUrs
    • CommentTimeMar 18th 2022

    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.

    • CommentRowNumber67.
    • CommentAuthorGuest
    • CommentTimeMar 20th 2022

    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.

  4. adding proof that the intermediate value theorem is not valid for all polynomials in constructive mathematics

    Anonymous

    diff, v32, current

  5. That polynomial functions satisfy the exact intermediate value only when weak countable choice is valid.

    Anonymous

    diff, v32, current

    • CommentRowNumber70.
    • CommentAuthorGuest
    • CommentTimeJun 2nd 2022

    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 |x|x 2{|x|} \coloneqq \sqrt{x^2} 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?

  6. properly defining the fundamental theorem of algebra in constructive mathematics.

    Anonymous

    diff, v34, current

    • CommentRowNumber72.
    • CommentAuthorGuest
    • CommentTimeMay 20th 2023

    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 \mathbb{C}: We cannot find a continuous solution X(c)X(c) to the equation X 2+c=0X^2 + c = 0 when cc \in \mathbb{C} is near 00.

    But the classical FTA does extend to all of \mathbb{C}.

    The problem is that all notions of \mathbb{C} 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 X 2+c=0X^2 + c = 0 has a solution when |c|>0\vert c \vert \gt 0 or |c|=0\vert c \vert = 0, but because \mathbb{C} is not discrete, one cannot show that |c|>0\vert c \vert \gt 0 or |c|=0\vert c \vert = 0 for all cc \in \mathbb{C}.

    • CommentRowNumber73.
    • CommentAuthorGuest
    • CommentTimeMay 20th 2023

    added Ruitenberg’s actual statement of the FTA to the article

    diff, v38, current

  7. In the section titled “in constructive mathematics” the following sentence appears:

    In fact, this fails in certain topoi, such as sheaves over \mathbb{C}, because that the complex numbers have a continuous square root over \mathbb{C} 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.

  8. The link to Fred Richman’s website in the reference

    doesn’t work anymore.

    Anonymouse

    diff, v40, current

  9. Found the doi and pdf for the Fred Richman paper:

    Anonymouse

    diff, v41, current

    • CommentRowNumber77.
    • CommentAuthorUrs
    • CommentTimeJan 28th 2024

    added also pointer to:

    • Fred Richman, Constructive Mathematics without Choice, in: Reuniting the Antipodes – Constructive and Nonstandard Views of the Continuum, Synthese Library 306, Springer (2001) 199-206 [doi:10.1007/978-94-015-9757-9_17]

    diff, v42, current

  10. 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

    diff, v43, current