Finite prime chains lift through module-finite domain extensions without Choice

First establish finite-module lying over. Fix any prime $\mathfrak{p}$ of $B$, put $S=B\setminus \mathfrak{p}$, $R=B_{\mathfrak{p}}$, $M=S^{-1}A$, and $\mathfrak{m}=\mathfrak{p}R$. The module $M$ is finite over $R$; it is a nonzero ring because $B\subseteq A$ are domains and no element of $S$ annihilates $1\in A$. If $\mathfrak{m}M=M$, [L1] gives $a\in \mathfrak{m}$ with $(1-a)M=0$. Write $a=b\mathrm{/}s$ with $b\in \mathfrak{p}$ and $s\mathrm{\notin }\mathfrak{p}$. Then $1-a=(s-b)\mathrm{/}s$ is an explicit unit of $R$, since $s-b\mathrm{\notin }\mathfrak{p}$. It would force $M=0$, a contradiction. Thus $M\mathrm{/}\mathfrak{m}M\mathrm{\ne }0$.

The quotient $C=M\mathrm{/}\mathfrak{m}M$ is a nonzero finite-dimensional algebra over the residue field $\kappa (\mathfrak{p})=R\mathrm{/}\mathfrak{m}$. Among its proper ideals, choose one $J$ of maximal $\kappa (\mathfrak{p})$-vector-space dimension; this is possible because the zero ideal is proper and the dimensions form a nonempty subset of the finite set $\{0,\dots ,{\dim }_{\kappa (\mathfrak{p})}C-1\}$. A strictly larger proper ideal would have larger vector-space dimension, so $J$ is a maximal, hence prime, ideal of $C$. The field map $\kappa (\mathfrak{p})\to C$ is injective because $C\mathrm{\ne }0$, and therefore the preimage of $J$ in $M$ contracts to $\mathfrak{m}$ in $R$. Pulling it back along the localization $A\to M$ gives a prime of $A$ contracting to $\mathfrak{p}$ in $B$.

Apply steps 1.1–2.1 to $B\subseteq A$ at ${\mathfrak{p}}_0$ to obtain ${\mathfrak{q}}_0$ above ${\mathfrak{p}}_0$. Suppose ${\mathfrak{q}}_i$ has been selected above ${\mathfrak{p}}_i$. The induced inclusion $B\mathrm{/}{\mathfrak{p}}_i\subseteq A\mathrm{/}{\mathfrak{q}}_i$ is again an injective module-finite extension of domains. Apply the finite-module lying-over construction to the prime ${\mathfrak{p}}_{i+1}\mathrm{/}{\mathfrak{p}}_i$ in the lower quotient. By [L2], its prime above pulls back to a prime ${\mathfrak{q}}_{i+1}\supseteq {\mathfrak{q}}_i$ of $A$ contracting to ${\mathfrak{p}}_{i+1}$. The inclusion is strict because its contractions are strict.

Repeating step 3.1 for the supplied finite number $r$ of links produces ${\mathfrak{q}}_0⊊\cdots ⊊{\mathfrak{q}}_r$ with the required contractions. Only finite choices of witnesses occurred: the finite-dimensional ideal in step 2.1 is selected from a bounded set of integer dimensions, and the chain has a supplied finite length.