The Stacks project

Proof. By the valuative criterion of properness applied to the finite morphism $Y' \to X$ we see that $\mathop{\mathrm{Spec}}(K)$-valued points of $Y$ matching $t|_{\mathop{\mathrm{Spec}}(K)}$ as maps into $X$ lift uniquely to morphisms $t' : \mathop{\mathrm{Spec}}(R) \to Y'$. Thus statement (1) make sense.

Choose an étale neighbourhood $(U, u) \to (X, t(\mathfrak m_ R))$ such that $U = \mathop{\mathrm{Spec}}(A)$ and such that $Y' \times _ X U \to U$ has a description as in Lemma 58.31.6 for some $f \in A$. Then $\mathop{\mathrm{Spec}}(R) \times _ X U \to \mathop{\mathrm{Spec}}(R)$ is étale and surjective. If $R'$ denotes the local ring of $\mathop{\mathrm{Spec}}(R) \times _ X U$ lying over the closed point of $\mathop{\mathrm{Spec}}(R)$, then $R'$ is a discrete valuation ring and $R \subset R'$ is an unramified extension of discrete valuation rings (More on Algebra, Lemma 15.44.4). The assumption on $t$ signifies that the map $A \to R'$ corresponding to

maps $f$ to a uniformizer $\pi \in R'$. Now suppose that

for some $e_ i \geq 1$. Then we see that

The rings $R'[x]/(x^{e_ i} - f)$ are discrete valuation rings (More on Algebra, Lemma 15.114.2) and hence have no map into the fraction field of $R'$ unless $e_ i = 1$.

Proof of (1). In this case the map $t' : \mathop{\mathrm{Spec}}(R) \to Y'$ base changes to determine a corresponding map $t'' : \mathop{\mathrm{Spec}}(R') \to Y' \times _ X U$ which must map into a summand corresponding to $i \in I$ with $e_ i = 1$ by the discussion above. Thus clearly we see that $Y' \times _ X U \to U$ is étale along the image of $t''$. Since being étale is a property one can check after étale base chamge, this proves (1).

Proof of (2). In this case the assumption implies that $e_ i = 1$ for all $i \in I$. Thus $Y' \times _ X U \to U$ is finite étale and we conclude as before. $\square$