Étale extensions of local rings

We prove that a finite étale extension of local rings is monogenic (generated by a single element), and that the derivative of the minimal polynomial evaluated at the generator is a unit. These are parts 1 and 2 of Lemma 3.2 of arXiv:2503.07846.

Main results

• IsLocalRing.exists_adjoin_eq_top: a finite étale extension of local rings is generated by a single element (Lemma 3.2, part 1).
• IsLocalRing.isUnit_aeval_derivative_minpoly_of_adjoin_eq_top: if R → S is étale and R[β] = S, then f'(β) is a unit, where f = minpoly R β (Lemma 3.2, part 2).

Key intermediate results

• IsLocalRing.adjoin_residue_eq_top_iff_adjoin_eq_top: β generates S over R iff β mod m_S generates S/m_S over R/m_R.
• IsLocalRing.finrank_eq_finrank_residueField: for finite étale extensions of local rings, finrank R S = finrank (ResidueField R) (ResidueField S).
• IsLocalRing.minpoly_map_residue: the minimal polynomial of β over R maps to the minimal polynomial of β mod m_S over the residue field.

Future work

The following results from arXiv:2503.07846 (formalized at uw-math-ai/monogenic-extensions) are planned for future PRs:

• Converse: If S ≅ R[X]/(f) with f monic and f'(root) a unit, then R → S is étale.
• Lemma 3.1 (partial étale case): If R and S are local integral domains with R integrally closed, S a UFD, R → S finite and injective, and there exists a height-one prime q ⊆ S such that R/(q ∩ R) → S/q is étale, then S ≅ R[X]/(f) for some monic f.

Tags

étale, monogenic, local ring, minimal polynomial, residue field

theorem IsLocalRing.adjoin_residue_eq_top_iff_adjoin_eq_top {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing S] [IsLocalRing R] [Module.Finite R S] [FaithfulSMul R S] [Algebra.FormallyUnramified R S] (β : S) : (ResidueField R)[(residue S) β] = ⊤ ↔ R[β] = ⊤

When β generates S over R, the residue β₀ = β mod m_S generates S/m_S over R/m_R.

theorem IsLocalRing.exists_adjoin_eq_top {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing S] [IsLocalRing R] [Module.Finite R S] [FaithfulSMul R S] [Algebra.FormallyUnramified R S] : ∃ (β : S), R[β] = ⊤

A finite étale extension of local rings is generated by a single element. This is Lemma 3.2, part 1 of arXiv:2503.07846. The proof lifts a primitive element of the residue field extension via Nakayama's lemma.

theorem IsLocalRing.finrank_eq_finrank_residueField {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing S] [IsLocalRing R] [Module.Finite R S] [FaithfulSMul R S] [Algebra.Etale R S] : Module.finrank R S = Module.finrank (ResidueField R) (ResidueField S)

For finite étale extensions of local rings, finrank R S = finrank (ResidueField R) (ResidueField S).

theorem IsLocalRing.minpoly_map_residue {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing S] [IsLocalRing R] [Module.Finite R S] [FaithfulSMul R S] [Algebra.Etale R S] {β : S} (hadj : R[β] = ⊤) : Polynomial.map (residue R) (minpoly R β) = minpoly (ResidueField R) ((residue S) β)

For a monogenic étale extension of local rings, the minimal polynomial of β maps to the minimal polynomial of β mod m_S over the residue field.

theorem IsLocalRing.isUnit_aeval_derivative_minpoly_of_adjoin_eq_top {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing S] [IsLocalRing R] [Module.Finite R S] [FaithfulSMul R S] [Algebra.Etale R S] {β : S} (hadj : R[β] = ⊤) : IsUnit ((Polynomial.aeval β) (Polynomial.derivative (minpoly R β)))

If R → S is étale and R[β] = S, then f'(β) is a unit in S, where f = minpoly R β. The proof reduces to separability of the residue field extension via minpoly_map_residue.