18
$\begingroup$

I'm interested in proofs using ideas from outside commutative algebra of Hilbert's Basis Theorem.

If $R$ is a noetherian ring, then so is $R[X]$.

or its sister version

If $R$ is a noetherian ring, then so is $R[[X]]$.

I am very much aware of the standard non-construtive proof by contradiction given by Hilbert as well as the direct version using Groebner basis.

Most important theorems in mathematics that are old enough have several very different proofs. Comparing different ideas can be very enlightening and also give a hint to possible generalizations in different areas. For the Basis Theorem however, I am not aware of such.

Improve this question
$\endgroup$
9
  • $\begingroup$ The proof I teach in class is what I thought was "the standard proof" but it's also constructive (for some interpretation of the word). You look at the increasing sequence of ideals generated by leading terms of polys of degree n in your ideal I of R[x] as n goes to infinity and then follow your nose. Why is the second assertion stronger than the first, by the way? Clearly each implies the other in the stupid sense that each one is true, but is there an easy way of deducing the first from the second? $\endgroup$
    – eric
    Commented Nov 7, 2015 at 16:15
  • $\begingroup$ You are right. It does not follow immediatly. I wrote that thinking an ideal in $R[X]$ is also an ideal in $R[[X]]$ under the inclusion, but this is wrong. $\endgroup$
    – Georg Lehner
    Commented Nov 7, 2015 at 16:38
  • $\begingroup$ Could someone link to a proof that they feel is 'constructive'? The standard proof I know of I would consider non-constructive (proof of existence by contradiction, axiom of dependent choice in one form or another). I was trying to think about this a couple of months ago and found it quite bedeviling. $\endgroup$
    – Todd Trimble
    Commented Nov 7, 2015 at 16:50
  • 1
    $\begingroup$ One problem is that the definition of Noetherian is itself not very constructive... there's some previous discussion of this on MO and math.SE but I can't find the one I had in mind. $\endgroup$
    – Qiaochu Yuan
    Commented Nov 7, 2015 at 18:28
  • $\begingroup$ That's the reason I was slightly coy when I claimed my proof was constructive. For example in the proof I know I define an increasing sequence of ideals in $R$ and argue that the union is finitely generated because my definition of "Noetherian" is "all ideals are finitely generated". If you use another one then already there are issues with dependent choice. In fact the point I guess I'm making here is that there issues with DC even in the equivalence of the standard definitions of Noetherian so one might initially have to be careful as to exactly what question is being asked. $\endgroup$
    – eric
    Commented Nov 7, 2015 at 19:41

3 Answers 3

Reset to default
10
$\begingroup$

Sorry, this is not an answer, but rather a too-long elaboration on constructive aspects. I post this here because there was some interest about the constructive content of the theorem in the comments.

  1. As pointed out in the comments, the first thing to get straight is the definition of a Noetherian module (or ring). For instance, with the usual definition "any submodule is finitely generated", even the $\mathbb{Z}$-module $\mathbb{Z}$ cannot be shown to be Noetherian constructively: Pick a formula $\varphi$ such that neither $\varphi$ nor $\neg\varphi$ can be shown. Then consider the submodule $U = \{ x \in \mathbb{Z} \,|\, (x = 0) \vee \varphi \}$. If $U$ were finitely generated, it would a forteriori be generated by a single element (Euclid's algorithm) and we could decide whether $1 \in U$ or $1 \not\in U$, that is whether $\varphi$ or $\neg\varphi$.

  2. A suitable notion of a Noetherian module is given in the very fine book A Course in Constructive Algebra by Mines, Richman, and Ruitenburg: A module is Noetherian if every ascending chain of finitely generated submodules stops (think "$U_n = U_{n+1}$", not "$U_n = U_{n+1} = U_{n+2} = \cdots$").

    This definition works fine for many purposes, but not for showing that $R[X]$ is Noetherian if $R$ is. See Chapter VIII of that book. Also it doesn't work well if dependent choice is not available, since it refers to sequences, which can be quite elusive without choice.

    A different definition appears in http://www.mittag-leffler.se/sites/default/files/IML-0001-30.pdf (by Coquand and Lombardi). There they claim that Noetherianity of $R$ implies Noetherianity of $R[X]$.

    Finally let me recommend the nice article Strongly Noetherian rings and constructive ideal theory by Hervé Perdry. He surveys several kinds of Noetherian conditions.

  3. A thesis of Coquand, Lombardi and others is that the Noetherian condition is often not the right one constructively. Instead, one should refer to the notion of a coherent ring. In classical mathematics, any Noetherian ring is coherent. See for instance page 27 of Commutative Algebra: Constructive Methods by Lombardi and Quitté.

  4. Finally, a short and constructive proof that the Krull dimension of $K[X_1,\ldots,X_n]$ is $n$ appears at http://hlombardi.free.fr/publis/KrullMathMonth.pdf (by Coquand and Lombardi).

Improve this answer
$\endgroup$
2
  • 2
    $\begingroup$ In the absence of dependent choice, a good definition is often "For any set $(I_a)_{a \in A}$ of ideals, there is an index $a$ such that, for all $b \in A$, the ideal $I_b$ does not properly contain $I_a$." I don't know how this plays with constructivity, though. $\endgroup$
    – David E Speyer
    Commented Feb 10, 2016 at 14:23
  • 1
    $\begingroup$ @David: Thanks! I didn't know this condition before. The phrase "does not properly" probably contains a few too many negations to be constructively sensible, but it would be interesting to ponder a more positive reformulation. There is a different definition by Richman, specifically devised to work in a choiceless context: Don't consider ascending sequences, but ascending trees. With this definition a scheme $X$ is locally Noetherian if and only if $\mathcal{O}_X$ is Noetherian from the internal point of view of the topos $\mathrm{Sh}(X)$. $\endgroup$
    – Ingo Blechschmidt
    Commented Feb 10, 2016 at 23:06
5
$\begingroup$

Although I can't imagine I'm telling anyone anything new, here's the proof I know. If $R$ is Noetherian and $I$ is an ideal in $R[X]$ then for each $n\geq0$ consider the subset $J_n$ of $R$ comprised of $\{0\}$ and the leading coefficients of the degree $n$ polynomials in $I$. The $J_n$ are an increasing sequence of ideals; if $J$ is their union then $J=J_N$ for some large $N$; now build a subset of $I$ by looping from $i=0$ to $N$ and at each stage throwing in finitely many polynomials whose leading terms generate $J_i$; an easy induction on degree shows that these polynomials generate $I$. People can muse over just how constructive this is but I have long since ceased to find such questions interesting from a mathematical viewpoint -- ZFC will do for me.

Improve this answer
$\endgroup$
3
$\begingroup$

There is a proof of the theorem for $R[[x]]$ that uses the well-known result of I.S. Cohen that a ring is noetherian if and only if its prime ideals are finitely generated. Such a proof is given by Kaplansky in his 1970 book Commutative Rings, Theorem 70.

This method of proof can be generalized to noncommutative rings to show that the power series ring $R[[x]]$ over a left noetherian ring is left noetherian, as long as one is careful when putting forth a definition of "prime left ideal." Gerhard Michler gave such a proof in a paper that's not so easy to locate (but it seems to be described here), and I gave a similar proof in Theorem 3.9 in this paper.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .