Lying-over theorem without Axiom of Choice

This question is motivated by this and this. Can the following proposition be proved without Axiom of Choice?

Proposition: Let $k$ be a field. Let $A$ and $B$ be commutative algebras without zero-divisors which are finitely generated over $k$. Suppose that $A$ is a subring of $B$ and $B$ is integral over $A$. Let $P$ be a prime ideal of $A$. Then there exists a prime ideal $Q$ of $B$ such that $P = A \cap Q$.

-
@Dylan: Even so, there are many definitions of "noetherian" and their equivalence depends on AC. E.g., ACC and every ideal is finitely generated depends on some choice, and of course the characterization in terms of nonempty families having maximal elements. So one needs to specify which definition of "noetherian" one is using if you are also working without AC. – Arturo Magidin Jul 7 '12 at 21:31
@DylanMoreland: The "strongest" definition of noetherian (in the sense that it implies the other two even in the absence of AC) is "if $\mathcal{C}$ is a nonempty family of submodules, then $\mathcal{C}$ has a maximal element." That definition essentially says "Zorn's Lemma holds" (one proves it from ACC using Zorn's Lemma), so I can see how one would not need to invoke Zorn's Lemma if you assume it holds. It implies ACC (just take the set of submodules in your chain) and finite generation of submodules (take the collection of finitely generated submodules of the given module), even without AC – Arturo Magidin Jul 7 '12 at 21:47
I don't think that you can prove it without AC. And to be honest, I think it is a little bit misguided to develop commutative algebra without AC. – Martin Brandenburg Jul 7 '12 at 22:39
But what difference does it make, if you do use it once you can use it always. This is mathematics, not World War II and AC is not a nuclear weapon. If you assumed AC for the existence of a basis for a vector space, there is absolutely no harm in use AC for proving a theorem about modules. If you were intentionally limiting yourself to models without AC to begin with, that would be a whole other story. However from your comment it seems that you still accept AC as necessary sometimes and does use it in those cases, so you have to assume it is true in the universe... – Asaf Karagila Jul 8 '12 at 20:05
@Asaf: Dear Asaf, There are plenty of reasons to be mindful of whether or not AC is being used. Naturally if we talk about all vectors spaces (arbitrary, and of arbitrarily large infinite dimension) then we will need AC to say things. But one expects that in more finitistic contexts AC would not be needed. As one example (that is close to my own interests and concerns), it is natural to ask whether AC is used in the proof of Fermat's Last Theorem. Certainly various forms of the result being asked about in this question are used, and so it is natural to wonder if AC is used. Regards, – Matt E Jul 9 '12 at 1:47

First we show

Lemma If $A\to B$ is a finite homomorphism of rings with $A$ local and $B\ne 0$, then the maximal ideal $P$ of $A$ is the pre-image of a maximal ideal $Q$ of $B$.

Proof. By Nakayama's lemma, $PB\ne B$. The quotient $B/PB$ is a finite $k$-algebra (where $k$ is the field $A/P$) and is no zero. The set of proper ideals of $B/PB$ is non-empty and has an element of maximal $k$-vector space dimension. The latter is then a maximal ideal, hence equal to $Q/PB$ for some maximal ideal $Q$ of $B$ containing $P$. The pre-image $P'$ of $Q$ is maximal because $A/P'$ is contained in $B/Q$ and the later is finite over $A/P'$. So $P'=P$.

Now we prove your proposition. As $B$ is a finitely generated $A$-algebra, $B$ integral over $A$ implies that $B$ is finite over $A$. Hence $A_P\to A_P\otimes_A B$ is finite with $A_P\otimes_A B\ne 0$. By the above lemma, $PA_P$ is the pre-image of a maximal ideal of $A_P\otimes_A B$. The existence of $Q$ as desired follows from standard arguments on localizations.

This been said, I agree with the second part of Martin Brandenburg's comment.

-
Have you proved that Nakayama's lemma does not require choice? – Asaf Karagila Jul 7 '12 at 23:02
@MakotoKato: I don't see why using determinant requires AC. Anyway, the point is there exists one proof without AC. – user18119 Jul 7 '12 at 23:17
The proof using determinant shows that there exists an elemet $r$ in $A$ such that $r \equiv 1$ (mod $P$) and $rB = 0$. Hence $B$ = 0, because if $r$ is not invertible, $r \in P$ by Zorn's lemma. – Makoto Kato Jul 7 '12 at 23:26
I agree with Makoto. The last step uses AC. See also my summary at MO: mathoverflow.net/questions/41836/… With ZF it is consistent that in some rings there are no prime ideals at all ... – Martin Brandenburg Jul 7 '12 at 23:40
I see. So we have to be careful on the definition of local rings. One (strong) form is the maximal ideal contains all non-invertible elements. The localization $A_P$ at a prime ideal is consistent with this definition. – user18119 Jul 8 '12 at 8:46

Definition 1 Let $A$ be a commutative ring. Suppose $A$ has a unique maximal ideal. We say $A$ is a local ring in the usual sense.

Definition 2 Let $A$ be a commutative ring. Let $P$ be an ideal of $A$. Suppose that every element of $A - P$ is invertible. Then we say $A$ is a strictly local ring. Clearly $P$ is the unique maximal ideal of $A$. Hence $A$ is a local ring in the usual sense.

Note 1 It can be proved by using AC that a local ring in the usual sense is a strictly local ring. However, we are not supposed to use AC here.

Lemma 1 Let $A$ be commutative ring. Let $P$ be a prime ideal of $A$. Then $A_P$ is a strictly local ring.

Proof: Clear.

Definition 3 Let $A$ be a domain. Let $P$ be a prime ideal of $A$. Let $k$ be the field of fractions of $A/P$. Let $K$ be a field which contains $A$ as a subring. Let $x$ be an element of $K$. Let $x'$ be an element of some field containing $k$. We say $x'$ is a specialzation of $x$ over $P$ and we write $x \rightarrow x'$ over $P$, if there exists a homomorophism $\psi:A[x] \rightarrow (A/P)[x']$ extending the canonical homomorphism $A \rightarrow A/P$ and $\psi(x) = x'$. This is equivalent to that $\tilde{f}(x') = 0$ whenever $f(X) \in A[X]$ such that $f(x) = 0$,where $\tilde{f}(X) \in (A/P)[X]$ is the reduction of $f(X)$ mod $P$.

Lemma 2 Let $A$ be a strictly local domain. Let $\mathfrak{m}$ be the unique maximal ideal of $A$. Let $k = A/\mathfrak{m}$. Let $K$ be a field which contains A. Let $x \in K$. Suppose $x$ has no specializaion in any finite extension field of $k$ over $\mathfrak{m}$. Then $x$ is non-zero and $1/x \rightarrow 0$ over $\mathfrak{m}$.

Proof: Let $P$ = {$f \in A[X]$; $f(x) = 0$}. $P$ is an ideal of $A[X]$. Let $P'$ be the ideal of $k[X]$ generated by the set {$f(X)$ (mod $\mathfrak{m}$); $f(X) \in P$}. We claim that $P' = k[X]$. Suppose otherwise. Then $P'$ is generated by a polynomial $h(X) \in k[X]$, where $h(X)$ is not a non-zero constant. Hence $h(X)$ has a root $x'$ in a finite extension of k. Then $x \rightarrow x'$ over $\frak{m}$ This is a contradiction. Hence there exists $f(X) \in P$ such that $f(X)$ (mod $\mathfrak{m}$) is a non-zero constant. Let $f(X) = a_mX^m + ... + a_0$. Then $a_0 \in A - \mathfrak{m}$, $a_i \in \mathfrak{m}$ for $i > 0$. We assume that $m$ is minimal among the degrees of such polynomials. Let $y = 1/x$. Let $g(Y) = a_0Y^m + ... + a_m$ be a polynomial in $A[Y]$. Then $g(y) = 0$. Let $h(Y)$ be any polynomial in $A[Y]$ such that $h(y) = 0$. Since $A$ is a strict local ring, $a_0$ is invertible. Hence $Z^{m-1}h(Y) = g(Y)q(Y) + r(Y)$, where $q(Y), r(Y) \in A[Y]$ and deg $r \leq m - 1$. Substituting $Y$ by $y$ we get $r(y) = 0$. Taking the reductions mod $\mathfrak{m}$ of the both sides, we get $Y^{m-1}\tilde{h}(Y) = \tilde{a_0}Y^m\tilde{q}(Y) + \tilde{r}(Y)$. Hence $\tilde{h}(0) = \tilde{r}(Y)$. Since $\tilde{r}(Y)$ cannot be a non-zero constant by the minimality of $m$, $\tilde{h}(0) = 0$. Hence $z \rightarrow 0$ over $\mathfrak{m}$. QED

Note 2 The idea of the proof of Lemma 2 is borrowed from Weil's Foundations of algebraic geometry. According to him, the idea is due to Chevalley. See also Note 3 below.

Lemma 3 Let $A$ be a domain. Let $P$ be a prime ideal of $A$. Let $k$ be the field of fractions of $A/P$. There exists a unique homomorphism $A_P \rightarrow k$ extending the canonical homomorphism $A \rightarrow A/P$.

Proof: Clear.

Lemma 4 Let $A$ be a domain. Let $P$ be a prime ideal of $A$. Let $k$ be the field of fractions of $A/P$. Let $K$ be a field which contains A as a subring. Let $x \in K$. Suppose $x$ has no specializaion in any finite extension of $k$ over $P$. Then $x$ is non-zero and $1/x \rightarrow 0$ over $P$.

Proof: Let $B = A_P$. By lemma 1, $B$ is a strictly local ring. Suppose $x \rightarrow x'$ over $PA_P$. By Lemma 3, $x \rightarrow x'$ over $P$. Hence $x$ has no specializaion in any finite extension of $k$ over $PA_P$. By Lemma 2, $1/x \rightarrow 0$ over $PA_P$. Hence, by Lemma 3, $1/x \rightarrow 0$ over $P$. QED

Note 3 Lemma 4 is a generalization of the one given in Weil's Foundations. He proved it when $A$ is a finitely generated domain over a field. Our Lemma 4 treats not only a case where $A$ and $A/P$ have equal characteristics but also a case of unequal ones.

Note 4 As van der Waerden and Weil showed, Lemma 4 has vast applications in algebraic geometry. For example, Hilbert Nullstellensatz can be proved by using it.

Lemma 5 Let $A$ be a domain. Let $P$ be a prime ideal of $A$. Let $k$ be the field of fractions of $A/P$. Let $K$ be a field which contains $A$ as a subring. Let $x \in K$. Suppose $x$ is integral over $A$. Then there exist a finite extension $k'$ of $k$ and $x' \in k'$ such that $x \rightarrow x'$ over $P$.

Proof: Suppose there exists no such x'. By Lemma 4, there exists a homomorophism $\psi:A[1/x] \rightarrow k$ such that $\psi(1/x) = 0$ extending the canonical homomorphism $A \rightarrow A/P$. Let $y = 1/x$. Since $x$ is integral over $A$, $x^n + a_1x^{n-1} + ... + a_0 = 0$. Hence $1 + a_1y + ... + a_0y^n = 0$. Applying $\psi$, we get $1 = 0$. A contradiction. QED

Proposition Let $B$ be a domain. Let $A$ be a subring of $B$. Suppose $B$ is finitely generated as an $A$-module. Let $P$ be a prime ideal of $A$. Let $k$ be the field of fractions of $A/P$. Then there exist a finite extension $k'$ of $k$ and a homomorophism $\psi:B \rightarrow k'$ extending the canonical homomorphism $A \rightarrow A/P$.

Proof: This follows Immediately from Lemma 5.

Corollary Let $B$ be a domain. Let $A$ be a subring of $B$. Suppose $B$ is finitely generated as an $A$-module. Let $P$ be a prime ideal of $A$. Then there exists a prime ideal $Q$ of $B$ such that $P = A \cap Q$.

Proof: This follows Immediately from the proposition.

-