Prove2Me

Places of C(t)[W]/(W2−h)\mathbb C(t)[W]/(W^2-h) containing C[t]\mathbb C[t] correspond bijectively to the points of w2=h(t)w^2=h(t)

Proved
CurveSymmetry.quad_finite_place_classification

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

curve-symmetry-leanfunction-fieldsvaluation-theory

Let h∈C[t]h\in\mathbb C[t] be squarefree and such that W2−h(t)W^2-h(t) is irreducible in C(t)[W]\mathbb C(t)[W]. Let Lh=C(t)[W]/(W2−h(t))L_h=\mathbb C(t)[W]/(W^2-h(t)), a quadratic field extension of C(t)\mathbb C(t), and let Rh=C[t][W]/(W2−h(t))R_h=\mathbb C[t][W]/(W^2-h(t)), mapped into LhL_h by sending WW to the class ww of WW. For c,d∈Cc,d\in\mathbb C with d2=h(c)d^2=h(c), let mc,d⊂Rh\mathfrak m_{c,d}\subset R_h be the kernel of the evaluation t↦ct\mapsto c, W↦dW\mapsto d, and let Oc,d={a/s: a,s∈Rh, s∉mc,d}⊆Lh\mathcal O_{c,d}=\{a/s:\ a,s\in R_h,\ s\notin\mathfrak m_{c,d}\}\subseteq L_h be the local ring of the point (c,d)(c,d). Then:

  1. for all c,dc,d with d2=h(c)d^2=h(c), Oc,d≠Lh\mathcal O_{c,d}\ne L_h and Oc,d\mathcal O_{c,d} contains C[t]\mathbb C[t];
  2. every valuation subring O\mathcal O of LhL_h with O≠Lh\mathcal O\ne L_h and C[t]⊆O\mathbb C[t]\subseteq\mathcal O equals Oc,d\mathcal O_{c,d} for some c,d∈Cc,d\in\mathbb C with d2=h(c)d^2=h(c);
  3. if d2=h(c)d^2=h(c), d′2=h(c′)d'^2=h(c') and Oc,d=Oc′,d′\mathcal O_{c,d}=\mathcal O_{c',d'}, then c=c′c=c' and d=d′d=d'.

Hence the points of w2=h(t)w^2=h(t) correspond bijectively to the places of LhL_h containing C[t]\mathbb C[t]:

{(c,d)∈C2: d2=h(c)} → ∼  {O⊊Lh valuation subring: C[t]⊆O},(c,d)↦Oc,d.\{(c,d)\in\mathbb C^2:\ d^2=h(c)\}\ \xrightarrow{\ \sim\ }\ \{\mathcal O\subsetneq L_h\ \text{valuation subring}:\ \mathbb C[t]\subseteq\mathcal O\},\qquad (c,d)\mapsto\mathcal O_{c,d}.

These are the places of the double cover over the finite tt-line. With hh the branch polynomial of the double cover (7), this is used for the genus in Lemma 4 and for Remark 5.

Formalization Note: the two hypotheses on hh are Fact instances; they make RhR_h a Dedekind domain with fraction field LhL_h, and Oc,d\mathcal O_{c,d} is built as the localization of RhR_h at mc,d\mathfrak m_{c,d}.

Preamble
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 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.RingTheory.AdjoinRoot
import Mathlib.RingTheory.DedekindDomain.Dvr
import Mathlib.RingTheory.DiscreteValuationRing.TFAE
import Mathlib.RingTheory.Localization.AsSubring
import Mathlib.RingTheory.MvPolynomial.Homogeneous
import Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
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

open CurveSymmetry
set_option autoImplicit false
open Polynomial
variable (h : ℂ[X])
variable [hsq : Fact (Squarefree h)] [hirr : Fact (Irreducible (quadRat h))]
Formal statement
theorem CurveSymmetry.quad_finite_place_classification :
    (∀ (c d : ℂ) (hd : d ^ 2 = h.eval c), quadPlace h c d hd ≠ ⊤ ∧
        ∀ p : ℂ[X], algebraMap ℂ[X] (QuadField h) p ∈ quadPlace h c d hd) ∧
      (∀ O : ValuationSubring (QuadField h), O ≠ ⊤ →
        (∀ p : ℂ[X], algebraMap ℂ[X] (QuadField h) p ∈ O) →
          ∃ (c d : ℂ) (hd : d ^ 2 = h.eval c), O = quadPlace h c d hd) ∧
      (∀ (c d c' d' : ℂ) (hd : d ^ 2 = h.eval c) (hd' : d' ^ 2 = h.eval c'),
        quadPlace h c d hd = quadPlace h c' d' hd' → c = c' ∧ d = d') := by sorry
Source
C. Perassi, Sharp symmetry bounds for real algebraic curves (note): lemma of the formalization, for proof of Lemma 4, equation (7), p. 3, https://github.com/carlok/curve-symmetry-lean/blob/d99bc17a1c397956c05d7417de50f9beed56580f/sharp_symmetry_bounds.pdf. Lean: https://github.com/carlok/curve-symmetry-lean/blob/d99bc17a1c397956c05d7417de50f9beed56580f/lean/QuadraticPlaces.lean (C. Perassi)

View graph