The local ring at an affine point of a normal coordinate ring is a discrete valuation ring

An integrally closed coordinate ring is a Dedekind domain (WeierstrassCurve.Affine.isDedekindDomain_coordinateRing_of_isIntegrallyClosed), and the ideal of a point is maximal and nonzero (XYIdeal_isMaximal_of_equation, XYIdeal_ne_bot). Localising at that ideal therefore gives a discrete valuation ring. Normality is what is assumed; for an elliptic curve WeierstrassCurve.Affine.isIntegrallyClosed_coordinateRing supplies it.

Main results

• WeierstrassCurve.Affine.CoordinateRing.isDiscreteValuationRing_localizationAtPrime: the localisation of the coordinate ring at ⟨X - x, Y - y(X)⟩ is a discrete valuation ring, for any y : F[X] solving the Weierstrass equation at x — in particular at a point of the curve, through XYIdeal_isMaximal_of_equation. It asks integral closedness of the coordinate ring, not ellipticity of the curve.

Mathlib's IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain is applied directly; what this file contributes is that both of its hypotheses hold at such an ideal — primality from XYIdeal_isMaximal and non-vanishing from XYIdeal_ne_bot — over a coordinate ring already known to be Dedekind.

No valuation is defined here: the result gives the IsDiscreteValuationRing structure, which is what an order-of-vanishing and uniformiser API would be built on.

Roadmap

TauCetiRoadmap/EllipticCurves/README.md, Layer 0 (the function field, places, and divisors). That layer's §Places asks for the affine places as the maximal ideals of the coordinate ring, "for elliptic W a Dedekind domain — itself a worthwhile lemma", together with an API of ord_v, uniformisers and residue fields; this supplies the local rings that such an API is stated over. The layer says its own place types are new API to be built there rather than pinned, and it seeds no declaration this competes with; it also records that the design is coordinated with D. Angdinata's in-flight upstream CoordinateRing work.

Provenance

The statement is that of localRing_isDVR in the AINTLIB HasseWeil project (github.com/CBirkbeck/AINTLIB, Apache-2.0, pinned by that roadmap at dev/hasse-weil @ 513e83879e2f), HasseWeil/Valuation.lean. Its proof is not ported: with the coordinate ring already known to be a Dedekind domain, Mathlib's IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain gives the conclusion directly. The source's hypothesis is nonsingularity of the point; here the curve equation suffices, matching the weakening already made for XYIdeal_isMaximal_of_equation.

theorem WeierstrassCurve.Affine.CoordinateRing.isDiscreteValuationRing_localizationAtPrime {F : Type u_1} [Field F] {W : Affine F} {x : F} [IsIntegrallyClosed W.CoordinateRing] {y : Polynomial F} (h : Polynomial.eval x (Polynomial.eval y W.polynomial) = 0) : IsDiscreteValuationRing (Localization.AtPrime (XYIdeal W x y))

The local ring of a normal coordinate ring at ⟨X - x, Y - y(X)⟩ is a discrete valuation ring, whenever y solves the Weierstrass equation at x. The curve is not assumed elliptic, only its coordinate ring integrally closed. The primality of the ideal is a consequence of the equation, through XYIdeal_isMaximal, so it is installed in the statement rather than assumed.