Adjoining a root of a separable monic polynomial is étale

Let f be a monic polynomial over a commutative ring R which is separable, that is, coprime to its derivative. Then R[X]/(f) is a standard étale R-algebra, hence étale over R (Polynomial.Monic.isStandardEtale_adjoinRoot). This is the presentation R[X][1/g]/(f) of Mathlib's StandardEtalePair with g = 1: the derivative of f is already invertible modulo f. Conversely, Monic.etale_adjoinRoot_iff shows that étaleness forces this separability condition.

Typical examples are X ^ n - 1, and its factors such as the cyclotomic polynomial Φ_n, over a ring in which n is invertible.

References

• Mathlib's Mathlib.RingTheory.Etale.StandardEtale, for StandardEtalePair and its universal mapping API.
• Stacks Project, Definition 10.144.1, for standard étale maps.

theorem Polynomial.Monic.isStandardEtale_adjoinRoot {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.Monic) (hs : f.Separable) : Algebra.IsStandardEtale R (AdjoinRoot f)

Adjoining a root of a separable monic polynomial gives a standard étale algebra. If f is monic and coprime to its derivative, then R[X]/(f) is standard étale over R; in particular it is étale.

@[simp]

theorem Polynomial.Monic.etale_adjoinRoot_iff {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.Monic) : Algebra.Etale R (AdjoinRoot f) ↔ f.Separable

A monic polynomial defines an étale algebra exactly when it is coprime to its derivative.