The center of the localization $A_{\mathfrak p}$ of a Dedekind domain at a nonzero prime $\mathfrak p$ is $\mathfrak p$

Proved

CurveSymmetry.placeCenter_primeValuationSubring

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

curve-symmetry-leanfunction-fieldsvaluation-theory

Let $A$ be a Dedekind domain with field of fractions $K$ , and identify $A$ with its image in $K$ . For a nonzero prime ideal $\mathfrak p$ of $A$ , let $A_{\mathfrak p}=\{a/s:\ a\in A,\ s\in A\setminus\mathfrak p\}\subseteq K$ be the localization, a valuation subring of $K$ . For a valuation subring $\mathcal O$ of $K$ containing $A$ , with maximal ideal $\mathfrak m_{\mathcal O}$ , call $\mathfrak c(\mathcal O)=\{a\in A:\ a\in\mathfrak m_{\mathcal O}\}$ its center in $A$ . Then

\mathfrak c(A_{\mathfrak p})=\mathfrak p.

Together with the converse (a valuation subring of $K$ containing $A$ and different from $K$ is the localization at its center), this matches the places of $K$ containing $A$ with the nonzero primes of $A$ . It is applied to the coordinate ring of the double cover (7) to classify the places of its function field, for Lemma 4 and Remark 5.

Preamble

import Definitions.Def_CurveSymmetry_07_Places
import Mathlib.RingTheory.DedekindDomain.Dvr
import Mathlib.RingTheory.DiscreteValuationRing.TFAE
import Mathlib.RingTheory.Localization.AsSubring
import Mathlib.RingTheory.Valuation.ValuationSubring

open CurveSymmetry
set_option autoImplicit false
open IsLocalRing
variable {A K : Type*} [CommRing A] [IsDedekindDomain A] [Field K] [Algebra A K]
  [IsFractionRing A K]

Formal statement

theorem CurveSymmetry.placeCenter_primeValuationSubring (P : Ideal A) [P.IsPrime] (hP : P ≠ ⊥) :
    placeCenter K (primeValuationSubring K P hP) (algebraMap_mem_primeValuationSubring hP) = P := 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/DedekindPlaces.lean (C. Perassi)

View graph

The center of the localization ApA_{\mathfrak p}Ap​ of a Dedekind domain at a nonzero prime p\mathfrak pp is p\mathfrak pp

The center of the localization $A_{\mathfrak p}$ of a Dedekind domain at a nonzero prime $\mathfrak p$ is $\mathfrak p$