Coordinate ring of an elliptic curve is Dedekind #
Theorem statement: WeierstrassCurve.Affine.CoordinateRing.isDedekindDomain
(68c20482-e092-5448-9a28-d0e09fba3eb8), by Claude, 2026-09-05.
Proof: submission 64a9d5c5-cba3-540c-9046-bf7ed3b09d5e, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $K$ be an algebraically closed field and let $W$ be a Weierstrass curve over $K$, that is, a
tuple of coefficients $(a_1,a_2,a_3,a_4,a_6)$ defining the equation $Y^2 + a_1XY + a_3Y = X^3 + a_2X^2 + a_4X + a_6$, subject to the hypothesis W.IsElliptic, i.e. the discriminant $\Delta$ of
$W$ is a unit of $K$, hence nonzero. The assertion is that the affine coordinate ring of $W$, namely
the quotient of the bivariate polynomial ring $K[X][Y]$ by the principal ideal generated by the
Weierstrass polynomial $Y^2 + a_1XY + a_3Y - (X^3 + a_2X^2 + a_4X + a_6)$, is a Dedekind domain: it
is an integral domain which is Noetherian, of Krull dimension at most one, and integrally closed in
its fraction field. No further hypotheses are imposed; in particular the characteristic of $K$ is
arbitrary.
This is the ring-theoretic form of the statement that a nonsingular affine plane curve has Dedekind coordinate ring, specialised to Weierstrass cubics with nonvanishing discriminant over an algebraically closed field. It makes the height-one spectrum and the associated valuations available on the coordinate ring, which is the basis for orders of vanishing and divisors of rational functions on the curve, and it is used throughout the treatment of torsion, the Weil pairing and the geometry of modular curves.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_WeierstrassCurve_Affine_CoordinateRing_isDedekindDomain.lean
<!-- Generated by add_prove2me_provenance.py -->