The coordinate ring of an elliptic curve is a Dedekind domain

For a Weierstrass curve W over a field F the coordinate ring F[W] = F[X, Y]/(W(X, Y)) is a free F[X]-module of rank two, so it is noetherian of dimension at most one for free. The content of this file is the remaining, and only nontrivial, Dedekind axiom: F[W] is integrally closed whenever W is elliptic.

The proof is the quadratic-extension calculation, run at one prime at a time. Writing s = a₁X + a₃ and c = X³ + a₂X² + a₄X + a₆, the coordinate ring carries the conjugation y ↦ -y - s — the coordinate-ring form of Mathlib's WeierstrassCurve.Affine.negY — and an element z of the function field integral over F[X] may be written (p + qy)/d. Its trace (2p - qs)/d and its norm (p² - pqs - q²c)/d² again lie in F(X) and are again integral, so F[X] being integrally closed forces d ∣ 2p - qs and d² ∣ p² - pqs - q²c. That divisibility input alone forces d ∣ p and d ∣ q, which says exactly z ∈ F[W].

The last step is where the curve enters, and it is a genuine use of nonsingularity rather than a discriminant computation, so no characteristic is special. Suppose a prime π divides d but not q, and let k = F[X]/(π). Choosing g with p ≡ gq modulo π, the two divisibilities say that π² divides H = g² - gs - c and that π divides 2g - s. Then π ∣ H and π ∣ H', and reading H' = g'(2g - s) - a₁g - c' modulo π turns those into

• (x₀, β) lies on W over k, where x₀ is the image of X and β the image of -g;
• W_Y(x₀, β) = 2β + a₁x₀ + a₃ = 0, which is π ∣ 2g - s;
• W_X(x₀, β) = a₁β - (3x₀² + 2a₂x₀ + a₄) = 0, which is π ∣ a₁g + c'.

That is a singular point of an elliptic curve, which is absurd. The argument is uniform in the characteristic, unlike the familiar route through Squarefree (4X³ + b₂X² + 2b₄X + b₆): in characteristic two that polynomial is the square (a₁X + a₃)².

Main definitions

• WeierstrassCurve.Affine.CoordinateRing.conj: the conjugation involution of R[W] over R[X], sending y to -y - (a₁X + a₃).

Main results

• WeierstrassCurve.Affine.CoordinateRing.mul_conj: x * conj x is the norm of x.
• WeierstrassCurve.Affine.CoordinateRing.add_negPolynomial_smul_basis: the expanded conjugation formula computes the trace on the basis {1, Y}.
• WeierstrassCurve.Affine.isIntegrallyClosed_coordinateRing: the coordinate ring of an elliptic curve over a field is integrally closed.
• WeierstrassCurve.Affine.isDedekindDomain_coordinateRing_of_isIntegrallyClosed: an integrally closed coordinate ring is a Dedekind domain — so an elliptic curve's is, by isIntegrallyClosed_coordinateRing.

The integral closedness is the seeded milestone isIntegrallyClosed_coordinateRing of TauCetiRoadmap/EllipticCurves/README.md, Layer 1, where it is named as the normality input to the induced map on points Isogeny.toPointHom; the Dedekind statement is the "worthwhile lemma" that Layer 0 asks for, on which the identification of the affine places with the maximal ideals of the coordinate ring rests.

Provenance

Not ported; these are direct proofs. Mathlib knows the coordinate ring, its R[X]-basis {1, Y} and the norm of p • 1 + q • Y (WeierstrassCurve.Affine.CoordinateRing.norm_smul_basis), all of which are used here, but has no normality or Dedekind statement about it.

isDedekindDomain_coordinateRing_of_isIntegrallyClosed asks normality and nothing else because the coordinate ring is module-finite over F[X], which carries Noetherianity and dimension at most one across; for an elliptic curve isIntegrallyClosed_coordinateRing then supplies the normality.

Conjugation on the coordinate ring

theorem WeierstrassCurve.Affine.CoordinateRing.eval₂_negPolynomial_polynomial {R : Type u_1} [CommRing R] (W : Affine R) : Polynomial.eval₂ Polynomial.C W.negPolynomial W.polynomial = W.polynomial

Substituting -Y - (a₁X + a₃) for Y leaves the Weierstrass polynomial unchanged: the two roots of W(X, ·) are y and its conjugate -y - (a₁X + a₃).

theorem WeierstrassCurve.Affine.CoordinateRing.mk_C_eq_algebraMap {R : Type u_1} [CommRing R] (W : Affine R) (r : Polynomial R) : (mk W) (Polynomial.C r) = (algebraMap (Polynomial R) W.CoordinateRing) r

The class of a constant polynomial is its image under algebraMap. AdjoinRoot.mk_C in the algebraMap spelling that rewriting wants.

Public because it is the canonical form of an identity that consumers otherwise re-prove: it is the coordinate-ring half of every mk W (C p) computation, and composing it with IsScalarTower.algebraMap_apply carries the class all the way into the function field.

noncomputable def WeierstrassCurve.Affine.CoordinateRing.conj {R : Type u_1} [CommRing R] (W : Affine R) : W.CoordinateRing ≃ₐ[Polynomial R] W.CoordinateRing

The conjugation involution of the coordinate ring R[W] over R[X], sending y to -y - (a₁X + a₃). It is the coordinate-ring form of WeierstrassCurve.Affine.negY: the pullback of the involution (x, y) ↦ (x, -y - a₁x - a₃) of the curve.

Equations

• WeierstrassCurve.Affine.CoordinateRing.conj W = AlgEquiv.ofAlgHom (WeierstrassCurve.Affine.CoordinateRing.conjHom✝ W) (WeierstrassCurve.Affine.CoordinateRing.conjHom✝ W) ⋯ ⋯

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.conj_mk_Y {R : Type u_1} [CommRing R] (W : Affine R) : (conj W) (AdjoinRoot.root W.polynomial) = (mk W) W.negPolynomial

Conjugation sends the coordinate y to -y - (a₁X + a₃).

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.conj_mk_C {R : Type u_1} [CommRing R] (W : Affine R) (r : Polynomial R) : (conj W) ((AdjoinRoot.of W.polynomial) r) = (mk W) (Polynomial.C r)

Conjugation fixes the coefficient ring R[X].

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.conj_conj {R : Type u_1} [CommRing R] (W : Affine R) (x : W.CoordinateRing) : (conj W) ((conj W) x) = x

Conjugation is an involution.

theorem WeierstrassCurve.Affine.CoordinateRing.conj_smul_basis {R : Type u_1} [CommRing R] (W : Affine R) (p q : Polynomial R) : (conj W) (p • 1 + q • (mk W) Polynomial.X) = (mk W) (Polynomial.C p + Polynomial.C q * W.negPolynomial)

In the basis {1, Y}, conjugation sends the element with coordinates (p, q) to the polynomial representative p + q * W.negPolynomial.

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.add_negPolynomial_smul_basis {R : Type u_1} [CommRing R] (W : Affine R) (p q : Polynomial R) : p • 1 + q • AdjoinRoot.root W.polynomial + (p • 1 + (AdjoinRoot.mk W.polynomial) (q • W.negPolynomial)) = (algebraMap (Polynomial R) W.CoordinateRing) (2 * p - q * (Polynomial.C W.a₁ * Polynomial.X + Polynomial.C W.a₃))

The sum of an element of the coordinate ring and its conjugate is its trace 2p - qs.

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.mul_conj {R : Type u_1} [CommRing R] (W : Affine R) (x : W.CoordinateRing) : x * (conj W) x = (algebraMap (Polynomial R) W.CoordinateRing) ((Algebra.norm (Polynomial R)) x)

The product of an element of the coordinate ring and its conjugate is its norm.

The divisibility core

Integral closedness

theorem WeierstrassCurve.Affine.isIntegrallyClosed_coordinateRing {F : Type u_1} [Field F] (W : Affine F) [WeierstrassCurve.IsElliptic W] : IsIntegrallyClosed W.CoordinateRing

The coordinate ring of an elliptic curve is integrally closed. This is the normality half of the statement that it is a Dedekind domain, and the input that the induced map on points of an isogeny consumes.

theorem WeierstrassCurve.Affine.isDedekindDomain_coordinateRing_of_isIntegrallyClosed {F : Type u_1} [Field F] (W : Affine F) [IsIntegrallyClosed W.CoordinateRing] : IsDedekindDomain W.CoordinateRing

An integrally closed coordinate ring is a Dedekind domain.