Lemma 10.152.2. Let R \to S be a ring map. Let \mathfrak q be a prime of S lying over \mathfrak p \subset R. Assume that R \to S is of finite type and unramified at \mathfrak q. Then there exist
an étale ring map R \to R',
a prime \mathfrak p' \subset R' lying over \mathfrak p.
a product decomposition
R' \otimes _ R S = A \times B
with the following properties
R' \to A is surjective, and
\mathfrak p'A is a prime of A lying over \mathfrak p' and over \mathfrak q.
Proof.
We may replace (R \to S, \mathfrak p, \mathfrak q) with any base change (R' \to R'\otimes _ R S, \mathfrak p', \mathfrak q') by an étale ring map R \to R' with a prime \mathfrak p' lying over \mathfrak p, and a choice of \mathfrak q' lying over both \mathfrak q and \mathfrak p'. Note also that given R \to R' and \mathfrak p' a suitable \mathfrak q' can always be found.
The assumption that R \to S is of finite type means that we may apply Lemma 10.145.4. Thus we may assume that S = A_1 \times \ldots \times A_ n \times B, that each R \to A_ i is finite with exactly one prime \mathfrak r_ i lying over \mathfrak p such that \kappa (\mathfrak p) \subset \kappa (\mathfrak r_ i) is purely inseparable and that R \to B is not quasi-finite at any prime lying over \mathfrak p. Then clearly \mathfrak q = \mathfrak r_ i for some i, since an unramified morphism is quasi-finite (see Lemma 10.151.6). Say \mathfrak q = \mathfrak r_1. By Lemma 10.151.5 we see that \kappa (\mathfrak r_1)/\kappa (\mathfrak p) is separable hence the trivial field extension, and that \mathfrak p(A_1)_{\mathfrak r_1} is the maximal ideal. Also, by Lemma 10.41.11 (which applies to R \to A_1 because a finite ring map satisfies going up by Lemma 10.36.22) we have (A_1)_{\mathfrak r_1} = (A_1)_{\mathfrak p}. It follows from Nakayama's Lemma 10.20.1 that the map of local rings R_{\mathfrak p} \to (A_1)_{\mathfrak p} = (A_1)_{\mathfrak r_1} is surjective. Since A_1 is finite over R we see that there exists a f \in R, f \not\in \mathfrak p such that R_ f \to (A_1)_ f is surjective. After replacing R by R_ f we win.
\square
Comments (2)
Comment #3260 by Dario Weißmann on
Comment #3356 by Johan on