4 Converse: Monogenic with Unit Derivative Implies Étale
Let \(f \in R[X]\) be monic with \(S \cong R[X]/(f)\) (via an \(\mathtt{IsAdjoinRootMonic}\) structure). If \(f'(\beta ) \in S^\times \) where \(\beta \) is the image of \(X\), then \(R \to S\) is étale.
Construct a \(\mathtt{StandardEtalePair}\) using \((f, f')\): the Bézout relation \(f' \cdot 1 + f \cdot 0 = (f')^1\) is trivially satisfied.
The natural map \(P.\mathtt{lift} \colon P.\mathtt{Ring} \to S\) sending \(X \mapsto \beta \) is well-defined by \(f(\beta ) = 0\) and the unit condition on \(f'(\beta )\).
Construct an explicit inverse via \(\mathtt{AdjoinRoot.liftAlgHom}\) composed with the algebra equivalence \(S \cong \mathtt{AdjoinRoot}\; f\). Verify it is both a left and right inverse by checking on generators, concluding bijectivity.
Hence \(S\) is standard étale (\(\mathtt{Algebra.IsStandardEtale}\)), and étale follows.