From 4e97b6a7abf709788d2348d0050c889d4a311c1c Mon Sep 17 00:00:00 2001
From: Grant Yang <rotartsi0482@gmail.com>
Date: Sat, 28 Feb 2026 17:54:31 -0800
Subject: [PATCH 01/11] feat(RingTheory/IsAdjoinRoot): mkOfAdjoinEqTop'
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Alternative hypothesis to existing theorem: prove the result from a Module.Free hypothesis instead of IsIntegrallyClosed. If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`.

Co-authored-by: George Peykanu <gpeyka@uw.edu>
Co-authored-by: Bryan Boehnke <bryanboehnke@gmail.com>
Co-authored-by: Bianca Viray <67076332+b-viray@users.noreply.github.com>
---
 Mathlib/RingTheory/IsAdjoinRoot.lean | 47 ++++++++++++++++++++++++++++
 1 file changed, 47 insertions(+)

diff --git a/Mathlib/RingTheory/IsAdjoinRoot.lean b/Mathlib/RingTheory/IsAdjoinRoot.lean
index 11d91121df6519..3b035d3ce040c8 100644
--- a/Mathlib/RingTheory/IsAdjoinRoot.lean
+++ b/Mathlib/RingTheory/IsAdjoinRoot.lean
@@ -616,6 +616,53 @@ theorem mkOfAdjoinEqTop_root : (IsAdjoinRoot.mkOfAdjoinEqTop hα hα₂).root =
 
 end mkOfAdjoinEqTop
 
+section mkOfAdjoinEqTop'
+
+variable [Module.Finite R S] [Module.Free R S] [Nontrivial R]
+
+/-- For finite free modules over a nontrivial ring,
+the degree of the minimal polynomials is bounded by the rank of the module -/
+theorem _root_.minpoly.natDegree_le' (α : S) :
+    (minpoly R α).natDegree ≤ Module.finrank R S := by
+  classical
+  let b := Module.Free.chooseBasis R S
+  let M := LinearMap.toMatrixAlgEquiv b (Algebra.lmul R S α)
+  have haeval : aeval α M.charpoly = 0 := by
+    have h := Matrix.aeval_self_charpoly M
+    rwa [aeval_algHom_apply, _root_.map_eq_zero_iff _ (LinearMap.toMatrixAlgEquiv b).injective,
+      aeval_algHom_apply, _root_.map_eq_zero_iff _ Algebra.lmul_injective] at h
+  exact (natDegree_le_natDegree (minpoly.min R α M.charpoly_monic haeval)).trans
+    (M.charpoly_natDegree_eq_dim.trans (Module.finrank_eq_card_chooseBasisIndex R S).symm).le
+
+/-- If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`. -/
+noncomputable def _root_.IsAdjoinRootMonic.mkOfAdjoinEqTop'
+    {α : S} (hα : Algebra.adjoin R {α} = ⊤) :
+    IsAdjoinRootMonic S (minpoly R α) := by
+  set f := minpoly R α
+  have hf : f.Monic := minpoly.monic (Algebra.IsIntegral.isIntegral α)
+  haveI := hf.free_adjoinRoot; haveI := hf.finite_adjoinRoot
+  let φ : AdjoinRoot f →ₐ[R] S :=
+    AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α (minpoly.aeval R α)
+  have hφ_surj : Function.Surjective φ := by
+    rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at hα
+    exact fun s =>
+      let ⟨p, hp⟩ := hα s; ⟨AdjoinRoot.mk f p, by simp [φ, ← aeval_def, hp]⟩
+  have hrank : f.natDegree = Module.finrank R S := le_antisymm (minpoly.natDegree_le' α) (by
+    have e := φ.toLinearMap.quotKerEquivRange.trans
+      (LinearEquiv.ofTop _ (LinearMap.range_eq_top.mpr hφ_surj))
+    rw [← e.finrank_eq]
+    exact (Submodule.finrank_quotient_le _).trans (finrank_quotient_span_eq_natDegree' hf).le)
+  have e := LinearEquiv.ofFinrankEq (R := R) (AdjoinRoot f) S
+    ((finrank_quotient_span_eq_natDegree' hf).trans hrank)
+  have hφ_inj : Function.Injective φ :=
+    fun x y h => OrzechProperty.injective_of_surjective_endomorphism
+    (e.symm.toLinearMap.comp φ.toLinearMap) (e.symm.surjective.comp hφ_surj) (congr_arg e.symm h)
+  exact
+    { IsAdjoinRoot.ofAdjoinRootEquiv
+        (AlgEquiv.ofBijective φ ⟨hφ_inj, hφ_surj⟩) with monic := hf }
+
+end mkOfAdjoinEqTop'
+
 section Equiv
 
 variable {T : Type*} [CommRing T] [Algebra R T] (h' : IsAdjoinRoot T f) {U : Type*} [CommRing U]

From 0544dfd1c7e567162ea38458375c42559a02c6bf Mon Sep 17 00:00:00 2001
From: Grant Yang <rotartsi0482@gmail.com>
Date: Sat, 28 Feb 2026 19:12:25 -0800
Subject: [PATCH 02/11] feat(LocalRing/Etale): Finite etale extensions are
 monogenic
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Formalization of lemma 3.2 from https://arxiv.org/abs/2503.07846: Given a local finite ring extension R -> S, if the algebraMap is etale, then there exists a β ∈ S such that R[β] = S. Furthermore, if f(z) ∈ R[z] is the minimal polynomial of β, then f′(β) ∈ S×.
---
 Mathlib.lean                            |   1 +
 Mathlib/RingTheory/LocalRing/Etale.lean | 172 ++++++++++++++++++++++++
 2 files changed, 173 insertions(+)
 create mode 100644 Mathlib/RingTheory/LocalRing/Etale.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 41fcf3dd929beb..56ed56e8a7dcf3 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -6466,6 +6466,7 @@ public import Mathlib.RingTheory.LocalProperties.Semilocal
 public import Mathlib.RingTheory.LocalProperties.Submodule
 public import Mathlib.RingTheory.LocalRing.Basic
 public import Mathlib.RingTheory.LocalRing.Defs
+public import Mathlib.RingTheory.LocalRing.Etale
 public import Mathlib.RingTheory.LocalRing.LocalSubring
 public import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
 public import Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs
diff --git a/Mathlib/RingTheory/LocalRing/Etale.lean b/Mathlib/RingTheory/LocalRing/Etale.lean
new file mode 100644
index 00000000000000..11c7df7d7c8615
--- /dev/null
+++ b/Mathlib/RingTheory/LocalRing/Etale.lean
@@ -0,0 +1,172 @@
+/-
+Copyright (c) 2026 University of Washington Math AI Lab. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bianca Viray, Bryan Boehnke, Grant Yang, George Peykanu, Tianshuo Wang
+-/
+
+module
+
+public import Mathlib.RingTheory.Unramified.LocalRing
+public import Mathlib.RingTheory.Smooth.Flat
+public import Mathlib.RingTheory.LocalRing.Module
+public import Mathlib.RingTheory.LocalRing.Quotient
+public import Mathlib.RingTheory.IsAdjoinRoot
+
+/-!
+# É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](https://arxiv.org/abs/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_of_adjoin_eq_top`: if `β` generates `S` over `R`, then
+  `β 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](https://arxiv.org/abs/2503.07846) (formalized at [uw-math-ai/monogenic-extensions](https://github.com/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
+-/
+
+@[expose] public section
+
+namespace IsLocalRing
+
+variable {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
+    [IsLocalRing S] [IsLocalRing R] [Module.Finite R S] [FaithfulSMul R S]
+
+open Polynomial in
+/-- A finite étale extension of local rings is generated by a single element.
+This is Lemma 3.2, part 1 of [arXiv:2503.07846](https://arxiv.org/abs/2503.07846).
+The proof lifts a primitive element of the residue field extension via Nakayama's lemma. -/
+theorem exists_adjoin_eq_top [Algebra.Etale R S] :
+    ∃ β : S, Algebra.adjoin R {β} = ⊤ := by
+  obtain ⟨β₀, hβ₀⟩ := Field.exists_primitive_element (IsLocalRing.ResidueField R)
+    (IsLocalRing.ResidueField S)
+  obtain ⟨β, hβ⟩ := Ideal.Quotient.mk_surjective β₀
+  refine ⟨β, ?_⟩
+  have h_adjoin_top : Algebra.adjoin (IsLocalRing.ResidueField R) {β₀} = ⊤ := by
+    rw [← IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic
+      (Algebra.IsAlgebraic.isAlgebraic β₀), hβ₀, IntermediateField.top_toSubalgebra]
+  rw [show β₀ = IsLocalRing.residue S β from hβ.symm,
+    Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at h_adjoin_top
+  set mR := IsLocalRing.maximalIdeal R
+  have h_le_sup : (⊤ : Submodule R S) ≤ (Algebra.adjoin R {β}).toSubmodule ⊔ mR • ⊤ := by
+    intro s _
+    obtain ⟨p, hp⟩ := h_adjoin_top (IsLocalRing.residue S s)
+    obtain ⟨q, rfl⟩ := Polynomial.map_surjective _ IsLocalRing.residue_surjective p
+    rw [Ideal.smul_top_eq_map]
+    refine Submodule.mem_sup.mpr ⟨aeval β q, ?_, s - aeval β q, ?_, by ring⟩
+    · rw [Algebra.adjoin_singleton_eq_range_aeval]; exact ⟨q, rfl⟩
+    · exact (Algebra.FormallyUnramified.map_maximalIdeal (R := R) (S := S)) ▸
+        Ideal.Quotient.eq.mp
+          (show IsLocalRing.residue S s = IsLocalRing.residue S (aeval β q) by
+            rw [map_aeval_eq_aeval_map (ψ := IsLocalRing.residue S)
+              (φ := IsLocalRing.residue R) rfl, hp])
+  exact eq_top_iff.mpr (Submodule.le_of_le_smul_of_le_jacobson_bot
+    (Module.finite_def.mp inferInstance) (IsLocalRing.maximalIdeal_le_jacobson ⊥) h_le_sup)
+
+-- ResidueField.Basic does not import Algebra stuff.
+/-- When `β` generates `S` over `R`, the residue `β₀ = β mod m_S`
+generates `S/m_S` over `R/m_R`. -/
+lemma adjoin_residue_eq_top_of_adjoin_eq_top
+    {β : S} (hβ_gen : Algebra.adjoin R {β} = ⊤) :
+    Algebra.adjoin (IsLocalRing.ResidueField R) {IsLocalRing.residue S β} = ⊤ := by
+  rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at *
+  intro x
+  obtain ⟨s, rfl⟩ := IsLocalRing.residue_surjective (R := S) x
+  obtain ⟨p, rfl⟩ := hβ_gen s
+  exact ⟨p.map (IsLocalRing.residue R),
+    (Polynomial.map_aeval_eq_aeval_map (ψ := IsLocalRing.residue S)
+      (φ := IsLocalRing.residue R) rfl p β).symm⟩
+
+-- Q: Is this in the right level of generality?
+-- consider adding the maximal ideals mapping as an explicit
+-- hypothesis instead of using Algebra.Etale.
+/-- For finite étale extensions of local rings,
+`finrank R S = finrank (ResidueField R) (ResidueField S)`. -/
+lemma finrank_eq_finrank_residueField [Algebra.Etale R S] :
+    Module.finrank R S =
+      Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S) := by
+  haveI : Module.Free R S := Module.free_of_flat_of_isLocalRing
+  have hmaximal : Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R) =
+      IsLocalRing.maximalIdeal S := Algebra.FormallyUnramified.map_maximalIdeal
+  let e : (S ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R))
+      ≃ₗ[R ⧸ IsLocalRing.maximalIdeal R] (S ⧸ IsLocalRing.maximalIdeal S) :=
+    AddEquiv.toLinearEquiv (Ideal.quotEquivOfEq hmaximal).toAddEquiv (fun r x => by
+      obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective r
+      obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
+      simp only [RingEquiv.toAddEquiv_eq_coe]; rfl)
+  erw [← e.finrank_eq, IsLocalRing.finrank_quotient_map (R := R) (S := 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. -/
+lemma minpoly_map_residue [Algebra.Etale R S]
+    {β : S} (hadj : Algebra.adjoin R {β} = ⊤) :
+    (minpoly R β).map (IsLocalRing.residue R) = minpoly (IsLocalRing.ResidueField R)
+      (IsLocalRing.residue S β) := by
+  have hmonic := minpoly.monic <| Algebra.IsIntegral.isIntegral (R:=R) β
+  let kR := IsLocalRing.ResidueField R
+  let β₀ := IsLocalRing.residue S β
+  let f_bar := (minpoly R β).map (IsLocalRing.residue R)
+  have hβ₀_int : IsIntegral kR β₀ := Algebra.IsIntegral.isIntegral β₀
+  -- β₀ is a root of f_bar, so minpoly kR β₀ divides f_bar
+  have hdvd : minpoly kR β₀ ∣ f_bar := minpoly.dvd kR β₀ (by
+    rw [← Polynomial.map_aeval_eq_aeval_map (ψ := IsLocalRing.residue S)
+      (φ := IsLocalRing.residue R) rfl, minpoly.aeval, map_zero])
+  have hβ₀_gen : Algebra.adjoin kR {β₀} = ⊤ := adjoin_residue_eq_top_of_adjoin_eq_top hadj
+  have hβ₀_field_gen : IntermediateField.adjoin kR {β₀} = ⊤ := by
+    rw [← IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic
+      (Algebra.IsAlgebraic.isAlgebraic β₀)] at hβ₀_gen
+    exact IntermediateField.toSubalgebra_injective hβ₀_gen
+  have hdeg_eq : f_bar.natDegree = (minpoly kR β₀).natDegree := by
+    haveI : Module.Free R S := Module.free_of_flat_of_isLocalRing
+    rw [hmonic.natDegree_map _,
+      ← (IsAdjoinRootMonic.mkOfAdjoinEqTop' hadj).finrank,
+      finrank_eq_finrank_residueField, ← IntermediateField.finrank_top', ← hβ₀_field_gen,
+      IntermediateField.adjoin.finrank hβ₀_int]
+  exact Polynomial.eq_of_monic_of_dvd_of_natDegree_le (minpoly.monic hβ₀_int)
+    (hmonic.map _) hdvd hdeg_eq.le
+
+open Polynomial in
+/-- 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`. -/
+lemma isUnit_aeval_derivative_minpoly_of_adjoin_eq_top
+    [Algebra.Etale R S] {β : S}
+    (hadj : Algebra.adjoin R {β} = ⊤) :
+    IsUnit (aeval β (minpoly R β).derivative) := by
+  apply fun s => (IsLocalRing.residue_ne_zero_iff_isUnit s).mp
+  let kR := IsLocalRing.ResidueField R
+  let β₀ := IsLocalRing.residue S β
+  have hderiv_ne_zero : aeval β₀ (minpoly kR β₀).derivative ≠ 0 :=
+    (Algebra.IsSeparable.isSeparable kR β₀).aeval_derivative_ne_zero (minpoly.aeval kR β₀)
+  rw [map_aeval_eq_aeval_map (ψ := IsLocalRing.residue S)
+    (φ := IsLocalRing.residue R) rfl, ← derivative_map, minpoly_map_residue hadj]
+  exact hderiv_ne_zero
+
+end IsLocalRing
+
+end

From a12e7f2d00435a7c203da4c254c32550d62a875c Mon Sep 17 00:00:00 2001
From: Grant Yang <rotartsi0482@gmail.com>
Date: Wed, 4 Mar 2026 17:07:31 -0800
Subject: [PATCH 03/11] simp lemma + update mathlib

---
 Mathlib/RingTheory/IsAdjoinRoot.lean | 24 +++++++++++++++---------
 1 file changed, 15 insertions(+), 9 deletions(-)

diff --git a/Mathlib/RingTheory/IsAdjoinRoot.lean b/Mathlib/RingTheory/IsAdjoinRoot.lean
index 3b035d3ce040c8..a4ec862ea22b75 100644
--- a/Mathlib/RingTheory/IsAdjoinRoot.lean
+++ b/Mathlib/RingTheory/IsAdjoinRoot.lean
@@ -624,23 +624,22 @@ variable [Module.Finite R S] [Module.Free R S] [Nontrivial R]
 the degree of the minimal polynomials is bounded by the rank of the module -/
 theorem _root_.minpoly.natDegree_le' (α : S) :
     (minpoly R α).natDegree ≤ Module.finrank R S := by
-  classical
-  let b := Module.Free.chooseBasis R S
+  have b := Module.Free.chooseBasis R S
   let M := LinearMap.toMatrixAlgEquiv b (Algebra.lmul R S α)
-  have haeval : aeval α M.charpoly = 0 := by
-    have h := Matrix.aeval_self_charpoly M
-    rwa [aeval_algHom_apply, _root_.map_eq_zero_iff _ (LinearMap.toMatrixAlgEquiv b).injective,
-      aeval_algHom_apply, _root_.map_eq_zero_iff _ Algebra.lmul_injective] at h
-  exact (natDegree_le_natDegree (minpoly.min R α M.charpoly_monic haeval)).trans
+  refine (natDegree_le_natDegree (minpoly.min R α M.charpoly_monic ?_)).trans
     (M.charpoly_natDegree_eq_dim.trans (Module.finrank_eq_card_chooseBasisIndex R S).symm).le
+  let h := Matrix.aeval_self_charpoly M
+  rwa [aeval_algHom_apply, _root_.map_eq_zero_iff _ (LinearMap.toMatrixAlgEquiv b).injective,
+    aeval_algHom_apply, _root_.map_eq_zero_iff _ Algebra.lmul_injective] at h
 
 /-- If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`. -/
-noncomputable def _root_.IsAdjoinRootMonic.mkOfAdjoinEqTop'
+def _root_.IsAdjoinRootMonic.mkOfAdjoinEqTop'
     {α : S} (hα : Algebra.adjoin R {α} = ⊤) :
     IsAdjoinRootMonic S (minpoly R α) := by
   set f := minpoly R α
   have hf : f.Monic := minpoly.monic (Algebra.IsIntegral.isIntegral α)
-  haveI := hf.free_adjoinRoot; haveI := hf.finite_adjoinRoot
+  letI : Module R (AdjoinRoot f) := Algebra.toModule
+  haveI := hf.free_adjoinRoot; haveI finite := hf.finite_adjoinRoot
   let φ : AdjoinRoot f →ₐ[R] S :=
     AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α (minpoly.aeval R α)
   have hφ_surj : Function.Surjective φ := by
@@ -661,6 +660,13 @@ noncomputable def _root_.IsAdjoinRootMonic.mkOfAdjoinEqTop'
     { IsAdjoinRoot.ofAdjoinRootEquiv
         (AlgEquiv.ofBijective φ ⟨hφ_inj, hφ_surj⟩) with monic := hf }
 
+@[simp]
+lemma _root_.IsAdjoinRootMonic.mkOfAdjoinEqTop'_map
+    {α : S} {hα : Algebra.adjoin R {α} = ⊤} :
+    (IsAdjoinRootMonic.mkOfAdjoinEqTop' hα).map = (aeval α) := by
+  unfold IsAdjoinRootMonic.mkOfAdjoinEqTop'
+  ext; simp
+
 end mkOfAdjoinEqTop'
 
 section Equiv

From 3f93f0b919497ade861d1f838247209f1a17766f Mon Sep 17 00:00:00 2001
From: Grant Yang <rotartsi0482@gmail.com>
Date: Mon, 9 Mar 2026 16:13:52 -0700
Subject: [PATCH 04/11] move lemmas

---
 Mathlib/FieldTheory/Minpoly/Basic.lean | 16 +++++
 Mathlib/RingTheory/IsAdjoinRoot.lean   | 82 +++++++++++++-------------
 2 files changed, 57 insertions(+), 41 deletions(-)

diff --git a/Mathlib/FieldTheory/Minpoly/Basic.lean b/Mathlib/FieldTheory/Minpoly/Basic.lean
index cc1e574160935b..c222fc9f84bbb7 100644
--- a/Mathlib/FieldTheory/Minpoly/Basic.lean
+++ b/Mathlib/FieldTheory/Minpoly/Basic.lean
@@ -6,6 +6,9 @@ Authors: Chris Hughes, Johan Commelin
 module
 
 public import Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
+public import Mathlib.LinearAlgebra.Dimension.Finrank
+import Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
+import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
 
 /-!
 # Minimal polynomials
@@ -236,6 +239,19 @@ theorem two_le_natDegree_subalgebra {B} [CommRing B] [Algebra A B] [Nontrivial B
   rw [two_le_natDegree_iff int, Iff.not]
   apply Set.ext_iff.mp Subtype.range_val_subtype
 
+omit [Nontrivial B] in
+/-- For finite free modules over a nontrivial ring,
+the degree of the minimal polynomials is bounded by the rank of the module -/
+theorem natDegree_le' [Module.Finite A B] [Module.Free A B] [Nontrivial A] :
+    (minpoly A x).natDegree ≤ Module.finrank A B := by
+  have b := Module.Free.chooseBasis A B
+  let M := LinearMap.toMatrixAlgEquiv b (Algebra.lmul A B x)
+  refine (natDegree_le_natDegree (minpoly.min A x M.charpoly_monic ?_)).trans
+    (M.charpoly_natDegree_eq_dim.trans (Module.finrank_eq_card_chooseBasisIndex A B).symm).le
+  let h := Matrix.aeval_self_charpoly M
+  rwa [aeval_algHom_apply, _root_.map_eq_zero_iff _ (LinearMap.toMatrixAlgEquiv b).injective,
+    aeval_algHom_apply, _root_.map_eq_zero_iff _ Algebra.lmul_injective] at h
+
 end
 
 /-- If `B/A` is an injective ring extension, and `a` is an element of `A`,
diff --git a/Mathlib/RingTheory/IsAdjoinRoot.lean b/Mathlib/RingTheory/IsAdjoinRoot.lean
index a4ec862ea22b75..ed0176931471ab 100644
--- a/Mathlib/RingTheory/IsAdjoinRoot.lean
+++ b/Mathlib/RingTheory/IsAdjoinRoot.lean
@@ -616,24 +616,55 @@ theorem mkOfAdjoinEqTop_root : (IsAdjoinRoot.mkOfAdjoinEqTop hα hα₂).root =
 
 end mkOfAdjoinEqTop
 
+section Equiv
+
+variable {T : Type*} [CommRing T] [Algebra R T] (h' : IsAdjoinRoot T f) {U : Type*} [CommRing U]
+
+@[simp]
+theorem lift_algEquiv (i : R →+* U) (x hx z) :
+    h'.lift i x hx (h.algEquiv h' z) = h.lift i x hx z := by rw [← h.map_repr z]; simp [-map_repr]
+
+@[simp]
+theorem liftHom_algEquiv [Algebra R U] (x : U) (hx z) :
+    h'.liftHom x hx (h.algEquiv h' z) = h.liftHom x hx z := h.lift_algEquiv h' _ _ hx _
+
+end Equiv
+
+end IsAdjoinRoot
+
+namespace IsAdjoinRootMonic
+
+variable (h : IsAdjoinRootMonic S f)
+
+theorem minpoly_eq [IsDomain R] [IsDomain S] [IsTorsionFree R S] [IsIntegrallyClosed R]
+  (hirr : Irreducible f) : minpoly R h.root = f :=
+  let ⟨q, hq⟩ := minpoly.isIntegrallyClosed_dvd h.isIntegral_root h.aeval_root_self
+  symm <|
+    eq_of_monic_of_associated h.monic (minpoly.monic h.isIntegral_root) <| by
+      convert
+        Associated.mul_left (minpoly R h.root) <|
+          associated_one_iff_isUnit.2 <|
+            (hirr.isUnit_or_isUnit hq).resolve_left <| minpoly.not_isUnit R h.root
+      rw [mul_one]
+
 section mkOfAdjoinEqTop'
 
 variable [Module.Finite R S] [Module.Free R S] [Nontrivial R]
 
-/-- For finite free modules over a nontrivial ring,
-the degree of the minimal polynomials is bounded by the rank of the module -/
-theorem _root_.minpoly.natDegree_le' (α : S) :
-    (minpoly R α).natDegree ≤ Module.finrank R S := by
-  have b := Module.Free.chooseBasis R S
-  let M := LinearMap.toMatrixAlgEquiv b (Algebra.lmul R S α)
-  refine (natDegree_le_natDegree (minpoly.min R α M.charpoly_monic ?_)).trans
-    (M.charpoly_natDegree_eq_dim.trans (Module.finrank_eq_card_chooseBasisIndex R S).symm).le
+-- theorem could be placed here with 0 imports, but
+-- it does not logically make sense.
+theorem alternate_natDegree_le' :
+    (minpoly A x).natDegree ≤ Module.finrank A B := by
+  have b := Module.Free.chooseBasis A B
+  let M := LinearMap.toMatrixAlgEquiv b (Algebra.lmul A B x)
+  refine (natDegree_le_natDegree (minpoly.min A x M.charpoly_monic ?_)).trans
+    (M.charpoly_natDegree_eq_dim.trans (Module.finrank_eq_card_chooseBasisIndex A B).symm).le
   let h := Matrix.aeval_self_charpoly M
   rwa [aeval_algHom_apply, _root_.map_eq_zero_iff _ (LinearMap.toMatrixAlgEquiv b).injective,
     aeval_algHom_apply, _root_.map_eq_zero_iff _ Algebra.lmul_injective] at h
 
 /-- If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`. -/
-def _root_.IsAdjoinRootMonic.mkOfAdjoinEqTop'
+def mkOfAdjoinEqTop'
     {α : S} (hα : Algebra.adjoin R {α} = ⊤) :
     IsAdjoinRootMonic S (minpoly R α) := by
   set f := minpoly R α
@@ -661,7 +692,7 @@ def _root_.IsAdjoinRootMonic.mkOfAdjoinEqTop'
         (AlgEquiv.ofBijective φ ⟨hφ_inj, hφ_surj⟩) with monic := hf }
 
 @[simp]
-lemma _root_.IsAdjoinRootMonic.mkOfAdjoinEqTop'_map
+lemma mkOfAdjoinEqTop'_map
     {α : S} {hα : Algebra.adjoin R {α} = ⊤} :
     (IsAdjoinRootMonic.mkOfAdjoinEqTop' hα).map = (aeval α) := by
   unfold IsAdjoinRootMonic.mkOfAdjoinEqTop'
@@ -669,37 +700,6 @@ lemma _root_.IsAdjoinRootMonic.mkOfAdjoinEqTop'_map
 
 end mkOfAdjoinEqTop'
 
-section Equiv
-
-variable {T : Type*} [CommRing T] [Algebra R T] (h' : IsAdjoinRoot T f) {U : Type*} [CommRing U]
-
-@[simp]
-theorem lift_algEquiv (i : R →+* U) (x hx z) :
-    h'.lift i x hx (h.algEquiv h' z) = h.lift i x hx z := by rw [← h.map_repr z]; simp [-map_repr]
-
-@[simp]
-theorem liftHom_algEquiv [Algebra R U] (x : U) (hx z) :
-    h'.liftHom x hx (h.algEquiv h' z) = h.liftHom x hx z := h.lift_algEquiv h' _ _ hx _
-
-end Equiv
-
-end IsAdjoinRoot
-
-namespace IsAdjoinRootMonic
-
-variable (h : IsAdjoinRootMonic S f)
-
-theorem minpoly_eq [IsDomain R] [IsDomain S] [IsTorsionFree R S] [IsIntegrallyClosed R]
-  (hirr : Irreducible f) : minpoly R h.root = f :=
-  let ⟨q, hq⟩ := minpoly.isIntegrallyClosed_dvd h.isIntegral_root h.aeval_root_self
-  symm <|
-    eq_of_monic_of_associated h.monic (minpoly.monic h.isIntegral_root) <| by
-      convert
-        Associated.mul_left (minpoly R h.root) <|
-          associated_one_iff_isUnit.2 <|
-            (hirr.isUnit_or_isUnit hq).resolve_left <| minpoly.not_isUnit R h.root
-      rw [mul_one]
-
 end IsAdjoinRootMonic
 
 section Algebra

From 5428c30b8c4b0fb9ca1f8c023347a3610ef00f9b Mon Sep 17 00:00:00 2001
From: Grant Yang <rotartsi0482@gmail.com>
Date: Mon, 9 Mar 2026 16:18:47 -0700
Subject: [PATCH 05/11] Revert "feat(LocalRing/Etale): Finite etale extensions
 are monogenic"

This reverts commit cc73956ac13ce055d398d2cf08f4bf0818a6296c.
---
 Mathlib.lean                            |   1 -
 Mathlib/RingTheory/LocalRing/Etale.lean | 172 ------------------------
 2 files changed, 173 deletions(-)
 delete mode 100644 Mathlib/RingTheory/LocalRing/Etale.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 56ed56e8a7dcf3..41fcf3dd929beb 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -6466,7 +6466,6 @@ public import Mathlib.RingTheory.LocalProperties.Semilocal
 public import Mathlib.RingTheory.LocalProperties.Submodule
 public import Mathlib.RingTheory.LocalRing.Basic
 public import Mathlib.RingTheory.LocalRing.Defs
-public import Mathlib.RingTheory.LocalRing.Etale
 public import Mathlib.RingTheory.LocalRing.LocalSubring
 public import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
 public import Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs
diff --git a/Mathlib/RingTheory/LocalRing/Etale.lean b/Mathlib/RingTheory/LocalRing/Etale.lean
deleted file mode 100644
index 11c7df7d7c8615..00000000000000
--- a/Mathlib/RingTheory/LocalRing/Etale.lean
+++ /dev/null
@@ -1,172 +0,0 @@
-/-
-Copyright (c) 2026 University of Washington Math AI Lab. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Bianca Viray, Bryan Boehnke, Grant Yang, George Peykanu, Tianshuo Wang
--/
-
-module
-
-public import Mathlib.RingTheory.Unramified.LocalRing
-public import Mathlib.RingTheory.Smooth.Flat
-public import Mathlib.RingTheory.LocalRing.Module
-public import Mathlib.RingTheory.LocalRing.Quotient
-public import Mathlib.RingTheory.IsAdjoinRoot
-
-/-!
-# É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](https://arxiv.org/abs/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_of_adjoin_eq_top`: if `β` generates `S` over `R`, then
-  `β 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](https://arxiv.org/abs/2503.07846) (formalized at [uw-math-ai/monogenic-extensions](https://github.com/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
--/
-
-@[expose] public section
-
-namespace IsLocalRing
-
-variable {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
-    [IsLocalRing S] [IsLocalRing R] [Module.Finite R S] [FaithfulSMul R S]
-
-open Polynomial in
-/-- A finite étale extension of local rings is generated by a single element.
-This is Lemma 3.2, part 1 of [arXiv:2503.07846](https://arxiv.org/abs/2503.07846).
-The proof lifts a primitive element of the residue field extension via Nakayama's lemma. -/
-theorem exists_adjoin_eq_top [Algebra.Etale R S] :
-    ∃ β : S, Algebra.adjoin R {β} = ⊤ := by
-  obtain ⟨β₀, hβ₀⟩ := Field.exists_primitive_element (IsLocalRing.ResidueField R)
-    (IsLocalRing.ResidueField S)
-  obtain ⟨β, hβ⟩ := Ideal.Quotient.mk_surjective β₀
-  refine ⟨β, ?_⟩
-  have h_adjoin_top : Algebra.adjoin (IsLocalRing.ResidueField R) {β₀} = ⊤ := by
-    rw [← IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic
-      (Algebra.IsAlgebraic.isAlgebraic β₀), hβ₀, IntermediateField.top_toSubalgebra]
-  rw [show β₀ = IsLocalRing.residue S β from hβ.symm,
-    Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at h_adjoin_top
-  set mR := IsLocalRing.maximalIdeal R
-  have h_le_sup : (⊤ : Submodule R S) ≤ (Algebra.adjoin R {β}).toSubmodule ⊔ mR • ⊤ := by
-    intro s _
-    obtain ⟨p, hp⟩ := h_adjoin_top (IsLocalRing.residue S s)
-    obtain ⟨q, rfl⟩ := Polynomial.map_surjective _ IsLocalRing.residue_surjective p
-    rw [Ideal.smul_top_eq_map]
-    refine Submodule.mem_sup.mpr ⟨aeval β q, ?_, s - aeval β q, ?_, by ring⟩
-    · rw [Algebra.adjoin_singleton_eq_range_aeval]; exact ⟨q, rfl⟩
-    · exact (Algebra.FormallyUnramified.map_maximalIdeal (R := R) (S := S)) ▸
-        Ideal.Quotient.eq.mp
-          (show IsLocalRing.residue S s = IsLocalRing.residue S (aeval β q) by
-            rw [map_aeval_eq_aeval_map (ψ := IsLocalRing.residue S)
-              (φ := IsLocalRing.residue R) rfl, hp])
-  exact eq_top_iff.mpr (Submodule.le_of_le_smul_of_le_jacobson_bot
-    (Module.finite_def.mp inferInstance) (IsLocalRing.maximalIdeal_le_jacobson ⊥) h_le_sup)
-
--- ResidueField.Basic does not import Algebra stuff.
-/-- When `β` generates `S` over `R`, the residue `β₀ = β mod m_S`
-generates `S/m_S` over `R/m_R`. -/
-lemma adjoin_residue_eq_top_of_adjoin_eq_top
-    {β : S} (hβ_gen : Algebra.adjoin R {β} = ⊤) :
-    Algebra.adjoin (IsLocalRing.ResidueField R) {IsLocalRing.residue S β} = ⊤ := by
-  rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at *
-  intro x
-  obtain ⟨s, rfl⟩ := IsLocalRing.residue_surjective (R := S) x
-  obtain ⟨p, rfl⟩ := hβ_gen s
-  exact ⟨p.map (IsLocalRing.residue R),
-    (Polynomial.map_aeval_eq_aeval_map (ψ := IsLocalRing.residue S)
-      (φ := IsLocalRing.residue R) rfl p β).symm⟩
-
--- Q: Is this in the right level of generality?
--- consider adding the maximal ideals mapping as an explicit
--- hypothesis instead of using Algebra.Etale.
-/-- For finite étale extensions of local rings,
-`finrank R S = finrank (ResidueField R) (ResidueField S)`. -/
-lemma finrank_eq_finrank_residueField [Algebra.Etale R S] :
-    Module.finrank R S =
-      Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S) := by
-  haveI : Module.Free R S := Module.free_of_flat_of_isLocalRing
-  have hmaximal : Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R) =
-      IsLocalRing.maximalIdeal S := Algebra.FormallyUnramified.map_maximalIdeal
-  let e : (S ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R))
-      ≃ₗ[R ⧸ IsLocalRing.maximalIdeal R] (S ⧸ IsLocalRing.maximalIdeal S) :=
-    AddEquiv.toLinearEquiv (Ideal.quotEquivOfEq hmaximal).toAddEquiv (fun r x => by
-      obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective r
-      obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
-      simp only [RingEquiv.toAddEquiv_eq_coe]; rfl)
-  erw [← e.finrank_eq, IsLocalRing.finrank_quotient_map (R := R) (S := 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. -/
-lemma minpoly_map_residue [Algebra.Etale R S]
-    {β : S} (hadj : Algebra.adjoin R {β} = ⊤) :
-    (minpoly R β).map (IsLocalRing.residue R) = minpoly (IsLocalRing.ResidueField R)
-      (IsLocalRing.residue S β) := by
-  have hmonic := minpoly.monic <| Algebra.IsIntegral.isIntegral (R:=R) β
-  let kR := IsLocalRing.ResidueField R
-  let β₀ := IsLocalRing.residue S β
-  let f_bar := (minpoly R β).map (IsLocalRing.residue R)
-  have hβ₀_int : IsIntegral kR β₀ := Algebra.IsIntegral.isIntegral β₀
-  -- β₀ is a root of f_bar, so minpoly kR β₀ divides f_bar
-  have hdvd : minpoly kR β₀ ∣ f_bar := minpoly.dvd kR β₀ (by
-    rw [← Polynomial.map_aeval_eq_aeval_map (ψ := IsLocalRing.residue S)
-      (φ := IsLocalRing.residue R) rfl, minpoly.aeval, map_zero])
-  have hβ₀_gen : Algebra.adjoin kR {β₀} = ⊤ := adjoin_residue_eq_top_of_adjoin_eq_top hadj
-  have hβ₀_field_gen : IntermediateField.adjoin kR {β₀} = ⊤ := by
-    rw [← IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic
-      (Algebra.IsAlgebraic.isAlgebraic β₀)] at hβ₀_gen
-    exact IntermediateField.toSubalgebra_injective hβ₀_gen
-  have hdeg_eq : f_bar.natDegree = (minpoly kR β₀).natDegree := by
-    haveI : Module.Free R S := Module.free_of_flat_of_isLocalRing
-    rw [hmonic.natDegree_map _,
-      ← (IsAdjoinRootMonic.mkOfAdjoinEqTop' hadj).finrank,
-      finrank_eq_finrank_residueField, ← IntermediateField.finrank_top', ← hβ₀_field_gen,
-      IntermediateField.adjoin.finrank hβ₀_int]
-  exact Polynomial.eq_of_monic_of_dvd_of_natDegree_le (minpoly.monic hβ₀_int)
-    (hmonic.map _) hdvd hdeg_eq.le
-
-open Polynomial in
-/-- 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`. -/
-lemma isUnit_aeval_derivative_minpoly_of_adjoin_eq_top
-    [Algebra.Etale R S] {β : S}
-    (hadj : Algebra.adjoin R {β} = ⊤) :
-    IsUnit (aeval β (minpoly R β).derivative) := by
-  apply fun s => (IsLocalRing.residue_ne_zero_iff_isUnit s).mp
-  let kR := IsLocalRing.ResidueField R
-  let β₀ := IsLocalRing.residue S β
-  have hderiv_ne_zero : aeval β₀ (minpoly kR β₀).derivative ≠ 0 :=
-    (Algebra.IsSeparable.isSeparable kR β₀).aeval_derivative_ne_zero (minpoly.aeval kR β₀)
-  rw [map_aeval_eq_aeval_map (ψ := IsLocalRing.residue S)
-    (φ := IsLocalRing.residue R) rfl, ← derivative_map, minpoly_map_residue hadj]
-  exact hderiv_ne_zero
-
-end IsLocalRing
-
-end

From 2aeb732f49f8be5bbbfb92ffe3fa0b27044db409 Mon Sep 17 00:00:00 2001
From: Grant Yang <rotartsi0482@gmail.com>
Date: Mon, 9 Mar 2026 17:23:43 -0700
Subject: [PATCH 06/11] oops fix natDegree_le'

---
 Mathlib/RingTheory/IsAdjoinRoot.lean | 14 +-------------
 1 file changed, 1 insertion(+), 13 deletions(-)

diff --git a/Mathlib/RingTheory/IsAdjoinRoot.lean b/Mathlib/RingTheory/IsAdjoinRoot.lean
index ed0176931471ab..703e4b0a5f1c1d 100644
--- a/Mathlib/RingTheory/IsAdjoinRoot.lean
+++ b/Mathlib/RingTheory/IsAdjoinRoot.lean
@@ -651,18 +651,6 @@ section mkOfAdjoinEqTop'
 
 variable [Module.Finite R S] [Module.Free R S] [Nontrivial R]
 
--- theorem could be placed here with 0 imports, but
--- it does not logically make sense.
-theorem alternate_natDegree_le' :
-    (minpoly A x).natDegree ≤ Module.finrank A B := by
-  have b := Module.Free.chooseBasis A B
-  let M := LinearMap.toMatrixAlgEquiv b (Algebra.lmul A B x)
-  refine (natDegree_le_natDegree (minpoly.min A x M.charpoly_monic ?_)).trans
-    (M.charpoly_natDegree_eq_dim.trans (Module.finrank_eq_card_chooseBasisIndex A B).symm).le
-  let h := Matrix.aeval_self_charpoly M
-  rwa [aeval_algHom_apply, _root_.map_eq_zero_iff _ (LinearMap.toMatrixAlgEquiv b).injective,
-    aeval_algHom_apply, _root_.map_eq_zero_iff _ Algebra.lmul_injective] at h
-
 /-- If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`. -/
 def mkOfAdjoinEqTop'
     {α : S} (hα : Algebra.adjoin R {α} = ⊤) :
@@ -677,7 +665,7 @@ def mkOfAdjoinEqTop'
     rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at hα
     exact fun s =>
       let ⟨p, hp⟩ := hα s; ⟨AdjoinRoot.mk f p, by simp [φ, ← aeval_def, hp]⟩
-  have hrank : f.natDegree = Module.finrank R S := le_antisymm (minpoly.natDegree_le' α) (by
+  have hrank : f.natDegree = Module.finrank R S := le_antisymm (minpoly.natDegree_le') (by
     have e := φ.toLinearMap.quotKerEquivRange.trans
       (LinearEquiv.ofTop _ (LinearMap.range_eq_top.mpr hφ_surj))
     rw [← e.finrank_eq]

From 428c8c4ad50bc188e51cb409eb88b3759c114548 Mon Sep 17 00:00:00 2001
From: Grant Yang <rotartsi0482@gmail.com>
Date: Tue, 17 Mar 2026 23:32:53 -0700
Subject: [PATCH 07/11] golf away simp lemma

---
 Mathlib/RingTheory/IsAdjoinRoot.lean | 64 ++++++++++++----------------
 1 file changed, 27 insertions(+), 37 deletions(-)

diff --git a/Mathlib/RingTheory/IsAdjoinRoot.lean b/Mathlib/RingTheory/IsAdjoinRoot.lean
index 703e4b0a5f1c1d..ead4e2df0afedf 100644
--- a/Mathlib/RingTheory/IsAdjoinRoot.lean
+++ b/Mathlib/RingTheory/IsAdjoinRoot.lean
@@ -647,46 +647,36 @@ theorem minpoly_eq [IsDomain R] [IsDomain S] [IsTorsionFree R S] [IsIntegrallyCl
             (hirr.isUnit_or_isUnit hq).resolve_left <| minpoly.not_isUnit R h.root
       rw [mul_one]
 
-section mkOfAdjoinEqTop'
-
-variable [Module.Finite R S] [Module.Free R S] [Nontrivial R]
-
 /-- If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`. -/
 def mkOfAdjoinEqTop'
+    [Module.Finite R S] [Module.Free R S] [Nontrivial R]
     {α : S} (hα : Algebra.adjoin R {α} = ⊤) :
-    IsAdjoinRootMonic S (minpoly R α) := by
-  set f := minpoly R α
-  have hf : f.Monic := minpoly.monic (Algebra.IsIntegral.isIntegral α)
-  letI : Module R (AdjoinRoot f) := Algebra.toModule
-  haveI := hf.free_adjoinRoot; haveI finite := hf.finite_adjoinRoot
-  let φ : AdjoinRoot f →ₐ[R] S :=
-    AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α (minpoly.aeval R α)
-  have hφ_surj : Function.Surjective φ := by
-    rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at hα
-    exact fun s =>
-      let ⟨p, hp⟩ := hα s; ⟨AdjoinRoot.mk f p, by simp [φ, ← aeval_def, hp]⟩
-  have hrank : f.natDegree = Module.finrank R S := le_antisymm (minpoly.natDegree_le') (by
-    have e := φ.toLinearMap.quotKerEquivRange.trans
-      (LinearEquiv.ofTop _ (LinearMap.range_eq_top.mpr hφ_surj))
-    rw [← e.finrank_eq]
-    exact (Submodule.finrank_quotient_le _).trans (finrank_quotient_span_eq_natDegree' hf).le)
-  have e := LinearEquiv.ofFinrankEq (R := R) (AdjoinRoot f) S
-    ((finrank_quotient_span_eq_natDegree' hf).trans hrank)
-  have hφ_inj : Function.Injective φ :=
-    fun x y h => OrzechProperty.injective_of_surjective_endomorphism
-    (e.symm.toLinearMap.comp φ.toLinearMap) (e.symm.surjective.comp hφ_surj) (congr_arg e.symm h)
-  exact
-    { IsAdjoinRoot.ofAdjoinRootEquiv
-        (AlgEquiv.ofBijective φ ⟨hφ_inj, hφ_surj⟩) with monic := hf }
-
-@[simp]
-lemma mkOfAdjoinEqTop'_map
-    {α : S} {hα : Algebra.adjoin R {α} = ⊤} :
-    (IsAdjoinRootMonic.mkOfAdjoinEqTop' hα).map = (aeval α) := by
-  unfold IsAdjoinRootMonic.mkOfAdjoinEqTop'
-  ext; simp
-
-end mkOfAdjoinEqTop'
+    IsAdjoinRootMonic S (minpoly R α) where
+  map := aeval α
+  ker_map := by
+    set f := minpoly R α
+    have hf := minpoly.monic (Algebra.IsIntegral.isIntegral (R := R) α)
+    let φ : AdjoinRoot f →ₐ[R] S :=
+      AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α (minpoly.aeval R α)
+    have hφ : Function.Surjective φ := by
+      rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at hα
+      intro s; obtain ⟨p, hp⟩ := hα s
+      exact ⟨AdjoinRoot.mk f p, by simp [φ, ← aeval_def, hp]⟩
+    refine IsAdjoinRoot.ofAdjoinRootEquiv (AlgEquiv.ofBijective φ ⟨?_, hφ⟩) |>.ker_map
+    haveI := hf.free_adjoinRoot; haveI := hf.finite_adjoinRoot
+    letI : Module R (AdjoinRoot f) := Algebra.toModule
+    have e := LinearEquiv.ofFinrankEq (R := R) (AdjoinRoot f) S
+      ((finrank_quotient_span_eq_natDegree' hf).trans <|
+        le_antisymm minpoly.natDegree_le' ?_)
+    · exact fun x y h => OrzechProperty.injective_of_surjective_endomorphism
+        (e.symm.toLinearMap.comp φ.toLinearMap)
+        (e.symm.surjective.comp hφ) (congr_arg e.symm h)
+    · rw [← φ.toLinearMap.quotKerEquivRange.trans
+        (LinearEquiv.ofTop _ (LinearMap.range_eq_top.mpr hφ)) |>.finrank_eq]
+      exact (Submodule.finrank_quotient_le _).trans (finrank_quotient_span_eq_natDegree' hf).le
+  map_surjective := by
+    rwa [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at *
+  monic := minpoly.monic (Algebra.IsIntegral.isIntegral α)
 
 end IsAdjoinRootMonic
 

From 4431b475f0612a311851db64334490718db92753 Mon Sep 17 00:00:00 2001
From: bryanboehnke <bryanboehnke@gmail.com>
Date: Tue, 31 Mar 2026 23:27:45 -0700
Subject: [PATCH 08/11] add Etale.lean

---
 Mathlib.lean                            |   1 +
 Mathlib/RingTheory/LocalRing/Etale.lean | 167 ++++++++++++++++++++++++
 2 files changed, 168 insertions(+)
 create mode 100644 Mathlib/RingTheory/LocalRing/Etale.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 41fcf3dd929beb..56ed56e8a7dcf3 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -6466,6 +6466,7 @@ public import Mathlib.RingTheory.LocalProperties.Semilocal
 public import Mathlib.RingTheory.LocalProperties.Submodule
 public import Mathlib.RingTheory.LocalRing.Basic
 public import Mathlib.RingTheory.LocalRing.Defs
+public import Mathlib.RingTheory.LocalRing.Etale
 public import Mathlib.RingTheory.LocalRing.LocalSubring
 public import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
 public import Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs
diff --git a/Mathlib/RingTheory/LocalRing/Etale.lean b/Mathlib/RingTheory/LocalRing/Etale.lean
new file mode 100644
index 00000000000000..121575bb0f47ad
--- /dev/null
+++ b/Mathlib/RingTheory/LocalRing/Etale.lean
@@ -0,0 +1,167 @@
+/-
+Copyright (c) 2026 University of Washington Math AI Lab. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bianca Viray, Bryan Boehnke, Grant Yang, George Peykanu, Tianshuo Wang
+-/
+
+module
+
+public import Mathlib.RingTheory.Unramified.LocalRing
+public import Mathlib.RingTheory.Smooth.Flat
+public import Mathlib.RingTheory.LocalRing.Module
+public import Mathlib.RingTheory.LocalRing.Quotient
+public import Mathlib.RingTheory.IsAdjoinRoot
+
+/-!
+# É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](https://arxiv.org/abs/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_of_adjoin_eq_top`: if `β` generates `S` over `R`, then
+  `β 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](https://arxiv.org/abs/2503.07846) (formalized at [uw-math-ai/monogenic-extensions](https://github.com/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
+-/
+
+@[expose] public section
+
+namespace IsLocalRing
+
+variable {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
+    [IsLocalRing S] [IsLocalRing R] [Module.Finite R S] [FaithfulSMul R S]
+
+open Polynomial
+
+open Algebra in
+/-- A finite étale extension of local rings is generated by a single element.
+This is Lemma 3.2, part 1 of [arXiv:2503.07846](https://arxiv.org/abs/2503.07846).
+The proof lifts a primitive element of the residue field extension via Nakayama's lemma. -/
+theorem exists_adjoin_eq_top [Algebra.Etale R S] :
+    ∃ β : S, adjoin R {β} = ⊤ := by
+  obtain ⟨β₀, hβ₀⟩ := @Field.exists_primitive_element
+    (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)
+    _ _ _ IsLocalRing.ResidueField.finite_of_module_finite
+    instIsSeparableResidueFieldOfFormallyUnramified
+  obtain ⟨β, hβ⟩ := Ideal.Quotient.mk_surjective β₀
+  refine ⟨β, eq_top_iff.mpr (Submodule.le_of_le_smul_of_le_jacobson_bot
+    (Module.finite_def.mp inferInstance) (IsLocalRing.maximalIdeal_le_jacobson ⊥)
+    (?_ : ⊤ ≤ (adjoin R {β}).toSubmodule ⊔ IsLocalRing.maximalIdeal R • ⊤))⟩
+  intro s _
+  have h_adjoin_top : adjoin (IsLocalRing.ResidueField R) {β₀} = ⊤ := by
+    rw [← IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic
+      (IsAlgebraic.isAlgebraic β₀), hβ₀, IntermediateField.top_toSubalgebra]
+  rw [show β₀ = IsLocalRing.residue S β from hβ.symm,
+    adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at h_adjoin_top
+  obtain ⟨p, hp⟩ := h_adjoin_top (IsLocalRing.residue S s)
+  obtain ⟨q, rfl⟩ := Polynomial.map_surjective _ IsLocalRing.residue_surjective p
+  rw [Ideal.smul_top_eq_map]
+  refine Submodule.mem_sup.mpr ⟨aeval β q, ?_, s - aeval β q, ?_, by ring⟩
+  · rw [adjoin_singleton_eq_range_aeval]; exact ⟨q, rfl⟩
+  · exact (FormallyUnramified.map_maximalIdeal (R := R) (S := S)) ▸
+      Ideal.Quotient.eq.mp (show
+        IsLocalRing.residue S s = IsLocalRing.residue S (aeval β q) from by
+        rw [map_aeval_eq_aeval_map
+          (ψ := IsLocalRing.residue S) (φ := IsLocalRing.residue R) rfl, hp])
+
+
+/-- When `β` generates `S` over `R`, the residue `β₀ = β mod m_S`
+generates `S/m_S` over `R/m_R`. -/
+lemma adjoin_residue_eq_top_of_adjoin_eq_top
+    {β : S} (hβ_gen : Algebra.adjoin R {β} = ⊤) :
+    Algebra.adjoin (IsLocalRing.ResidueField R) {IsLocalRing.residue S β} = ⊤ := by
+  rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at *
+  intro x
+  obtain ⟨s, rfl⟩ := IsLocalRing.residue_surjective (R := S) x
+  obtain ⟨p, rfl⟩ := hβ_gen s
+  exact ⟨p.map (IsLocalRing.residue R),
+    (map_aeval_eq_aeval_map (ψ := IsLocalRing.residue S)
+      (φ := IsLocalRing.residue R) rfl p β).symm⟩
+
+
+/-- For finite étale extensions of local rings,
+`finrank R S = finrank (ResidueField R) (ResidueField S)`. -/
+lemma finrank_eq_finrank_residueField [Algebra.Etale R S] :
+    Module.finrank R S =
+      Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S) := by
+  haveI : Module.Free R S := Module.free_of_flat_of_isLocalRing
+  have e := AddEquiv.toLinearEquiv (R := R ⧸ IsLocalRing.maximalIdeal R)
+    (Ideal.quotEquivOfEq <|
+      Algebra.FormallyUnramified.map_maximalIdeal (R := R) (S := S)).toAddEquiv ?_
+  · erw [← e.finrank_eq, IsLocalRing.finrank_quotient_map (R := R) (S := S)]
+  · intro r x
+    obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective r
+    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
+    simp only [RingEquiv.toAddEquiv_eq_coe]; rfl
+
+
+-- /-- 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. -/
+-- lemma minpoly_map_residue [Algebra.Etale R S]
+--     {β : S} (hadj : Algebra.adjoin R {β} = ⊤) :
+--     (minpoly R β).map (IsLocalRing.residue R) = minpoly (IsLocalRing.ResidueField R)
+--       (IsLocalRing.residue S β) := by
+--   have hmonic := minpoly.monic <| Algebra.IsIntegral.isIntegral (R:=R) β
+--   set kR := IsLocalRing.ResidueField R
+--   set β₀ := IsLocalRing.residue S β
+--   -- Both monic, same degree, divisibility ⟹ equal
+--   refine eq_of_monic_of_dvd_of_natDegree_le (minpoly.monic <| Algebra.IsIntegral.isIntegral β₀)
+--     (hmonic.map _) (minpoly.dvd kR β₀ ?_) ?_
+--   · rw [← map_aeval_eq_aeval_map (ψ := IsLocalRing.residue S)
+--       (φ := IsLocalRing.residue R) rfl, minpoly.aeval, map_zero]
+--   · suffices ((minpoly R β).map (IsLocalRing.residue R)).natDegree
+--       = (minpoly kR β₀).natDegree from this.le
+--     haveI : Module.Free R S := Module.free_of_flat_of_isLocalRing
+--     erw [hmonic.natDegree_map _,
+--       ← (IsAdjoinRootMonic.mkOfAdjoinEqTop' hadj).finrank,
+--       finrank_eq_finrank_residueField,
+--       ← IntermediateField.finrank_top']
+--     rw [← show IntermediateField.adjoin kR {β₀} = ⊤ by
+--       have hβ₀_gen : Algebra.adjoin kR {β₀} = ⊤ := adjoin_residue_eq_top_of_adjoin_eq_top hadj
+--       rw [← IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic
+--         (Algebra.IsAlgebraic.isAlgebraic β₀)] at hβ₀_gen
+--       exact IntermediateField.toSubalgebra_injective hβ₀_gen]
+--     rw [IntermediateField.adjoin.finrank <| Algebra.IsIntegral.isIntegral β₀]
+
+-- /-- 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`. -/
+-- lemma isUnit_aeval_derivative_minpoly_of_adjoin_eq_top
+--     [Algebra.Etale R S] {β : S}
+--     (hadj : Algebra.adjoin R {β} = ⊤) :
+--     IsUnit (aeval β (minpoly R β).derivative) := by
+--   -- alternative:
+--   -- suffices h : IsLocalRing.residue S (aeval β (minpoly R β).derivative) ≠ 0 from
+--   --   (IsLocalRing.residue_ne_zero_iff_isUnit _).mp h
+--   apply fun s => (IsLocalRing.residue_ne_zero_iff_isUnit s).mp
+--   rw [map_aeval_eq_aeval_map (ψ := IsLocalRing.residue S)
+--     (φ := IsLocalRing.residue R) rfl, ← derivative_map, minpoly_map_residue hadj]
+--   exact (Algebra.IsSeparable.isSeparable _ _).aeval_derivative_ne_zero (minpoly.aeval _ _)
+
+end IsLocalRing

From 05e0de146f1e407d58e3691efae22a5351770be4 Mon Sep 17 00:00:00 2001
From: Grant Yang <rotartsi0482@gmail.com>
Date: Wed, 1 Apr 2026 11:02:46 -0700
Subject: [PATCH 09/11] uncomment results depending mkOfAdjoinEqTop'

---
 Mathlib/RingTheory/LocalRing/Etale.lean | 84 ++++++++++++-------------
 1 file changed, 39 insertions(+), 45 deletions(-)

diff --git a/Mathlib/RingTheory/LocalRing/Etale.lean b/Mathlib/RingTheory/LocalRing/Etale.lean
index 121575bb0f47ad..57cafacfcfa2c8 100644
--- a/Mathlib/RingTheory/LocalRing/Etale.lean
+++ b/Mathlib/RingTheory/LocalRing/Etale.lean
@@ -90,7 +90,6 @@ theorem exists_adjoin_eq_top [Algebra.Etale R S] :
         rw [map_aeval_eq_aeval_map
           (ψ := IsLocalRing.residue S) (φ := IsLocalRing.residue R) rfl, hp])
 
-
 /-- When `β` generates `S` over `R`, the residue `β₀ = β mod m_S`
 generates `S/m_S` over `R/m_R`. -/
 lemma adjoin_residue_eq_top_of_adjoin_eq_top
@@ -104,7 +103,6 @@ lemma adjoin_residue_eq_top_of_adjoin_eq_top
     (map_aeval_eq_aeval_map (ψ := IsLocalRing.residue S)
       (φ := IsLocalRing.residue R) rfl p β).symm⟩
 
-
 /-- For finite étale extensions of local rings,
 `finrank R S = finrank (ResidueField R) (ResidueField S)`. -/
 lemma finrank_eq_finrank_residueField [Algebra.Etale R S] :
@@ -120,48 +118,44 @@ lemma finrank_eq_finrank_residueField [Algebra.Etale R S] :
     obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
     simp only [RingEquiv.toAddEquiv_eq_coe]; rfl
 
-
--- /-- 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. -/
--- lemma minpoly_map_residue [Algebra.Etale R S]
---     {β : S} (hadj : Algebra.adjoin R {β} = ⊤) :
---     (minpoly R β).map (IsLocalRing.residue R) = minpoly (IsLocalRing.ResidueField R)
---       (IsLocalRing.residue S β) := by
---   have hmonic := minpoly.monic <| Algebra.IsIntegral.isIntegral (R:=R) β
---   set kR := IsLocalRing.ResidueField R
---   set β₀ := IsLocalRing.residue S β
---   -- Both monic, same degree, divisibility ⟹ equal
---   refine eq_of_monic_of_dvd_of_natDegree_le (minpoly.monic <| Algebra.IsIntegral.isIntegral β₀)
---     (hmonic.map _) (minpoly.dvd kR β₀ ?_) ?_
---   · rw [← map_aeval_eq_aeval_map (ψ := IsLocalRing.residue S)
---       (φ := IsLocalRing.residue R) rfl, minpoly.aeval, map_zero]
---   · suffices ((minpoly R β).map (IsLocalRing.residue R)).natDegree
---       = (minpoly kR β₀).natDegree from this.le
---     haveI : Module.Free R S := Module.free_of_flat_of_isLocalRing
---     erw [hmonic.natDegree_map _,
---       ← (IsAdjoinRootMonic.mkOfAdjoinEqTop' hadj).finrank,
---       finrank_eq_finrank_residueField,
---       ← IntermediateField.finrank_top']
---     rw [← show IntermediateField.adjoin kR {β₀} = ⊤ by
---       have hβ₀_gen : Algebra.adjoin kR {β₀} = ⊤ := adjoin_residue_eq_top_of_adjoin_eq_top hadj
---       rw [← IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic
---         (Algebra.IsAlgebraic.isAlgebraic β₀)] at hβ₀_gen
---       exact IntermediateField.toSubalgebra_injective hβ₀_gen]
---     rw [IntermediateField.adjoin.finrank <| Algebra.IsIntegral.isIntegral β₀]
-
--- /-- 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`. -/
--- lemma isUnit_aeval_derivative_minpoly_of_adjoin_eq_top
---     [Algebra.Etale R S] {β : S}
---     (hadj : Algebra.adjoin R {β} = ⊤) :
---     IsUnit (aeval β (minpoly R β).derivative) := by
---   -- alternative:
---   -- suffices h : IsLocalRing.residue S (aeval β (minpoly R β).derivative) ≠ 0 from
---   --   (IsLocalRing.residue_ne_zero_iff_isUnit _).mp h
---   apply fun s => (IsLocalRing.residue_ne_zero_iff_isUnit s).mp
---   rw [map_aeval_eq_aeval_map (ψ := IsLocalRing.residue S)
---     (φ := IsLocalRing.residue R) rfl, ← derivative_map, minpoly_map_residue hadj]
---   exact (Algebra.IsSeparable.isSeparable _ _).aeval_derivative_ne_zero (minpoly.aeval _ _)
+/-- 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. -/
+lemma minpoly_map_residue [Algebra.Etale R S]
+    {β : S} (hadj : Algebra.adjoin R {β} = ⊤) :
+    (minpoly R β).map (IsLocalRing.residue R) = minpoly (IsLocalRing.ResidueField R)
+      (IsLocalRing.residue S β) := by
+  have hmonic := minpoly.monic <| Algebra.IsIntegral.isIntegral (R:=R) β
+  set kR := IsLocalRing.ResidueField R
+  set β₀ := IsLocalRing.residue S β
+  -- Both monic, same degree, divisibility ⟹ equal
+  refine eq_of_monic_of_dvd_of_natDegree_le (minpoly.monic <| Algebra.IsIntegral.isIntegral β₀)
+    (hmonic.map _) (minpoly.dvd kR β₀ ?_) ?_
+  · rw [← map_aeval_eq_aeval_map (ψ := IsLocalRing.residue S)
+      (φ := IsLocalRing.residue R) rfl, minpoly.aeval, map_zero]
+  · suffices ((minpoly R β).map (IsLocalRing.residue R)).natDegree
+      = (minpoly kR β₀).natDegree from this.le
+    haveI : Module.Free R S := Module.free_of_flat_of_isLocalRing
+    erw [hmonic.natDegree_map _,
+      ← (IsAdjoinRootMonic.mkOfAdjoinEqTop' hadj).finrank,
+      finrank_eq_finrank_residueField,
+      ← IntermediateField.finrank_top']
+    rw [← show IntermediateField.adjoin kR {β₀} = ⊤ by
+      have hβ₀_gen : Algebra.adjoin kR {β₀} = ⊤ := adjoin_residue_eq_top_of_adjoin_eq_top hadj
+      rw [← IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic
+        (Algebra.IsAlgebraic.isAlgebraic β₀)] at hβ₀_gen
+      exact IntermediateField.toSubalgebra_injective hβ₀_gen]
+    rw [IntermediateField.adjoin.finrank <| Algebra.IsIntegral.isIntegral β₀]
+
+/-- 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`. -/
+lemma isUnit_aeval_derivative_minpoly_of_adjoin_eq_top
+    [Algebra.Etale R S] {β : S}
+    (hadj : Algebra.adjoin R {β} = ⊤) :
+    IsUnit (aeval β (minpoly R β).derivative) := by
+  apply fun s => (IsLocalRing.residue_ne_zero_iff_isUnit s).mp
+  rw [map_aeval_eq_aeval_map (ψ := IsLocalRing.residue S)
+    (φ := IsLocalRing.residue R) rfl, ← derivative_map, minpoly_map_residue hadj]
+  exact (Algebra.IsSeparable.isSeparable _ _).aeval_derivative_ne_zero (minpoly.aeval _ _)
 
 end IsLocalRing

From 3e196f09e81d1bcd47052c305fc1fa4d60cf5e61 Mon Sep 17 00:00:00 2001
From: Grant Yang <rotartsi0482@gmail.com>
Date: Fri, 17 Apr 2026 11:53:11 -0700
Subject: [PATCH 10/11] minor fixes

---
 Mathlib/RingTheory/LocalRing/Etale.lean | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/Mathlib/RingTheory/LocalRing/Etale.lean b/Mathlib/RingTheory/LocalRing/Etale.lean
index 57cafacfcfa2c8..8ed47d5f1b157b 100644
--- a/Mathlib/RingTheory/LocalRing/Etale.lean
+++ b/Mathlib/RingTheory/LocalRing/Etale.lean
@@ -65,10 +65,8 @@ This is Lemma 3.2, part 1 of [arXiv:2503.07846](https://arxiv.org/abs/2503.07846
 The proof lifts a primitive element of the residue field extension via Nakayama's lemma. -/
 theorem exists_adjoin_eq_top [Algebra.Etale R S] :
     ∃ β : S, adjoin R {β} = ⊤ := by
-  obtain ⟨β₀, hβ₀⟩ := @Field.exists_primitive_element
+  obtain ⟨β₀, hβ₀⟩ := Field.exists_primitive_element
     (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)
-    _ _ _ IsLocalRing.ResidueField.finite_of_module_finite
-    instIsSeparableResidueFieldOfFormallyUnramified
   obtain ⟨β, hβ⟩ := Ideal.Quotient.mk_surjective β₀
   refine ⟨β, eq_top_iff.mpr (Submodule.le_of_le_smul_of_le_jacobson_bot
     (Module.finite_def.mp inferInstance) (IsLocalRing.maximalIdeal_le_jacobson ⊥)
@@ -135,7 +133,7 @@ lemma minpoly_map_residue [Algebra.Etale R S]
   · suffices ((minpoly R β).map (IsLocalRing.residue R)).natDegree
       = (minpoly kR β₀).natDegree from this.le
     haveI : Module.Free R S := Module.free_of_flat_of_isLocalRing
-    erw [hmonic.natDegree_map _,
+    rw [hmonic.natDegree_map _,
       ← (IsAdjoinRootMonic.mkOfAdjoinEqTop' hadj).finrank,
       finrank_eq_finrank_residueField,
       ← IntermediateField.finrank_top']

From a08730a1b77266e3473e3e9da4e4d79cf8b73096 Mon Sep 17 00:00:00 2001
From: Grant Yang <rotartsi0482@gmail.com>
Date: Sun, 19 Apr 2026 17:07:16 -0700
Subject: [PATCH 11/11] open IsLocalRing + iff result

---
 Mathlib/RingTheory/LocalRing/Etale.lean | 132 +++++++++++-------------
 1 file changed, 60 insertions(+), 72 deletions(-)

diff --git a/Mathlib/RingTheory/LocalRing/Etale.lean b/Mathlib/RingTheory/LocalRing/Etale.lean
index 8ed47d5f1b157b..5790dfac6ef677 100644
--- a/Mathlib/RingTheory/LocalRing/Etale.lean
+++ b/Mathlib/RingTheory/LocalRing/Etale.lean
@@ -6,11 +6,10 @@ Authors: Bianca Viray, Bryan Boehnke, Grant Yang, George Peykanu, Tianshuo Wang
 
 module
 
-public import Mathlib.RingTheory.Unramified.LocalRing
-public import Mathlib.RingTheory.Smooth.Flat
-public import Mathlib.RingTheory.LocalRing.Module
-public import Mathlib.RingTheory.LocalRing.Quotient
 public import Mathlib.RingTheory.IsAdjoinRoot
+public import Mathlib.RingTheory.LocalRing.Quotient
+public import Mathlib.RingTheory.Smooth.Flat
+public import Mathlib.RingTheory.Unramified.LocalRing
 
 /-!
 # Étale extensions of local rings
@@ -28,7 +27,7 @@ These are parts 1 and 2 of Lemma 3.2 of [arXiv:2503.07846](https://arxiv.org/abs
 
 ## Key intermediate results
 
-* `IsLocalRing.adjoin_residue_eq_top_of_adjoin_eq_top`: if `β` generates `S` over `R`, then
+* `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)`.
@@ -57,60 +56,58 @@ namespace IsLocalRing
 variable {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
     [IsLocalRing S] [IsLocalRing R] [Module.Finite R S] [FaithfulSMul R S]
 
-open Polynomial
+open Polynomial IsLocalRing Algebra
+
+/-- When `β` generates `S` over `R`, the residue `β₀ = β mod m_S`
+generates `S/m_S` over `R/m_R`. -/
+lemma adjoin_residue_eq_top_iff_adjoin_eq_top [Algebra.Etale R S] (β : S) :
+    Algebra.adjoin (ResidueField R) {residue S β} = ⊤ ↔ Algebra.adjoin R {β} = ⊤ := by
+  constructor
+  · intro hβ
+    refine eq_top_iff.mpr <| Submodule.le_of_le_smul_of_le_jacobson_bot
+      (Module.finite_def.mp inferInstance) (IsLocalRing.maximalIdeal_le_jacobson ⊥)
+      (?_ : ⊤ ≤ (adjoin R {β}).toSubmodule ⊔ maximalIdeal R • ⊤)
+    intro s _
+    rw [adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at hβ
+    obtain ⟨p, hp⟩ := hβ (residue S s)
+    obtain ⟨q, rfl⟩ := Polynomial.map_surjective _ residue_surjective p
+    rw [Ideal.smul_top_eq_map]
+    refine Submodule.mem_sup.mpr ⟨aeval β q, ?_, s - aeval β q, ?_, by ring⟩
+    · rw [adjoin_singleton_eq_range_aeval]; exact ⟨q, rfl⟩
+    · rw [Algebra.FormallyUnramified.map_maximalIdeal]
+      erw [← Ideal.Quotient.eq,
+        map_aeval_eq_aeval_map (ψ := residue S) (φ := residue R) rfl, hp]
+      rfl
+  · intro hβ_gen
+    rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at *
+    intro x
+    obtain ⟨s, rfl⟩ := IsLocalRing.residue_surjective (R := S) x
+    obtain ⟨p, rfl⟩ := hβ_gen s
+    exact ⟨p.map (residue R), by
+      rw [← map_aeval_eq_aeval_map (ψ := residue S) (φ := residue R) rfl p β]⟩
 
-open Algebra in
 /-- A finite étale extension of local rings is generated by a single element.
 This is Lemma 3.2, part 1 of [arXiv:2503.07846](https://arxiv.org/abs/2503.07846).
 The proof lifts a primitive element of the residue field extension via Nakayama's lemma. -/
 theorem exists_adjoin_eq_top [Algebra.Etale R S] :
-    ∃ β : S, adjoin R {β} = ⊤ := by
-  obtain ⟨β₀, hβ₀⟩ := Field.exists_primitive_element
-    (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)
-  obtain ⟨β, hβ⟩ := Ideal.Quotient.mk_surjective β₀
-  refine ⟨β, eq_top_iff.mpr (Submodule.le_of_le_smul_of_le_jacobson_bot
-    (Module.finite_def.mp inferInstance) (IsLocalRing.maximalIdeal_le_jacobson ⊥)
-    (?_ : ⊤ ≤ (adjoin R {β}).toSubmodule ⊔ IsLocalRing.maximalIdeal R • ⊤))⟩
-  intro s _
-  have h_adjoin_top : adjoin (IsLocalRing.ResidueField R) {β₀} = ⊤ := by
-    rw [← IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic
-      (IsAlgebraic.isAlgebraic β₀), hβ₀, IntermediateField.top_toSubalgebra]
-  rw [show β₀ = IsLocalRing.residue S β from hβ.symm,
-    adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at h_adjoin_top
-  obtain ⟨p, hp⟩ := h_adjoin_top (IsLocalRing.residue S s)
-  obtain ⟨q, rfl⟩ := Polynomial.map_surjective _ IsLocalRing.residue_surjective p
-  rw [Ideal.smul_top_eq_map]
-  refine Submodule.mem_sup.mpr ⟨aeval β q, ?_, s - aeval β q, ?_, by ring⟩
-  · rw [adjoin_singleton_eq_range_aeval]; exact ⟨q, rfl⟩
-  · exact (FormallyUnramified.map_maximalIdeal (R := R) (S := S)) ▸
-      Ideal.Quotient.eq.mp (show
-        IsLocalRing.residue S s = IsLocalRing.residue S (aeval β q) from by
-        rw [map_aeval_eq_aeval_map
-          (ψ := IsLocalRing.residue S) (φ := IsLocalRing.residue R) rfl, hp])
-
-/-- When `β` generates `S` over `R`, the residue `β₀ = β mod m_S`
-generates `S/m_S` over `R/m_R`. -/
-lemma adjoin_residue_eq_top_of_adjoin_eq_top
-    {β : S} (hβ_gen : Algebra.adjoin R {β} = ⊤) :
-    Algebra.adjoin (IsLocalRing.ResidueField R) {IsLocalRing.residue S β} = ⊤ := by
-  rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at *
-  intro x
-  obtain ⟨s, rfl⟩ := IsLocalRing.residue_surjective (R := S) x
-  obtain ⟨p, rfl⟩ := hβ_gen s
-  exact ⟨p.map (IsLocalRing.residue R),
-    (map_aeval_eq_aeval_map (ψ := IsLocalRing.residue S)
-      (φ := IsLocalRing.residue R) rfl p β).symm⟩
+    ∃ β : S, Algebra.adjoin R {β} = ⊤ := by
+  obtain ⟨β₀, hβ₀⟩ := Field.exists_primitive_element (ResidueField R) (ResidueField S)
+  obtain ⟨β, hβ⟩ := residue_surjective (R := S) β₀
+  refine ⟨β, adjoin_residue_eq_top_iff_adjoin_eq_top β |>.mp ?_⟩
+  rw [hβ,
+    ← IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic (IsAlgebraic.of_finite _ _),
+    hβ₀, IntermediateField.top_toSubalgebra]
 
 /-- For finite étale extensions of local rings,
 `finrank R S = finrank (ResidueField R) (ResidueField S)`. -/
 lemma finrank_eq_finrank_residueField [Algebra.Etale R S] :
     Module.finrank R S =
-      Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S) := by
+      Module.finrank (ResidueField R) (ResidueField S) := by
   haveI : Module.Free R S := Module.free_of_flat_of_isLocalRing
-  have e := AddEquiv.toLinearEquiv (R := R ⧸ IsLocalRing.maximalIdeal R)
-    (Ideal.quotEquivOfEq <|
-      Algebra.FormallyUnramified.map_maximalIdeal (R := R) (S := S)).toAddEquiv ?_
-  · erw [← e.finrank_eq, IsLocalRing.finrank_quotient_map (R := R) (S := S)]
+  have e := AddEquiv.toLinearEquiv (R := R ⧸ maximalIdeal R) (Ideal.quotEquivOfEq <|
+      Algebra.FormallyUnramified.map_maximalIdeal (R := R) (S := S)).toAddEquiv
+    ?_
+  · erw [← e.finrank_eq, finrank_quotient_map (R := R) (S := S)]
   · intro r x
     obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective r
     obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
@@ -120,29 +117,20 @@ lemma finrank_eq_finrank_residueField [Algebra.Etale R S] :
 maps to the minimal polynomial of `β mod m_S` over the residue field. -/
 lemma minpoly_map_residue [Algebra.Etale R S]
     {β : S} (hadj : Algebra.adjoin R {β} = ⊤) :
-    (minpoly R β).map (IsLocalRing.residue R) = minpoly (IsLocalRing.ResidueField R)
-      (IsLocalRing.residue S β) := by
-  have hmonic := minpoly.monic <| Algebra.IsIntegral.isIntegral (R:=R) β
-  set kR := IsLocalRing.ResidueField R
-  set β₀ := IsLocalRing.residue S β
+    (minpoly R β).map (residue R) = minpoly (ResidueField R) (residue S β) := by
+  have h := minpoly.monic <| Algebra.IsIntegral.isIntegral (R:=R) β
   -- Both monic, same degree, divisibility ⟹ equal
-  refine eq_of_monic_of_dvd_of_natDegree_le (minpoly.monic <| Algebra.IsIntegral.isIntegral β₀)
-    (hmonic.map _) (minpoly.dvd kR β₀ ?_) ?_
-  · rw [← map_aeval_eq_aeval_map (ψ := IsLocalRing.residue S)
-      (φ := IsLocalRing.residue R) rfl, minpoly.aeval, map_zero]
-  · suffices ((minpoly R β).map (IsLocalRing.residue R)).natDegree
-      = (minpoly kR β₀).natDegree from this.le
-    haveI : Module.Free R S := Module.free_of_flat_of_isLocalRing
-    rw [hmonic.natDegree_map _,
+  refine eq_of_monic_of_dvd_of_natDegree_le
+    (minpoly.monic <| Algebra.IsIntegral.isIntegral <| residue S β)
+    (h.map _) (minpoly.dvd (ResidueField R) (residue S β) ?_) ?_
+  · rw [← map_aeval_eq_aeval_map (ψ := residue S) (φ := residue R) rfl]
+    simp
+  · haveI : Module.Free R S := Module.free_of_flat_of_isLocalRing
+    have hβ₀ := (adjoin_residue_eq_top_iff_adjoin_eq_top β).mpr hadj
+    rw [h.natDegree_map _,
       ← (IsAdjoinRootMonic.mkOfAdjoinEqTop' hadj).finrank,
       finrank_eq_finrank_residueField,
-      ← IntermediateField.finrank_top']
-    rw [← show IntermediateField.adjoin kR {β₀} = ⊤ by
-      have hβ₀_gen : Algebra.adjoin kR {β₀} = ⊤ := adjoin_residue_eq_top_of_adjoin_eq_top hadj
-      rw [← IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic
-        (Algebra.IsAlgebraic.isAlgebraic β₀)] at hβ₀_gen
-      exact IntermediateField.toSubalgebra_injective hβ₀_gen]
-    rw [IntermediateField.adjoin.finrank <| Algebra.IsIntegral.isIntegral β₀]
+      (IsAdjoinRootMonic.mkOfAdjoinEqTop' hβ₀).finrank]
 
 /-- 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
@@ -151,9 +139,9 @@ lemma isUnit_aeval_derivative_minpoly_of_adjoin_eq_top
     [Algebra.Etale R S] {β : S}
     (hadj : Algebra.adjoin R {β} = ⊤) :
     IsUnit (aeval β (minpoly R β).derivative) := by
-  apply fun s => (IsLocalRing.residue_ne_zero_iff_isUnit s).mp
-  rw [map_aeval_eq_aeval_map (ψ := IsLocalRing.residue S)
-    (φ := IsLocalRing.residue R) rfl, ← derivative_map, minpoly_map_residue hadj]
-  exact (Algebra.IsSeparable.isSeparable _ _).aeval_derivative_ne_zero (minpoly.aeval _ _)
+  apply fun s => (residue_ne_zero_iff_isUnit s).mp
+  rw [map_aeval_eq_aeval_map (ψ := residue S) (φ := residue R) rfl,
+    ← derivative_map, minpoly_map_residue hadj]
+  exact Algebra.IsSeparable.isSeparable _ _ |>.aeval_derivative_ne_zero (minpoly.aeval _ _)
 
 end IsLocalRing