Etale.lean

/-
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.IsAdjoinRoot
public import Mathlib.RingTheory.LocalRing.Quotient
public import Mathlib.RingTheory.Smooth.Flat
public import Mathlib.RingTheory.Unramified.LocalRing

/-!
# É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_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](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 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 β]⟩

/-- 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 (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 (ResidueField R) (ResidueField S) := by
  haveI : Module.Free R S := Module.free_of_flat_of_isLocalRing
  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
    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 (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 <| 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,
      (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
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 => (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