The derivative of an unramified monogenic algebra

If R[X]/(f) is formally unramified over R, the image of f' is a unit. Equivalently, f is separable in the ring-theoretic sense of being coprime to its derivative. No monicity or finiteness assumption is needed for this implication.

For monic polynomials this supplies the necessary half of the monogenic étaleness criterion; compare the definition of standard étale maps in the Stacks Project, Tag 00UB. It detects the obstruction to étaleness of root extractions in residue characteristics dividing the exponent. The square-zero test algebra used here is the trivial extension of R[X]/(f, f') by itself.

theorem Polynomial.isUnit_mk_derivative_of_formallyUnramified_adjoinRoot {R : Type u_1} [CommRing R] (f : Polynomial R) [Algebra.FormallyUnramified R (AdjoinRoot f)] : IsUnit ((AdjoinRoot.mk f) (derivative f))

In a formally unramified monogenic algebra, the derivative of its defining equation is invertible.