Monogenic Extensions

Lean 4 formalization of Lemmas 3.1 and 3.2 from arXiv:2503.07846 (Balçik et al.), proving that finite étale extensions of local rings are monogenic among other results. See our lean blueprint (built from blueprint/).

We are the Algebraic Geometry group at the UW Math AI lab for Autumn 2025 and Winter 2026.

Currently, we are working on upstreaming these results into Mathlib.

Theorems

Lemma 3.2 (étale case): A finite injective étale extension of local rings R → S is monogenic:

• Monogenic.exists_adjoin_eq_top — ∃ β ∈ S, R[β] = S
• Monogenic.isUnit_aeval_derivative_minpoly_of_adjoin_eq_top — f'(β) ∈ S×, where f = minpoly_R β
• IsAdjoinRootMonic.mkOfAdjoinEqTop' — constructs the isomorphism S ≅ R[X]/(f) (from Module.Free, no IsIntegrallyClosed required). In mathlib, Algebra.adjoin R {β} = ⊤ means that there is a surjective map R[X] → S, whereas IsAdjoinRootMonic S f means that this surjective map's kernel is the principal ideal (in this case generated by the minimal polynomial of β). Thus, we need this theorem.

Converse (IsAdjoinRootMonic.algebra_etale): If S ≅ R[X]/(f) with f monic and f'(β) a unit, then R → S is étale.

Lemma 3.1 (partial étale case, Monogenic.exists_isAdjoinRootMonic_of_quotientMap_etale): Let R, S be local domains with R integrally closed and S a UFD (follows from being regular local rings). If R → S is finite injective and there exists a height-1 prime q ⊂ S such that R/(q ∩ R) → S/q is étale, then S ≅ R[X]/(f) for some monic f.

Files

• Monogenic.lean — root import
• Monogenic/Generator.lean — Lemma 3.2 and the converse
• Monogenic/MonogenicOfNonEtale.lean — Lemma 3.1
• blueprint/src/content.tex - Lean blueprint

Build

lake exe cache get   # fetch prebuilt mathlib cache
lake build

Uses Lean 4 with Mathlib. Key dependencies: Mathlib.RingTheory.Etale.StandardEtale, Mathlib.RingTheory.IsAdjoinRoot, Mathlib.RingTheory.Unramified.LocalRing, Mathlib.RingTheory.Ideal.Height.