Finite étale covers of a smooth proper family over a complete DVR are determined by the closed fibre

Both $X$ and $X_0$ are regular. Indeed [F3] gives an étale map from a neighbourhood of each point to an affine space over the regular base. In a local étale map $A\to B$ with $A$ regular of dimension $d$, its regular parameter sequence remains regular in $B$ by flatness, giving $\mathrm{depth}B\ge d$. The maximal ideal of $B$ is generated by those $d$ parameters by [F3], so $\dim B\le d$; depth bounded by dimension then forces $\dim B=\mathrm{edim}B=d$. Thus $B$ is regular, proving the claim for the total space and the fibre. Regular Noetherian schemes have finitely many disjoint integral open and closed components by normality in [F3]. Each nonempty component of $X$ dominates the trait: its smooth map is open and its proper map has closed image, so the image is all of the connected trait. Work on one such integral component, and combine the eventual covers by disjoint union.

Take $Z\to X$ from [F1], with isomorphism locus $U$. Pull $Y_0$ back to the special fibre $Z_0$. Projective flat lifting in [F1] produces a finite étale cover $W\to Z$. Its generic algebra at the common function field of $Z$ and $X$ is a product of finite separable fields. Normalize $X$ in that algebra; [F2] gives a finite normal cover $Y\to X$. Over $U$ it agrees with $W$: on the normal open $U$, a finite étale algebra is the integral closure in its generic algebra by [F2]. The open $U$ contains all codimension-one points, so $Y$ is étale there and hence everywhere by purity in [F2]. Every irreducible component of $X_0$ has a codimension-one generic point in $X$, since the uniformizer cuts the fibre and is a nonzerodivisor by smooth flatness. Thus $U_0$ is dense in every component of the regular, hence normal, special fibre. The two finite étale covers $Y\mathrm{\mid }{X}_0$ and $Y_0$ agree on $U_0$, using the original identification $W\mathrm{\mid }{Z}_0=Y_0{\times }_{X_0}{Z}_0$. Finite étale algebras over a normal integral base are its integral closures in their generic algebras by [F2], so that agreement extends uniquely on every component of $X_0$. Hence $Y\mathrm{\mid }{X}_0\cong Y_0$, proving essential surjectivity over the proper, possibly nonprojective $X$.

Let $Y,Z$ be finite étale covers of $X$ and let $a_0:Y_0\to Z_0$ be a map. Its graph is an open and closed finite étale subscheme of $(Y{\times }_{X}Z{)}_0$. The scheme $P=Y{\times }_{X}Z$ is smooth and proper over $R$ by [F3]–[F4], so the existence argument of steps 1.1 and 2.1 applies to it and lifts that graph to a finite étale cover $Q\to P$. The projection $Q\to Y$ is finite étale by [F4]. It has degree one at every point of the closed fibre by construction. Every connected component of $Y$ meets that fibre, since it is proper over the local trait and nonempty, so its degree is one everywhere. By [F4] the projection is an isomorphism, and $Y\cong Q\to Z$ lifts $a_0$. If two lifts agree on the closed fibre, their open and closed equalizer has complementary closed subscheme proper over $R$ with empty special fibre. A nonempty closed image in a local trait contains its closed point, so that complement is empty. This proves uniqueness and full faithfulness. Together with step 2.1 it proves the equivalence, with the AC use exactly as recorded in [F4].