Monogenic generators for étale extensions of local rings

Given a finite étale extension R → S of local rings, we construct a single generator β ∈ S such that S ≅ R[X]/(minpoly R β) as R-algebras, and show the derivative f'(β) is a unit. This formalizes Lemma 3.2 of arXiv:2503.07846 (Balçik et al.). We also prove the converse: if S has such a presentation with unit derivative, then R → S is étale.

Main results

• Monogenic.exists_adjoin_eq_top: a finite étale extension of local rings is generated by a single element.
• Monogenic.isUnit_aeval_derivative_minpoly_of_adjoin_eq_top: the derivative of the minimal polynomial at the generator is a unit.
• IsAdjoinRootMonic.mkOfAdjoinEqTop': if Algebra.adjoin R {α} = ⊤ and S is a finite free R-module, then S ≅ R[X]/(minpoly R α) as an R-algebra.
• IsAdjoinRootMonic.algebra_etale: the converse — if S ≅ R[X]/(f) with f monic and f'(root) a unit, then R → S is étale.

Key intermediate results

• minpoly.natDegree_le': the degree of the minimal polynomial is at most finrank R S, proved via Cayley–Hamilton.
• Monogenic.minpoly_map_residue: for étale extensions, the minimal polynomial reduces to the minimal polynomial over the residue field.
• Monogenic.adjoin_eq_top_of_quotient: Nakayama-type argument lifting generation from a quotient S/q to S.

References

• Balçik et al., Monogenic generators for étale extensions of local rings

Tags

étale, monogenic, local ring, minimal polynomial

theorem minpoly.natDegree_le' {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S] [Module.Free R S] [Nontrivial R] {x : S} : (minpoly R x).natDegree ≤ Module.finrank R S

For finite free modules over a nontrivial ring, the degree of the minimal polynomial of any element is bounded by the rank of the module

noncomputable def IsAdjoinRootMonic.mkOfAdjoinEqTop' {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S] [Module.Free R S] [Nontrivial R] {α : S} (hα : Algebra.adjoin R {α} = ⊤) : IsAdjoinRootMonic S (minpoly R α)

If Algebra.adjoin R {α} = ⊤ and S is a finite free R-module, then S ≅ R[X]/(minpoly R α) as an R-algebra.

This avoids the IsIntegrallyClosed hypothesis by using Cayley–Hamilton to bound the degree, quotient rank for the reverse bound, and the Orzech property for injectivity of the evaluation map.

Equations

• IsAdjoinRootMonic.mkOfAdjoinEqTop' hα = { map := Polynomial.aeval α, map_surjective := ⋯, ker_map := ⋯, monic := ⋯ }

Helper lemmas for the derivative unit condition

A key fact from Lemma 3.2 of arXiv:2503.07846 is that for a finite étale extension of local rings, the derivative of the minimal polynomial evaluated at the generator is a unit.

The proof proceeds through the residue fields:

1. Since R -> S is étale, the residue field extension R / m_R → S / m_S is separable
2. For separable extensions, the minimal polynomial is separable.
3. Separable polynomial ⟹ derivative at root is non-zero
4. Non-zero in residue field ⟹ unit in local ring

theorem Monogenic.adjoin_residue_eq_top_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] {β : S} (hβ_gen : Algebra.adjoin R {β} = ⊤) : Algebra.adjoin (IsLocalRing.ResidueField R) {(IsLocalRing.residue S) β} = ⊤

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

theorem Monogenic.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 (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)

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

theorem Monogenic.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 : Algebra.adjoin R {β} = ⊤) : Polynomial.map (IsLocalRing.residue R) (minpoly R β) = minpoly (IsLocalRing.ResidueField R) ((IsLocalRing.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 Monogenic.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 : Algebra.adjoin 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.

Nakayama helpers for the quotient-lifting argument

These lemmas support the proof that Algebra.adjoin R {β} = ⊤ when β generates the quotient S/q over R/(q ∩ R), and a suitable element π ∈ Algebra.adjoin R {β} generates the maximal ideal modulo mR · S.

theorem Monogenic.Ideal.pow_le_span_pow_sup {S : Type u_2} [CommRing S] {I J : Ideal S} {π : S} (h : I = Ideal.span {π} ⊔ J) (k : ℕ) : I ^ k ≤ Ideal.span {π ^ k} ⊔ J

If I = ⟨π⟩ + J, then I^k ≤ ⟨π^k⟩ + J. Pure ideal arithmetic.

theorem Monogenic.exists_adjoin_sub_mem {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (β : S) (q : Ideal S) (h_gen : Algebra.adjoin (R ⧸ Ideal.comap (algebraMap R S) q) {(Ideal.Quotient.mk q) β} = ⊤) (s : S) : ∃ t ∈ Algebra.adjoin R {β}, s - t ∈ q

If (R/p)[β] = S/q where p = q.comap φ, then every element of S is congruent to an element of R[β] modulo q.

theorem Monogenic.exists_sub_mem_adjoin_of_pow {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {A : Subalgebra R S} {q ms mR_S : Ideal S} {π : S} (h_lift : ∀ (s : S), ∃ t ∈ A, s - t ∈ q) (hπ_mem : π ∈ A) (hπ_ms : π ∈ ms) (hq_le : q ≤ ms) (h_ms : ms = Ideal.span {π} ⊔ mR_S) (k : ℕ) (x : S) : ∃ a ∈ Subalgebra.toSubmodule A, x - a ∈ Ideal.span {π ^ k} ⊔ mR_S

Iterative approximation: each x can be approximated by an element of A modulo ⟨π^k⟩ + mR·S.

theorem Monogenic.adjoin_eq_top_of_quotient {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing R] [IsLocalRing S] [Module.Finite R S] (β : S) (q : Ideal S) [q.IsPrime] (h_gen : Algebra.adjoin (R ⧸ Ideal.comap (algebraMap R S) q) {(Ideal.Quotient.mk q) β} = ⊤) (π : S) (hπ_mem : π ∈ Algebra.adjoin R {β}) (h_ms : IsLocalRing.maximalIdeal S = Ideal.span {π} ⊔ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R)) : Algebra.adjoin R {β} = ⊤

If (R/p)[β] = S/q and m_S = ⟨π⟩ + m_R · S for some π ∈ R[β], then R[β] = S. The proof combines quotient lifting, Artinian descent on S/m_R·S, iterative approximation, and Nakayama's lemma.

theorem Monogenic.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.Etale R S] : ∃ (β : S), Algebra.adjoin 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.

Converse: monogenic with unit derivative implies étale

The converse direction: if S ≅ R[X]/(f) with f monic and f'(root) a unit, then the algebra map R → S is étale. This completes the characterization: for finite local extensions, étale with single generator is equivalent to monogenic with unit derivative (i.e., standard étale).

theorem IsAdjoinRootMonic.algebra_etale {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {f : Polynomial R} (adj : IsAdjoinRootMonic S f) (hunit : IsUnit ((Polynomial.aeval adj.root) (Polynomial.derivative f))) : Algebra.Etale R S

If S ≅ R[X]/(f) with f monic and f'(root) a unit in S, then R → S is étale. This is the converse of isUnit_aeval_derivative_minpoly: together they show that for finite extensions of local rings, the étale condition is equivalent to being a monogenic extension with unit derivative.

The proof constructs a StandardEtalePresentation using the pair (f, f'): since f' · 1 + f · 0 = f'^1, the derivative condition gives the Bézout-type relation needed for standard étaleness.