Constructive Proof of Maximal Ideal in Ring with Unity

ac.commutative-algebralo.logic

Many commutative algebra textbooks establish that every ideal of a ring is contained in a maximal ideal by appealing to Zorn's lemma, which I dislike on grounds of non-constructivity. For Noetherian rings I'm told one can replace Zorn's lemma with countable choice, which is nice, but still not nice enough – I'd like to do without choice entirely.

So under what additional hypotheses on a ring $R$ can we exhibit one of its maximal ideals while staying in ZF? (I'd appreciate both hypotheses on the structure of $R$ and hypotheses on what we're given in addition to $R$ itself, e.g. if $R$ is a finitely generated algebra over a field, an explicit choice of generators.)

Edit: I guess it's also relevant to ask whether there are decidability issues here.

Best Answer

I suspect that the most general reasonable answer is a ring endowed with a constructive replacement for what the axiom of choice would have given you.

How do you show in practice that a ring is Noetherian? Either explicitly or implicitly, you find an ordinal height for its ideals. Once you do that, an ideal of least height is a maximal ideal. This suffices to show fairly directly that any number field ring has a maximal ideal: The norms of elements serve as a Noetherian height.

The Nullstellensatz implies that any finitely generated ring over a field is constructively Noetherian in this sense.

Any Euclidean domain is also constructively Noetherian, I think. A Euclidean norm is an ordinal height, but not at first glance one with the property that $a|b$ implies that $h(a) \le h(b)$ (with equality only when $a$ and $b$ are associates). However, you can make a new Euclidean height $h'(a)$ of $a$, defined as the minimum of $h(b)$ for all non-zero multiples $b$ of $a$. I think that this gives you a Noetherian height.

I'm not sure that a principal ideal domain is by itself a constructive structure, but again, usually there is an argument based on ordinals that it is a PID.