How to construct a constructive proof from a non-constructive proof using prime ideals?

Question

The sum of two nilpotent elements of a commutative ring is nilpotent. This can be checked by a direct calculation using the binomial theorem. In fact, this calculation shows the stronger statement $x^n=y^m=0 \Rightarrow (x+y)^{n+m-1}=0$.

But we can also give a more sophisticated proof: If $x,y$ are nilpotent, they are contained in every prime ideal. Hence, the same is true for $x+y$. Hence, $x+y$ is nilpotent: otherwise, the localization at $x+y$ would be non-zero and therefore have a prime ideal, but this corresponds to a prime ideal in the given ring not containing $x+y$. (In short: The set of nilpotent elements is the intersection of all prime ideals, hence closed under addition.)

The general existence of prime ideals is equivalent to the Boolean Prime Ideal Theorem and therefore the proof above is not constructive. The proof shows nothing about the nilpotence exponent of the sum. On the other hand, it is quite elegant and it is really a no-brainer if you are used to commutative algebra. Moreover, it can be made "more constructive" (not really constructive, as Matt F. points out), or at least provable in $\mathsf{ZF}$, as follows:

We restrict our attention to the subring generated by $x,y$. This ring is countable. The same is true for the localization at $x+y$. There is a constructive proof that every non-trivial countable commutative ring has a maximal ideal, hence has a prime ideal. And now we may proceed as before.

So we have two constructive proofs: (a) the direct calculation using the binomial theorem, (b) the proof using prime ideals. The question is: Assume that we know the proof (b), is there a general method how to produce the proof (a) from it? Perhaps even including the stronger statement about the nilpotence exponent? This is just a toy example for the general question how to get rid of prime ideals in proofs in commutative algebra where we would expect to have, or already know, more direct proofs. I have only picked this toy example because I hope that the general method can be easily explained with it.

Another toy example: How to produce the direct proof of $I+J=A \Rightarrow I^n+J^n=A$ for ideals $I,J \subseteq A$ from the proof using prime ideals? A more sophisticated example can be found here, where I have no idea how a direct calculation looks like (perhaps I will ask this in a separate question).

I know that Thierry Coquand and Henri Lombardi have worked on related questions, but after some skimming through their work I couldn't find an answer to my question.

Answer 1

Exactly what kind of answer you get depends on the kind of proof you start with and what exactly you mean by constructive. But the proof mining approach offers an answer to some questions of this kind.

The crucial idea that comes out of it is that, to prove concrete facts, one can generally replace the notion of a prime ideal with sort of "local primality" notion. Basically, if P is a possibly prime ideal, one often doesn't need it to be truly prime to complete the proof; it might suffice, say, to look at a single pair $f_Pg_P\in P$ and need $f_P\in P$ or $g_P\in P$ to complete the argument. Therefore one can first fix the function $P\mapsto (f_P,g_P)$, and then ask for an ideal P with the property that $f_P\in P$ or $g_P\in P$. (More generally, we might hope to look at only finitely many test cases of this kind.)

At least in suitably restricted settings (say, where we are considering ideals which have reasonable finitary representations of some kind), one can extract constructive proofs along these lines.

Under suitable circumstances (in particular, one has to consider questions about how the ideal $P$ is represented) one can obtain constructive proofs this way. William Simmons I will be soon (I hope by the end of the month) uploading a paper on proof mining in polynomial and differential polynomial rings which tackles some related problems. Being polynomial rings, however, makes a big difference, because it means ideals are guaranteed to have finite representations.

Answer 2

Here is a method which is very efficient in the case were "constructive" is interpreted as "no axiom of choice at all, not even countable and no law of excluded middle", i.e. essentially "topos logic".

It is possible to construct a very well behaved "Zariski spectrum" (including its structural sheaf whose globale section will be $A$ exactly) as a locale instead of a topological space: on will simply say that $\text{Spec } A$ is the classifying space of the theory of "complement of prime ideals" described below.

One can then construct the structural sheaf and so one and it is relatively trivial that the set of global section is $A$ and that an element of $A$ which is nowhere invertible in the structural sheaf is nilpotent.

points of the spectrum are still the prime ideal, but because it is now a locale instead of a topological space one does not really care about existence of points or not.

well this is not entirely true: technically the point (in the sense of classyfing topos) are the "complement of prime ideal" I.e. subset $I$ that satisfies $0 \notin I$, $1 \in I$, if $x+y \in I$ then $x\in I$ or $y \in I$ and $yx \in I$ if and only if $x \in I$ and $y \in I$. assuming the law of excluded middle this is the same as saying that the complement of $I$ is a prime ideal...

almost all "geometrical argument" can be made constructive by replacing the ordinary zariski spectrum by the localic Zariski spectrum, and this include most prof that involve using all prime ideal.

This technique is very well known among topos theorist but I don't know any reference explaining this clearly, maybe someone will know of one ?

In the mean time, I will try to give a little more explanation: Basically, instead of saying "let $\rho$ be a prime ideal" you move to the structural sheaf over the Zariski spectrum, especially if you know a little bit of internal logic this amount to assume that you have a subset $I$ as above which play the role of (the complement of) your prime ideal and if you can prove that your element $x$ is never in $I$ then it is nilpotent or if your some ideal "always contains an element of $I$" it has to be the whole ring and so one... Moreover, the structural sheaf is the localization at $I$ and $I$ is exactly the set of element that are invertible in the structural sheaf.

The drawback is that the rest of the proof has to be performed internally in in the topos of sheaves over the zariski spectrum, hence really has to be constructive (not involving the law of excluded middle) or has to involve working explicitly with sheaves.

Let me illustrate this on your two examples:

The sum of two nilpotent is nilpotent:

($I$ denote the universal "completment of prime ideal" in the logic of $spec A$, it is also the subobject of the structural sheaf of invertible element)

let $x$ and $y$ be nilpotent, internally in $\text{Spec } A$ $x$ and $y$ are not invertible (i.e. not element of $I$) hence $x+y$ is not invertible either (because $x+Y \in I \Rightarrow x \in I$ or $y \in Y$), hence $x+y$ is nowhere invertible on the spectrum hence nilpotent.

The thing about sum of ideals: well the exact same proof apply, just redefine $V(A)$ to be the corresponding closed subspace of the Zariski spectrum instead of a set of prime ideal...

Answer 3

Since this is somewhat hidden in the comments, let me give the following answer:

• The statement that the sum of two nilpotents is nilpotent is so basic that it seems to be used in the construction and the verification of the Zariski locale/topos/lattice. I don't think that constructive algebra can prove this without circular arguments.
• However, the statement $I+J=A \Rightarrow I^n+J^m=A$ can be proven by working in the lattice of radical ideals: $$\sqrt{I^n+J^m}=\sqrt{I^n} \vee \sqrt{J^m}=\sqrt{I} \vee \sqrt{J}=\sqrt{I+J}=A.$$ Whenever one uses the open subset $D(I)$ in a proof, one may simply replace it by the radical ideal $\sqrt{I}$