Does "zero dimensional domains are fields" require the Boolean Prime Ideal theorem?

Consider the following simple lemma:

Lemma 1. Let $R$ be a commutative domain, then $R$ is a field iff $\dim(R)=0$.

N.B. By "commutative domain" I mean ''nonzero commutative ring with 1 such that $xy=0$ implies either $x=0$ or $y=0$'' and "dimension" means "Krull dimension". $(\!\!\implies\!\!)$ is unconditionally true. The proof I know for $(\!\!\impliedby\!\!)$ involves the existence of maximal ideals and thus Zorn's lemma. This initally led me to wonder:

Wrong question: is the axiom of choice (in the form that every proper ideal is contained in a maximal ideal) required to prove Lemma 1? Is Lemma 1 even equivalent to the axiom of choice?

After searching the internet for clues I stumbled on this MathOverflow question on the existence of prime ideals and godelian's answer. The following doesn't require any choice principle:

Lemma 2. Let $R$ be a nonzero commutative ring with $1$, then $R$ is a field iff its only ideals are $(0)$ and $(1)$.

So to prove that zero dimensional domains are fields it is enough to prove that their only ideals are $(0)$ and $(1)$. If there were some proper ideal $(0)<I<(1)$ then, by the Boolean Prime Ideal (BPI) theorem, the quotient ring $R/I$ would have a prime ideal which pulls back to a prime $(0)<I\leq \mathfrak{p}$ in $R$. Thus $\dim(R)\geq 1$ which is a contradiction.

Better question: is BPI required to prove Lemma 1? Is Lemma 1 strictly weaker than the BPI?

One can slightly broaden the scope of the question by dropping the domain condition and asking

Slightly broader question. Does "prime ideals in zero dimensional rings are maximal" require the BPI? Is it possibly even equivalent to the BPI? Or is it weaker?

One can ask a broader question still without mentioning dimensions:

Alternative phrasing. What choice principle is required to prove that prime ideals which are maximal among prime ideals are maximal among all proper ideals.

Yes, your Lemma 1 is equivalent to the Boolean Prime Ideal Theorem. $\DeclareMathOperator{\colim}{colim} \DeclareMathOperator{\Spec}{Spec} \DeclareMathOperator{\Atoms}{Atoms} \DeclareMathOperator{\Primes}{Primes} \newcommand{FinSetSurj}{\mathsf{FinSet}_{\mathrm{surj}}} $

We work in ZF with the axiom that every commutative domain is either a field or has a nonzero prime ideal. We are given a nonzero Boolean ring $B$ and the aim is to produce a prime ideal of $B.$

The plan is to transform each finite subring of $B$ to adjoin a zero prime ideal to the spectrum. I will describe the underlying problem as the construction of a contravariant functor from the category of finite sets and surjections, to the category of commutative rings with unity $$G:\FinSetSurj^{\mathrm{op}}\to\mathsf{CRing}$$ such that each ring $G(A)$ is a domain whose nonzero prime ideals are naturally isomorphic to $A.$ More specifically, for finite sets $A$ define $T(A)$ to be the topological space on the set $A\cup \{*\}$ where the elements of $A$ are closed points, and $*$ is a new point whose closure is the whole space. On morphisms $T$ just extends by sending $*$ to $*.$ The topological space $\Spec(G(A))$ is required to be homeomorphic to $T(A),$ naturally in $A.$

Assuming for now the existence of $G$ the rest of the argument is mostly formal. Let $I$ be the directed set of finite subrings of $B$ ordered by inclusion. All the following colimits range over $R\in I,$ and the limits range over $R\in I^{\mathrm{op}}.$ Let $\Primes:\mathsf{CRing}\to \mathsf{Set}^{\mathrm{op}}$ be the functor that takes a ring to its set of primes i.e. the underlying set of the prime spectrum. Let $\Atoms:I\to \FinSetSurj^{\mathrm{op}}$ be the restriction of $\Primes$ to subrings of $B.$ There are bijections \begin{align*} \Primes(B) &\cong\Primes(\colim R)\\ &\cong \lim \Atoms(R)\\ &\cong \lim (T(\Atoms(R))\setminus\{*\})\\ &\cong (\lim T(\Atoms(R)))\setminus\{*\}\\ &\cong (\lim \Primes(G(\Atoms(R))))\setminus\{(0)\}\\ &\cong \Primes(\colim G(\Atoms(R)))\setminus\{(0)\} \end{align*} where I’m abusing $*$ to mean the element of the limit that sends each $R$ to the $*,$ and similarly for $(0).$ The second and final bijections are the fact that $\Primes$ takes directed colimits of rings to limits in $\mathsf{Set}$ - see https://stacks.math.columbia.edu/tag/078L. To check that $C=\colim G(\Atoms(R))$ is not a field, fix some $R\in I$ and pick any nonzero element $x$ in any nonzero prime ideal of $G(\Atoms(R)).$ Because the connecting maps $\Primes(G(\Atoms(S)))\to\Primes(G(\Atoms(R)))$ are surjective, the connecting maps $G(\Atoms(R))\to G(\Atoms(S))$ take $x$ to an element of a prime ideal, which means $x$ is not invertible in $C.$ A directed colimit of domains is a domain. So by assumption the last set in this chain of bijections is nonempty, which means the first set $\Primes(B)$ must be non-empty, QED.

The existence of $G$ is a problem of “inverting Spec” solved by M. Hochster, Prime ideal structure in commutative rings, Trans. Amer. Math. Soc. 142 (1969), 43--60. Theorem 6(a). I am not sure if those rings would be domains, but quotienting by the unique minimal prime ideal should do. To make this answer more self-contained, and to relieve any anxiety over whether Hochster’s result requires ZFC, I will also describe a construction of $G.$

Define $G(A)$ to be the ring of rational functions in the indeterminates $X_a,$ $a\in A,$ such that the denominator is not divisible by any $X_a.$ In other words, take the polynomial ring on $\{X_a\}$ with rational coefficients, and localize at the set of primes $\{(X_a)\}.$ This removes all the prime ideals except for $(0)$ and each $(X_a).$ For each surjection $f:B\to A$ we need to define a map $G(f):R(A)\to R(B)$ such that the preimage of $(X_b)$ is $(X_{f(b)}).$ Define $G(f)$ on each fraction $p/q$ by substituting each variable $X_a$ by $\prod_{f(b)=a} X_b.$ Observe that distinct monomials are sent to distinct monomials (this is where we need $f$ to be surjective). If every monomial of $G(f)(q)$ is divisible by $X_b,$ then every monomial in $q$ is divisible by $X_{f(b)},$ which was disallowed in the definition of $G(B).$ So $G(f)$ is well defined. The functoriality of $G$ is straightforward.

Remark. I will mention a few properties of this specific $G.$ The rings $G(A)$ are PIDs so the ring $C=\colim G(\Atoms(R))$ is a Bézout domain. The rational number coefficients could be replaced by any fixed base field. The ring $C$ can alternatively be described as the monoid algebra over the monoid $\colim \mathbb N^{\Atoms(R)},$ localized at the set of polynomials that are not divisible by any nontrivial monomial.