Points of the Kummer cover $y^n=f(x)$ : evaluation homomorphisms and the local coordinate $x-a$

Definition

CurveSymmetry_11_KummerLocal

by carlok · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

commutative-algebracurve-symmetry-leankummer-theory

Let $n\in\mathbb N$ , $f\in\mathbb C[x]$ , and let $R_{n,f}=\mathbb C[x][Y]/(Y^n-f)$ be the coordinate ring of the Kummer cover $y^n=f(x)$ , with $y$ the class of $Y$ .

The file defines two objects. For a point $(a,b)\in\mathbb C^2$ of the curve, that is with $b^n=f(a)$ , the evaluation homomorphism

\mathrm{ev}_{a,b}:R_{n,f}\longrightarrow\mathbb C,\qquad x\longmapsto a,\qquad y\longmapsto b,

whose kernel is a prime ideal; and, for $a\in\mathbb C$ , the element $x-a\in R_{n,f}$ .

The rest of the file establishes, with proofs, the local structure that later parts use:

for $n\ge1$ , $R_{n,f}$ is integral over $\mathbb C[x]$ , and its maximal ideals are exactly the kernels $\ker\mathrm{ev}_{a,b}$ with $b^n=f(a)$ ;
for $n\ge1$ , in a localization of $R_{n,f}$ at $\ker\mathrm{ev}_{a,b}$ the maximal ideal is generated by $x-a$ when $f(a)\ne0$ , and by $y$ when $f(a)=0$ and $f$ is squarefree;
for $n\ge1$ and $f$ squarefree of positive degree, $Y^n-f$ is irreducible over $\mathbb C(x)$ , $R_{n,f}$ is a Noetherian domain, its localizations at the points $(a,b)$ are discrete valuation rings, and $R_{n,f}$ is a Dedekind domain.

These identify the finite places of the Kummer field $\mathbb C(x)[Y]/(Y^n-f)$ and their uniformizers, as needed to compute the genus three of $\operatorname{Re}(z^4)=1$ , that is, of $y^4=2-x^4$ , in Remark 5.

Formalization Note: A point is passed together with a proof of $b^n=f(a)$ ; the condition $n\ne0$ is the instance NeZero n, and the conditions that $f$ is squarefree and has positive degree are Fact instances. The statements about local rings hold for any ring presented as the localization at $\ker\mathrm{ev}_{a,b}$ .

Definition code

-- Definitions, part 11 of 12, generated from curve-symmetry-lean by skeleton
-- subtraction: the source modules below, in dependency order, each in its own
-- section; only definitions, instances and the theorems they need are kept.
import Definitions.Def_CurveSymmetry_01_RealLoci
import Definitions.Def_CurveSymmetry_02_FamilyBasics
import Definitions.Def_CurveSymmetry_03_IsometriesAndCharts
import Definitions.Def_CurveSymmetry_05_FamilyFunctionField
import Definitions.Def_CurveSymmetry_06_QuadraticRing
import Definitions.Def_CurveSymmetry_07_Places
import Definitions.Def_CurveSymmetry_08_Differentials
import Definitions.Def_CurveSymmetry_09_Genus
import Definitions.Def_CurveSymmetry_10_KummerField
import Mathlib.Algebra.MvPolynomial.Nilpotent
import Mathlib.Algebra.MvPolynomial.NoZeroDivisors
import Mathlib.Algebra.MvPolynomial.PDeriv
import Mathlib.Algebra.Polynomial.FieldDivision
import Mathlib.Algebra.Polynomial.Reverse
import Mathlib.Algebra.Polynomial.SpecificDegree
import Mathlib.Analysis.Complex.Isometry
import Mathlib.Analysis.Complex.OperatorNorm
import Mathlib.Analysis.Complex.Polynomial.Basic
import Mathlib.Analysis.Normed.Affine.MazurUlam
import Mathlib.Data.Complex.Basic
import Mathlib.FieldTheory.RatFunc.Basic
import Mathlib.FieldTheory.Separable
import Mathlib.LinearAlgebra.Basis.Basic
import Mathlib.LinearAlgebra.FiniteDimensional.Defs
import Mathlib.LinearAlgebra.TensorProduct.Basis
import Mathlib.RingTheory.AdjoinRoot
import Mathlib.RingTheory.DedekindDomain.Dvr
import Mathlib.RingTheory.DiscreteValuationRing.TFAE
import Mathlib.RingTheory.Etale.Field
import Mathlib.RingTheory.Etale.Kaehler
import Mathlib.RingTheory.Kaehler.Basic
import Mathlib.RingTheory.Kaehler.Polynomial
import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
import Mathlib.RingTheory.LocalRing.Module
import Mathlib.RingTheory.Localization.AsSubring
import Mathlib.RingTheory.MvPolynomial.Homogeneous
import Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
import Mathlib.RingTheory.Nakayama
import Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
import Mathlib.RingTheory.Polynomial.GaussLemma
import Mathlib.RingTheory.RootsOfUnity.Complex
import Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
import Mathlib.RingTheory.Valuation.ValuationSubring
import Mathlib.Tactic

-- lean/KummerLocal.lean
section

namespace CurveSymmetry

set_option autoImplicit false

open Polynomial

/-- In a field containing `ℂ`, an `n`-th root of a constant is a constant. -/
lemma exists_eq_algebraMap_of_pow_eq {L : Type*} [Field L] [Algebra ℂ L] {n : ℕ} (hn : n ≠ 0)
    {t : L} {β : ℂ} (ht : t ^ n = algebraMap ℂ L β) :
    ∃ d : ℂ, d ^ n = β ∧ t = algebraMap ℂ L d := by
  by_cases hβ : β = 0
  · refine ⟨0, by rw [hβ, zero_pow hn], ?_⟩
    rw [hβ, map_zero] at ht
    rw [map_zero]
    exact (pow_eq_zero_iff hn).mp ht
  · obtain ⟨α, hα⟩ := IsAlgClosed.exists_pow_nat_eq β (Nat.pos_of_ne_zero hn)
    have hα0 : α ≠ 0 := by
      rintro rfl
      exact hβ (by rw [← hα, zero_pow hn])
    have hια : algebraMap ℂ L α ≠ 0 := (map_ne_zero_iff _ (algebraMap ℂ L).injective).mpr hα0
    have hιβ : algebraMap ℂ L β ≠ 0 := (map_ne_zero_iff _ (algebraMap ℂ L).injective).mpr hβ
    have hξ : (t / algebraMap ℂ L α) ^ n = 1 := by
      rw [div_pow, ht, ← map_pow, hα, div_self hιβ]
    have : NeZero n := ⟨hn⟩
    have hζ := Complex.isPrimitiveRoot_exp n hn
    obtain ⟨i, -, hi⟩ :=
      (hζ.map_of_injective (algebraMap ℂ L).injective).eq_pow_of_pow_eq_one hξ
    refine ⟨Complex.exp (2 * Real.pi * Complex.I / n) ^ i * α, ?_, ?_⟩
    · rw [mul_pow, ← pow_mul, mul_comm i n, pow_mul, hζ.pow_eq_one, one_pow, one_mul, hα]
    · rw [map_mul, map_pow, hi, div_mul_cancel₀ _ hια]

section Eval

variable (n : ℕ) (f : ℂ[X])

lemma eval₂_kummerPoly {S : Type*} [CommRing S] (i : ℂ[X] →+* S) (x : S) :
    (kummerPoly n f).eval₂ i x = x ^ n - i f := by
  simp [kummerPoly]

/-- Evaluation of the coordinate ring at a point `(a, b)` with `bⁿ = f(a)`. -/
noncomputable def kummerEval (a b : ℂ) (hb : b ^ n = f.eval a) : KummerRing n f →+* ℂ :=
  AdjoinRoot.lift (evalRingHom a) b (by rw [eval₂_kummerPoly, coe_evalRingHom, hb, sub_self])

variable {n f}

lemma kummerEval_of (a b : ℂ) (hb : b ^ n = f.eval a) (p : ℂ[X]) :
    kummerEval n f a b hb (AdjoinRoot.of _ p) = p.eval a :=
  AdjoinRoot.lift_of _

lemma kummerEval_algebraMap (a b : ℂ) (hb : b ^ n = f.eval a) (p : ℂ[X]) :
    kummerEval n f a b hb (algebraMap ℂ[X] (KummerRing n f) p) = p.eval a := by
  rw [AdjoinRoot.algebraMap_eq, kummerEval_of]

lemma kummerEval_root (a b : ℂ) (hb : b ^ n = f.eval a) :
    kummerEval n f a b hb (AdjoinRoot.root _) = b :=
  AdjoinRoot.lift_root _

lemma kummerEval_surjective (a b : ℂ) (hb : b ^ n = f.eval a) :
    Function.Surjective (kummerEval n f a b hb) :=
  fun z => ⟨AdjoinRoot.of _ (C z), by rw [kummerEval_of, eval_C]⟩

instance kummerEval_ker_isPrime (a b : ℂ) (hb : b ^ n = f.eval a) :
    (RingHom.ker (kummerEval n f a b hb)).IsPrime :=
  RingHom.ker_isPrime _

variable (n f) in
lemma kummerRing_root_pow :
    AdjoinRoot.root (kummerPoly n f) ^ n = algebraMap ℂ[X] (KummerRing n f) f := by
  have h0 := AdjoinRoot.eval₂_root (kummerPoly n f)
  rw [eval₂_kummerPoly, sub_eq_zero] at h0
  rw [h0, AdjoinRoot.algebraMap_eq]

variable (n f) in
/-- The coordinate `x − a` of the coordinate ring. -/
noncomputable def kummerShift (a : ℂ) : KummerRing n f :=
  algebraMap ℂ[X] (KummerRing n f) (X - C a)

lemma kummerShift_mem_ker (a b : ℂ) (hb : b ^ n = f.eval a) :
    kummerShift n f a ∈ RingHom.ker (kummerEval n f a b hb) := by
  rw [RingHom.mem_ker, kummerShift, kummerEval_algebraMap]
  simp

/-- The point ideal is generated by `x − a` and `y − b`. -/
lemma kummerKer_le_span (a b : ℂ) (hb : b ^ n = f.eval a) (r : KummerRing n f)
    (hr : r ∈ RingHom.ker (kummerEval n f a b hb)) :
    r ∈ Ideal.span {kummerShift n f a,
      AdjoinRoot.root (kummerPoly n f) - AdjoinRoot.of (kummerPoly n f) (C b)} := by
  induction r using AdjoinRoot.induction_on with
  | ih p =>
    obtain ⟨q, hq⟩ : (X - C (C b)) ∣ p - C (p.eval (C b)) := X_sub_C_dvd_sub_C_eval
    obtain ⟨q', hq'⟩ : (X - C a) ∣ p.eval (C b) - C ((p.eval (C b)).eval a) :=
      X_sub_C_dvd_sub_C_eval
    have h1 : AdjoinRoot.mk (kummerPoly n f) p =
        (AdjoinRoot.root (kummerPoly n f) - AdjoinRoot.of (kummerPoly n f) (C b)) *
            AdjoinRoot.mk (kummerPoly n f) q +
          AdjoinRoot.of (kummerPoly n f) (p.eval (C b)) := by
      have hp : p = (X - C (C b)) * q + C (p.eval (C b)) := by linear_combination hq
      conv_lhs => rw [hp]
      rw [map_add, map_mul, map_sub, AdjoinRoot.mk_X, AdjoinRoot.mk_C, AdjoinRoot.mk_C]
    have hg : (p.eval (C b)).eval a = 0 := by
      have he := hr
      rw [RingHom.mem_ker, h1, map_add, map_mul, map_sub, kummerEval_root, kummerEval_of,
        eval_C, sub_self, zero_mul, zero_add, kummerEval_of] at he
      exact he
    have h2 : AdjoinRoot.of (kummerPoly n f) (p.eval (C b)) =
        kummerShift n f a * AdjoinRoot.of (kummerPoly n f) q' := by
      have hpq : p.eval (C b) = (X - C a) * q' := by
        rw [← hq', hg, C_0, sub_zero]
      rw [hpq, map_mul, kummerShift, AdjoinRoot.algebraMap_eq]
    rw [h1, h2]
    exact Ideal.add_mem _ (Ideal.mul_mem_right _ _ (Ideal.subset_span (by simp)))
      (Ideal.mul_mem_right _ _ (Ideal.subset_span (by simp)))

end Eval

section Points

variable {n : ℕ} [NeZero n] {f : ℂ[X]}

instance kummerRing_isIntegral : Algebra.IsIntegral ℂ[X] (KummerRing n f) :=
  haveI := (AdjoinRoot.powerBasis' (kummerPoly_monic n f (NeZero.ne n))).finite
  Algebra.IsIntegral.of_finite ℂ[X] (KummerRing n f)

/-- **R01c-2a**: the maximal ideals of `ℂ[x][Y]/(Yⁿ − f)` are exactly the evaluation kernels
at the points `(a, b)` with `bⁿ = f(a)`. -/
theorem kummerRing_isMaximal_iff (𝔪 : Ideal (KummerRing n f)) :
    𝔪.IsMaximal ↔ ∃ (a b : ℂ) (hb : b ^ n = f.eval a), 𝔪 = RingHom.ker (kummerEval n f a b hb) := by
  constructor
  · intro hmax
    have hcomap := Ideal.isMaximal_comap_of_isIntegral_of_isMaximal'
      (algebraMap ℂ[X] (KummerRing n f)) (fun x => Algebra.IsIntegral.isIntegral x) 𝔪
    obtain ⟨a, ha⟩ := exists_X_sub_C_mem hcomap
    let : Field (KummerRing n f ⧸ 𝔪) := Ideal.Quotient.field 𝔪
    let q := Ideal.Quotient.mk 𝔪
    let ι := algebraMap ℂ (KummerRing n f ⧸ 𝔪)
    have hqX : q (AdjoinRoot.of _ X) = ι a := by
      have hmem : AdjoinRoot.of (kummerPoly n f) (X - C a) ∈ 𝔪 := ha
      have h0 := Ideal.Quotient.eq_zero_iff_mem.mpr hmem
      rw [map_sub, map_sub, sub_eq_zero] at h0
      rw [h0]
      rfl
    have hqp (p : ℂ[X]) : q (AdjoinRoot.of _ p) = ι (p.eval a) := by
      induction p using Polynomial.induction_on' with
      | add p r hp hr => rw [map_add, map_add, hp, hr, eval_add, map_add]
      | monomial k c =>
          rw [← C_mul_X_pow_eq_monomial, map_mul, map_mul, map_pow, map_pow, hqX, eval_mul,
            eval_C, eval_pow, eval_X, map_mul, map_pow]
          rfl
    have hpow : q (AdjoinRoot.root _) ^ n = ι (f.eval a) := by
      rw [← map_pow, kummerRing_root_pow, AdjoinRoot.algebraMap_eq, hqp]
    obtain ⟨b, hbb, hqr⟩ := exists_eq_algebraMap_of_pow_eq (NeZero.ne n) hpow
    refine ⟨a, b, hbb, ?_⟩
    have hext : q = ι.comp (kummerEval n f a b hbb) := by
      apply AdjoinRoot.ringHom_ext
      · ext p
        · simp only [RingHom.comp_apply]
          rw [hqp, kummerEval_of]
        · simp only [RingHom.comp_apply]
          rw [hqp, kummerEval_of]
      · simp only [RingHom.comp_apply]
        rw [hqr, kummerEval_root]
    have hker := congrArg RingHom.ker hext
    rw [Ideal.mk_ker, RingHom.ker_comp_of_injective _ ι.injective] at hker
    exact hker
  · rintro ⟨a, b, hb, rfl⟩
    exact RingHom.ker_isMaximal_of_surjective _ (kummerEval_surjective a b hb)

end Points

section Uniformizers

variable {n : ℕ} [NeZero n] {f : ℂ[X]} (a b : ℂ) (hb : b ^ n = f.eval a)
  (S : Type*) [CommRing S] [Algebra (KummerRing n f) S]
  [IsLocalization.AtPrime S (RingHom.ker (kummerEval n f a b hb))] [IsLocalRing S]

include hb

omit [NeZero n] in
/-- The image of the point ideal in its localization lies in any ideal containing the images
of `x − a` and `y − b`. -/
lemma kummerKer_map_le {I : Ideal S}
    (hx : algebraMap (KummerRing n f) S (kummerShift n f a) ∈ I)
    (hy : algebraMap (KummerRing n f) S
      (AdjoinRoot.root (kummerPoly n f) - AdjoinRoot.of (kummerPoly n f) (C b)) ∈ I) :
    IsLocalRing.maximalIdeal S ≤ I := by
  intro z hz
  obtain ⟨r, s, rfl⟩ := IsLocalization.exists_mk'_eq
    (RingHom.ker (kummerEval n f a b hb)).primeCompl z
  have hmem : r ∈ RingHom.ker (kummerEval n f a b hb) :=
    (IsLocalization.AtPrime.mk'_mem_maximal_iff S (RingHom.ker (kummerEval n f a b hb)) r s).mp hz
  rw [IsLocalization.mk'_eq_mul_mk'_one]
  refine Ideal.mul_mem_right _ _ ?_
  have hle : Ideal.map (algebraMap (KummerRing n f) S) (Ideal.span {kummerShift n f a,
      AdjoinRoot.root (kummerPoly n f) - AdjoinRoot.of (kummerPoly n f) (C b)}) ≤ I := by
    rw [Ideal.map_span, Ideal.span_le]
    rintro _ ⟨w, hw, rfl⟩
    rcases hw with rfl | rfl
    · exact hx
    · exact hy
  exact hle (Ideal.mem_map_of_mem _ (kummerKer_le_span a b hb r hmem))

/-- **R01c-2a, unramified points**: where `f(a) ≠ 0`, the coordinate `x − a` generates the
maximal ideal of the local ring. -/
theorem kummer_unramified_maximalIdeal (hfa : f.eval a ≠ 0) :
    IsLocalRing.maximalIdeal S =
      Ideal.span {algebraMap (KummerRing n f) S (kummerShift n f a)} := by
  have hb0 : b ≠ 0 := by
    rintro rfl
    exact hfa (by rw [← hb, zero_pow (NeZero.ne n)])
  set y := AdjoinRoot.root (kummerPoly n f)
  set bb := AdjoinRoot.of (kummerPoly n f) (C b)
  set u : KummerRing n f := ∑ i ∈ Finset.range n, y ^ i * bb ^ (n - 1 - i) with hu_def
  have hu : u ∈ (RingHom.ker (kummerEval n f a b hb)).primeCompl := by
    rw [Ideal.primeCompl, Submonoid.mem_mk, Subsemigroup.mem_mk, Set.mem_compl_iff,
      SetLike.mem_coe, RingHom.mem_ker]
    have heval : kummerEval n f a b hb u = (n : ℂ) * b ^ (n - 1) := by
      rw [hu_def, map_sum]
      simp only [map_mul, map_pow, y, bb, kummerEval_root, kummerEval_of, eval_C]
      rw [Finset.sum_congr rfl fun i hi => by
        rw [← pow_add, Nat.add_sub_cancel' (Nat.le_sub_one_of_lt (Finset.mem_range.mp hi))],
        Finset.sum_const, Finset.card_range, nsmul_eq_mul]
    rw [heval]
    exact mul_ne_zero (Nat.cast_ne_zero.mpr (NeZero.ne n)) (pow_ne_zero _ hb0)
  obtain ⟨g, hg⟩ : (X - C a) ∣ f - C (f.eval a) := X_sub_C_dvd_sub_C_eval
  have hfac : (y - bb) * u = kummerShift n f a * AdjoinRoot.of (kummerPoly n f) g := by
    rw [mul_comm, hu_def, geom_sum₂_mul, kummerRing_root_pow, ← map_pow, ← C_pow, hb,
      kummerShift, AdjoinRoot.algebraMap_eq, ← map_mul, ← hg, map_sub]
  obtain ⟨v, hv⟩ := (IsLocalization.map_units S ⟨u, hu⟩).exists_right_inv
  have hy : algebraMap (KummerRing n f) S (y - bb) ∈
      Ideal.span {algebraMap (KummerRing n f) S (kummerShift n f a)} := by
    refine Ideal.mem_span_singleton.mpr
      ⟨algebraMap (KummerRing n f) S (AdjoinRoot.of (kummerPoly n f) g) * v, ?_⟩
    calc algebraMap (KummerRing n f) S (y - bb)
        = algebraMap (KummerRing n f) S ((y - bb) * u) * v := by
          rw [map_mul, mul_assoc, hv, mul_one]
      _ = algebraMap (KummerRing n f) S (kummerShift n f a) *
            (algebraMap (KummerRing n f) S (AdjoinRoot.of (kummerPoly n f) g) * v) := by
          rw [hfac, map_mul, mul_assoc]
  refine le_antisymm (kummerKer_map_le a b hb S (Ideal.mem_span_singleton_self _) hy) ?_
  rw [Ideal.span_le, Set.singleton_subset_iff, SetLike.mem_coe]
  exact (IsLocalization.AtPrime.to_map_mem_maximal_iff S
    (RingHom.ker (kummerEval n f a b hb)) (kummerShift n f a)).mpr (kummerShift_mem_ker a b hb)

/-- **R01c-2a, ramified points**: where `f(a) = 0` (so `b = 0`), the root `y` generates the
maximal ideal of the local ring. -/
theorem kummer_ramified_maximalIdeal [Fact (Squarefree f)] (hfa : f.eval a = 0) :
    IsLocalRing.maximalIdeal S =
      Ideal.span {algebraMap (KummerRing n f) S (AdjoinRoot.root (kummerPoly n f))} := by
  have hb0 : b = 0 := (pow_eq_zero_iff (NeZero.ne n)).mp (hb.trans hfa)
  set y := AdjoinRoot.root (kummerPoly n f)
  obtain ⟨k, hk, hka⟩ := exists_factor_of_root f a hfa
  have hk_mem : AdjoinRoot.of (kummerPoly n f) k ∈
      (RingHom.ker (kummerEval n f a b hb)).primeCompl := by
    rw [Ideal.primeCompl, Submonoid.mem_mk, Subsemigroup.mem_mk, Set.mem_compl_iff,
      SetLike.mem_coe, RingHom.mem_ker, kummerEval_of]
    exact hka
  obtain ⟨v, hv⟩ := (IsLocalization.map_units S ⟨_, hk_mem⟩).exists_right_inv
  have hfac : kummerShift n f a * AdjoinRoot.of (kummerPoly n f) k = y ^ n := by
    rw [kummerRing_root_pow, kummerShift, AdjoinRoot.algebraMap_eq, ← map_mul, ← hk]
  have hx : algebraMap (KummerRing n f) S (kummerShift n f a) ∈
      Ideal.span {algebraMap (KummerRing n f) S y} := by
    refine Ideal.mem_span_singleton.mpr ⟨algebraMap (KummerRing n f) S y ^ (n - 1) * v, ?_⟩
    calc algebraMap (KummerRing n f) S (kummerShift n f a)
        = algebraMap (KummerRing n f) S
            (kummerShift n f a * AdjoinRoot.of (kummerPoly n f) k) * v := by
          rw [map_mul, mul_assoc, hv, mul_one]
      _ = algebraMap (KummerRing n f) S y * (algebraMap (KummerRing n f) S y ^ (n - 1) * v) := by
          rw [hfac, map_pow, ← mul_assoc, ← pow_succ',
            Nat.sub_add_cancel (Nat.pos_of_ne_zero (NeZero.ne n))]
  have hy : algebraMap (KummerRing n f) S (y - AdjoinRoot.of (kummerPoly n f) (C b)) ∈
      Ideal.span {algebraMap (KummerRing n f) S y} := by
    rw [hb0, C_0, map_zero, sub_zero]
    exact Ideal.mem_span_singleton_self _
  refine le_antisymm (kummerKer_map_le a b hb S hx hy) ?_
  rw [Ideal.span_le, Set.singleton_subset_iff, SetLike.mem_coe]
  refine (IsLocalization.AtPrime.to_map_mem_maximal_iff S
    (RingHom.ker (kummerEval n f a b hb)) y).mpr ?_
  rw [RingHom.mem_ker, kummerEval_root, hb0]

end Uniformizers

section Dedekind

variable {n : ℕ} [NeZero n] {f : ℂ[X]} [Fact (Squarefree f)] [Fact (0 < f.natDegree)]

instance kummerRat_fact : Fact (Irreducible (kummerRat n f)) :=
  ⟨kummerRat_irreducible n f (NeZero.ne n) Fact.out Fact.out⟩

instance kummerRing_isDomain : IsDomain (KummerRing n f) :=
  AdjoinRoot.isDomain_of_prime (UniqueFactorizationMonoid.irreducible_iff_prime.mp
    (kummerPoly_irreducible n f (NeZero.ne n) Fact.out Fact.out))

instance kummerRing_isNoetherianRing : IsNoetherianRing (KummerRing n f) :=
  haveI := (AdjoinRoot.powerBasis' (kummerPoly_monic n f (NeZero.ne n))).finite
  IsNoetherianRing.of_finite ℂ[X] (KummerRing n f)

lemma kummerShift_ne_zero (a : ℂ) : kummerShift n f a ≠ 0 := by
  intro h0
  have := congrArg (kummerRingMap n f) h0
  rw [kummerShift, AlgHom.commutes, map_zero,
    IsScalarTower.algebraMap_apply ℂ[X] (RatFunc ℂ) (KummerField n f)] at this
  have hX := (algebraMap (RatFunc ℂ) (KummerField n f)).injective (this.trans (map_zero _).symm)
  exact X_sub_C_ne_zero a (RatFunc.algebraMap_injective ℂ (hX.trans (map_zero _).symm))

lemma kummerEval_ker_ne_bot (a b : ℂ) (hb : b ^ n = f.eval a) :
    RingHom.ker (kummerEval n f a b hb) ≠ ⊥ := by
  intro hbot
  have hmem := kummerShift_mem_ker a b hb
  rw [hbot, Ideal.mem_bot] at hmem
  exact kummerShift_ne_zero a hmem

/-- **R01c-2a**: the local ring at every point is a discrete valuation ring. -/
theorem kummer_localization_dvr (a b : ℂ) (hb : b ^ n = f.eval a) :
    IsDiscreteValuationRing (Localization.AtPrime (RingHom.ker (kummerEval n f a b hb))) := by
  have hnf := IsLocalization.AtPrime.not_isField (KummerRing n f) (kummerEval_ker_ne_bot a b hb)
    (Localization.AtPrime (RingHom.ker (kummerEval n f a b hb)))
  refine ((IsDiscreteValuationRing.TFAE _ hnf).out 4 0).mp ?_
  by_cases hfa : f.eval a = 0
  · rw [kummer_ramified_maximalIdeal a b hb _ hfa]
    exact ⟨⟨_, rfl⟩⟩
  · rw [kummer_unramified_maximalIdeal a b hb _ hfa]
    exact ⟨⟨_, rfl⟩⟩

/-- **R01c-2a**: the coordinate ring of the Kummer cover is a Dedekind domain. -/
theorem kummerRing_isDedekindDomain : IsDedekindDomain (KummerRing n f) :=
  have : IsDedekindDomainDvr (KummerRing n f) :=
    { toIsNoetherian := inferInstance
      is_dvr_at_nonzero_prime := fun P hP hPp => by
        have hmax : P.IsMaximal := by
          have hne : P.under ℂ[X] ≠ ⊥ := fun h => hP (Ideal.eq_bot_of_comap_eq_bot h)
          exact Ideal.isMaximal_of_isIntegral_of_isMaximal_comap (R := ℂ[X]) P
            (IsPrime.to_maximal_ideal hne)
        obtain ⟨a, b, hb, rfl⟩ := (kummerRing_isMaximal_iff P).mp hmax
        exact kummer_localization_dvr a b hb }
  IsDedekindDomainDvr.isDedekindDomain (KummerRing n f)

end Dedekind

end CurveSymmetry

end

Source

C. Perassi, Sharp symmetry bounds for real algebraic curves (note), definitions of the formalization, https://github.com/carlok/curve-symmetry-lean/blob/d99bc17a1c397956c05d7417de50f9beed56580f/sharp_symmetry_bounds.pdf. Lean modules KummerLocal in https://github.com/carlok/curve-symmetry-lean/tree/d99bc17a1c397956c05d7417de50f9beed56580f/lean (C. Perassi)

View graph

Points of the Kummer cover yn=f(x)y^n=f(x)yn=f(x): evaluation homomorphisms and the local coordinate x−ax-ax−a

Points of the Kummer cover $y^n=f(x)$ : evaluation homomorphisms and the local coordinate $x-a$