I'm trying to understand the various equivalent definitions of an unramified morphism of schemes. Let $f: X \rightarrow S$ be a morphism of schemes which is locally of finite type, $x \in X$, and $s = f(x)$. Let's say that $f$ is unramified if the stalk of $\Omega_{X/S}$ at $x$ is zero. I want to understand the following result:
If the maximal ideal $\mathfrak m_x$ is generated by the maximal ideal $\mathcal m_s$, and if $\kappa(s) \subset \kappa(x)$ is a finite separable extension, then $f$ is unramified at $x$.
Let $k = \operatorname{Spec} \kappa(s)$, $X_s = X \times_S \operatorname{Spec} k$ be the fiber of $s$, and $p: X_s \rightarrow X$ the "projection." We have
$$p^{\ast} (\Omega_{X/S}) = \Omega_{X_s/k}$$
And therefore
$$(\Omega_{X_s/k})_x = (\Omega_{X/S})_x \otimes_{\mathcal O_{X,x}} \mathcal O_{X_s,x} = (\Omega_{X/S})_x \otimes_{\mathcal O_{X,x}}(\mathcal O_{X,x} \otimes_{\mathcal O_{S,s}} \kappa(s)) = (\Omega_{X/S})_x \otimes_{\mathcal O_{S,s}} \kappa(s)$$
I'm trying to reduce the problem to the special case when $S$ is the spectrum of the field. I thought I could use Nakayama's lemma to say that if we show $(\Omega_{X_s/k})_x = 0$, then $(\Omega_{X/S})_x = 0$. But I do not know that $(\mathcal O_{X/S})_x$ is finitely generated as an $\mathcal O_{S,s}$-module. It is only finitely generated as an $\mathcal O_{X,x}$-module.
How should I go about proving the result? And where is the hypothesis that $\mathfrak m_s$ generates $\mathfrak m_x$ coming in?
Using Property (1) in your previous question, you can reduce your last term in the middle of the post the following case. Let me use the notation $(S,n) \subset (T,m)$, where $m \cap S= n$ and $S/n \subset T/m$ is finite and separable. Your last expression is then $$\Omega_{(T/S)} \otimes_S S/n \cong \Omega_{(T\otimes_S S/n)/(S/n)},$$ where the isomorphism follows from (1). Notice that $T \otimes_S S/n \cong T/nT = T/m$ since $nT = m$. As $S/n \subset T/m$ is finitely and separable, we see that the module in question is zero.