Proof and intuition for a generalization of primitive element theorem?

Question

A couple of weeks ago I asked this question about a geometric interpretation of the primitive element theorem. A comment pointed me to Proposition 1.3.15 of these notes by Charles, which reads:

Proposition 1.3.15. Let $f:X\to S$ be a morphism of schemes. Let $x$ be a point of $X$ and let $s=f(x)$. Assume that $f$ is étale at $x$. Then there exist open affine neighborhoods $U=\operatorname{Spec}B$ and $V=\operatorname{Spec}A$ of $x$ and $s$ respectively, with $f(U)\subset V$, and an $S$-immersion $U\to\mathbb A_S^1$ that identifies $U$ with an open subscheme of a closed subscheme $Z\subset \mathbb A_S^1$ defined by a monic polynomial $P\in A[X]$ such that $P^\prime$ does not vanish on $U$.

Remark 1.3.16. Conversely, it is easy to check that such a $U$ is étale over $S$. The theorem above should be considered as a generalization of the primitive element theorem for separable extensions of fields.

For proof author cites chapter V of Raynaud's Anneaux locaux henséliens, but I cannot read french so it doesn't help me very much.

I'd like two things:

1. A proof of this proposition (an English reference would be great);
2. An explanation of the geometric picture, and why this generalizes the classical primitive element theorem. Why is separability no longer needed?

Answer 1

1. A proof of this proposition (an English reference would be great).

As stated in the comments, this is (10) in http://stacks.math.columbia.edu/tag/02GU, up to notational changes. You can probably find it in Bosch-Lütkebohmert-Raynaud's Néron Models here.

• S. Bosch, W. Lütkebohmert, and M. Raynaud. Néron models. Ergebnisse der Mathematik und ihrer Grenzgebiete (3) [Results in Mathematics and Related Areas (3)], 21. Springer-Verlag, Berlin, 1990. x+325 pp.

2. An explanation of the geometric picture, and why this generalizes the classical primitive element theorem. Why is separability no longer needed?

Let $K/k$ be a finite extension of fields. Then it is separable if and only if $\text{Spec}\,K \to \text{Spec}\,k$ is étale (this is by the differential criterion for étaleness), so taking $X = \text{Spec}\,K$, $S = \text{Spec}\,k$ we do recover the classical result (note that $U$ is the $\text{Spec}$ of $A[X]/P$ with the notations above). Geometrically, it means that $X$ can locally be defined by a single equation. Here is another interpretation: general results show that if $X \to S$ is étale, then Zariski-locally, $X$ can be cut out by $r$ equations in $\mathbb{A}^r \times S$ with the differential of these equations being independent. Now the local inversion theorem does not hold for the Zariski topology so we can not take $r = 0$. What the proposition shows is that we can at least take $r = 1$.