Maximal ideals in countable rings, constructively

TL;DR

This paper demonstrates how to construct maximal ideals in countable rings within constructive set theory without relying on the axiom of choice, using a novel recursive approach and minimal logic.

Contribution

It introduces a constructive method to find maximal ideals in countable rings without choice or strong discreteness assumptions, extending to arbitrary rings via a metatheorem.

Findings

Constructive existence of maximal ideals in countable rings

Maximal ideals lead to residue fields and geometric fields under certain conditions

Method applies to rings indexed by well-founded sets and in Heyting arithmetic

Abstract

The existence of a maximal ideal in a general nontrivial commutative ring is tied together with the axiom of choice. Following Berardi, Valentini and thus Krivine but using the relative interpretation of negation (that is, as "implies 0 = 1") we show, in constructive set theory with minimal logic, how for countable rings one can do without any kind of choice and without the usual decidability assumption that the ring is strongly discrete (membership in finitely generated ideals is decidable). By a functional recursive definition we obtain a maximal ideal in the sense that the quotient ring is a residue field (every noninvertible element is zero), and with strong discreteness even a geometric field (every element is either invertible or else zero). Krull's lemma for the related notion of prime ideal follows by passing to rings of fractions. All this equally applies to rings indexed by any well-founded set, and can be carried over to Heyting arithmetic with minimal logic. We further show how a metatheorem of Joyal and Tierney can be used to expand our treatment to arbitrary rings. Along the way we do a case study for proofs in algebra with minimal logic. An Agda formalization is available at an accompanying repository.