The function field of an elliptic curve has genus one #

Let W be an elliptic Weierstrass curve over a field F, with coordinate functions x and y and place at infinity O. This file computes the Riemann–Roch spaces L(n · O) by hand and reads off the two invariants of F(W) / F that the general theory of function fields needs:

F is the exact field of constants of F(W);
F(W) has genus one, and is therefore an elliptic function field in the sense of TauCeti.IsEllipticFunctionField, the place at infinity being rational.

The computation is the classical one. A function with no pole away from O is regular at every height-one prime of the coordinate ring, which is a Dedekind domain, so it lies in the coordinate ring and is p + q y for polynomials p and q. At infinity the two summands have pole orders 2 deg p and 2 deg q + 3; these have different parities, so they never cancel, and

p + q y ∈ L(n · O) exactly when 2 deg p ≤ n and 2 deg q + 3 ≤ n.

Counting the monomials xⁱ and xʲ y allowed by these bounds gives ℓ(n · O) = n for n ≥ 1 and ℓ(0) = 1. The second value says the constants are exact; the first, compared with Riemann's theorem in large degree, says the genus is one. No Riemann–Roch theorem, differential or ramification computation is used.

Main results #

WeierstrassCurve.Affine.mem_riemannRochSpace_natCast_zsmul_ofPoint_infinity_iff: the functions in L(n · O) are the p + q y with 2 deg p ≤ n and 2 deg q + 3 ≤ n.
WeierstrassCurve.Affine.isIntegrallyClosedIn_functionField: F is the exact field of constants of F(W).
WeierstrassCurve.Affine.genus_functionField: F(W) has genus one.
WeierstrassCurve.Affine.isEllipticFunctionField: F(W) / F is an elliptic function field.

References #

H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Definition 1.4.15, Theorem 1.4.17 and Proposition 6.1.3.
J. Silverman, The Arithmetic of Elliptic Curves, Section III.3.

Pole orders at infinity #

The monomials `xⁱ` and `xʲ y` #

The Riemann–Roch spaces `L(n · O)` #

source

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

IsDedekindDomain W.CoordinateRing

source

theorem WeierstrassCurve.Affine.mem_riemannRochSpace_natCast_zsmul_ofPoint_infinity_iff {F : Type u_1} [Field F] (W : Affine F) [WeierstrassCurve.IsElliptic W] {n : ℕ} {f : W.FunctionField} :

f ∈ TauCeti.riemannRochSpace (↑n • TauCeti.AlgebraicGeometry.WeilDivisor.ofPoint (TauCeti.Place.infinity W)) ↔ ∃ (p : Polynomial F) (q : Polynomial F), 2 * p.natDegree ≤ n ∧ (q = 0 ∨ 2 * q.natDegree + 3 ≤ n) ∧ (algebraMap (Polynomial F) W.FunctionField) p + (algebraMap (Polynomial F) W.FunctionField) q * (algebraMap W.CoordinateRing W.FunctionField) ((CoordinateRing.mk W) Polynomial.X) = f

The Riemann–Roch spaces at infinity of an elliptic curve: for n : ℕ, a function lies in L(n · O) exactly when it is p + q y for polynomials p and q with 2 deg p ≤ n and 2 deg q + 3 ≤ n (the latter read as vacuous when q = 0). So L(n · O) is spanned by the monomials xⁱ with 2i ≤ n and xʲ y with 2j + 3 ≤ n.

source

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

IsIntegrallyClosedIn F W.FunctionField

F is the exact field of constants of the function field of an elliptic curve: the functions without poles form the one-dimensional space L(0), which is the field of constants.

source

@[simp]

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

TauCeti.genus F W.FunctionField = 1

The function field of an elliptic curve has genus one. Riemann's theorem gives ℓ(D) = deg D + 1 - g for every divisor of large degree, and at D = n · O the left side is n while deg D = n, the place at infinity being rational.

source