Unramified residue extensions are finite separable

The local picture. Let $\mathfrak{p}\subseteq B$ be the prime with $x=\mathfrak{p}$ and $\mathfrak{q}=\mathfrak{p}\cap A$, so that $s=f(x)$ corresponds to $\mathfrak{q}$. Put $R:=B_{\mathfrak{p}}={\mathcal{O}}_{X,x}$ and $A^{\mathrm{\prime }}:=A_{\mathfrak{q}}={\mathcal{O}}_{S,s}$, with maximal ideals $\mathfrak{m}=\mathfrak{p}{B}_{\mathfrak{p}}$ and ${\mathfrak{m}}_s=\mathfrak{q}{A}_{\mathfrak{q}}$. By [F2], $\kappa (x)=\mathrm{Frac}(B\mathrm{/}\mathfrak{p})$, $\kappa (s)=\mathrm{Frac}(A\mathrm{/}\mathfrak{q})$, ${\mathfrak{m}}_{s}R\subseteq \mathfrak{m}$, and the hypothesis reads ${\mathrm{\Omega }}_{R\mathrm{/}{A}^{\mathrm{\prime }}}=({\mathrm{\Omega }}_{B\mathrm{/}A}{)}_{\mathfrak{p}}={\mathrm{\Omega }}_{X\mathrm{/}S,x}=0$.

Choice. Assume the Axiom of Choice [F4]; it is consumed below only by the two Choice-dependent results [F6] and [F11], while the separable-residue supplier [F7] is choice-free.

The residue extension is finitely generated. By [F1] the $A$-algebra $B$ is generated by finitely many elements $b_1,\dots ,b_N$, so $B\mathrm{/}\mathfrak{p}$ is generated as an $A\mathrm{/}\mathfrak{q}$-algebra, hence as a $\kappa (s)$-algebra, by the images of the $b_i$; therefore $\kappa (x)=\mathrm{Frac}(B\mathrm{/}\mathfrak{p})$ is a finitely generated field extension of $\kappa (s)$ in the sense of [F3].

The differentials of the residue extension vanish. Apply the conormal sequence [F5] to the ring map $A^{\mathrm{\prime }}\to R$ and the ideal $\mathfrak{m}\subseteq R$ with $R\mathrm{/}\mathfrak{m}=\kappa (x)$: the sequence $\mathfrak{m}\mathrm{/}{\mathfrak{m}}^2\to \kappa (x){\otimes }_R{\mathrm{\Omega }}_{R\mathrm{/}{A}^{\mathrm{\prime }}}\to {\mathrm{\Omega }}_{\kappa (x)\mathrm{/}{A}^{\mathrm{\prime }}}\to 0$ is exact, and ${\mathrm{\Omega }}_{R\mathrm{/}{A}^{\mathrm{\prime }}}=0$ by step 1.1, so ${\mathrm{\Omega }}_{\kappa (x)\mathrm{/}{A}^{\mathrm{\prime }}}=0$. The structure map $A^{\mathrm{\prime }}\to \kappa (x)$ factors as $A^{\mathrm{\prime }}\to \kappa (s)\to \kappa (x)$ with $A^{\mathrm{\prime }}\to \kappa (s)$ surjective, and ${\mathrm{\Omega }}_{\kappa (s)\mathrm{/}{A}^{\mathrm{\prime }}}=0$ by [F5]; the transitivity sequence [F5] for $A^{\mathrm{\prime }}\to \kappa (s)\to \kappa (x)$ has first term ${\mathrm{\Omega }}_{\kappa (s)\mathrm{/}{A}^{\mathrm{\prime }}}{\otimes }_{\kappa (s)}\kappa (x)=0$ and is exact at ${\mathrm{\Omega }}_{\kappa (x)\mathrm{/}{A}^{\mathrm{\prime }}}$, so the natural map ${\mathrm{\Omega }}_{\kappa (x)\mathrm{/}{A}^{\mathrm{\prime }}}\to {\mathrm{\Omega }}_{\kappa (x)\mathrm{/}\kappa (s)}$ is an isomorphism. Hence ${\mathrm{\Omega }}_{\kappa (x)\mathrm{/}\kappa (s)}=0$.

The fibre ring. Put $\bar{R}:=R\mathrm{/}{\mathfrak{m}}_{s}R$, $\bar{\mathfrak{m}}:=\mathfrak{m}\mathrm{/}{\mathfrak{m}}_{s}R$. By [F10], $\bar{R}\cong R{\otimes }_{A^{\mathrm{\prime }}}\kappa (s)=B_{\mathfrak{p}}{\otimes }_{A_{\mathfrak{q}}}\kappa (s)\cong (B{\otimes }_A\kappa (s){)}_{\mathfrak{p}}$, the last isomorphism because localisation is extension of scalars and $\kappa (s)=A_{\mathfrak{q}}\mathrm{/}\mathfrak{q}{A}_{\mathfrak{q}}$; hence $\bar{R}$ is a localisation of the finitely generated $\kappa (s)$-algebra $B{\otimes }_A\kappa (s)$ [F9], so $\bar{R}$ is a Noetherian local $\kappa (s)$-algebra with maximal ideal $\bar{\mathfrak{m}}$ and residue field $\bar{R}\mathrm{/}\bar{\mathfrak{m}}\cong R\mathrm{/}\mathfrak{m}=\kappa (x)$.

$\kappa (x)\mathrm{/}\kappa (s)$ is finite separable. By step 2.1 the extension $\kappa (x)\mathrm{/}\kappa (s)$ is finitely generated and by step 2.2 it has vanishing module of differentials, so [F6], applied under the Axiom of Choice of step 1.2, shows that $\kappa (x)\mathrm{/}\kappa (s)$ is finite and separable.

The differentials of the fibre ring vanish. By [F9], ${\mathrm{\Omega }}_{(B{\otimes }_A\kappa (s))\mathrm{/}\kappa (s)}\cong {\mathrm{\Omega }}_{B\mathrm{/}A}{\otimes }_B(B{\otimes }_A\kappa (s))$; localising at $\mathfrak{p}$ and using ${\mathrm{\Omega }}_{R\mathrm{/}{A}^{\mathrm{\prime }}}=({\mathrm{\Omega }}_{B\mathrm{/}A}{)}_{\mathfrak{p}}=0$ from step 1.1 together with $\bar{R}\cong (B{\otimes }_A\kappa (s){)}_{\mathfrak{p}}$ from step 2.3 gives ${\mathrm{\Omega }}_{\bar{R}\mathrm{/}\kappa (s)}\cong ({\mathrm{\Omega }}_{B\mathrm{/}A}{)}_{\mathfrak{p}}{\otimes }_{B_{\mathfrak{p}}}\bar{R}=0$.

The cotangent space of the fibre ring vanishes. The field $\kappa (x)$ is a finite separable extension of $\kappa (s)$ by step 3.1, hence separably generated over $\kappa (s)$ by [F8]; the ring $\bar{R}$ is a Noetherian local $\kappa (s)$-algebra with residue field $\kappa (x)$ by step 2.3, so the supplier [F7] applies and the injective cotangent map is an isomorphism $\bar{\mathfrak{m}}\mathrm{/}{\bar{\mathfrak{m}}}^2\cong {\mathrm{\Omega }}_{\bar{R}\mathrm{/}\kappa (s)}{\otimes }_{\bar{R}}\kappa (x)=0$, the vanishing being step 3.2.

The maximal ideal of the fibre ring is zero. Since $\bar{R}$ is Noetherian [step 2.3], the ideal $\bar{\mathfrak{m}}$ is finitely generated, and $\bar{\mathfrak{m}}\mathrm{/}{\bar{\mathfrak{m}}}^2=0$ by step 4.1 means $\bar{\mathfrak{m}}={\bar{\mathfrak{m}}}^2$. As $\bar{\mathfrak{m}}=J(\bar{R})$ is the Jacobson radical of the local ring $\bar{R}$ [F11], Nakayama's lemma [F11] with $I=M=\bar{\mathfrak{m}}$ gives $\bar{\mathfrak{m}}=0$.

The maximal ideals match. Since $\bar{\mathfrak{m}}=\mathfrak{m}\mathrm{/}{\mathfrak{m}}_{s}R$ is zero by step 5.1, we get $\mathfrak{m}={\mathfrak{m}}_{s}R$, that is ${\mathfrak{m}}_{f(x)}{\mathcal{O}}_{X,x}={\mathfrak{m}}_x$.

Conclusion. Steps 3.1 and 6.1 prove the two assertions under the stated hypotheses. If $f$ is unramified then ${\mathrm{\Omega }}_{X\mathrm{/}S}=0$ by [F12], so the hypotheses hold at every point $x$; if $f$ is formally etale and locally of finite type then ${\mathrm{\Omega }}_{X\mathrm{/}S}=0$ by [F12] and again the hypotheses hold at every point. The Axiom of Choice entered only through [F6] in step 3.1 and [F11] in step 5.1.