Nonsingularity of the Weierstrass equation of a genus-one function field

Let x and y be Weierstrass coordinates at a place P of degree one of a function field F / k: they have pole divisors 2P and 3P and satisfy the equation of a Weierstrass curve W over k. This file shows that W has no singular point over k unless F has genus zero; over a perfect field this makes W an elliptic curve.

The argument is the classical one. If (x₀, y₀) ∈ k² is a singular point of W, then the Taylor expansion of the Weierstrass equation at it reads Y² + a₁XY = X³ + (3x₀ + a₂)X² for X = x - x₀ and Y = y - y₀. Dividing by X² shows that the slope z = Y / X satisfies X = z² + a₁z - (3x₀ + a₂) and Y = zX, so x and y lie in k(z). Since x and y generate F, so does z, and F has genus zero.

Over a perfect field a singular Weierstrass curve always has a rational singular point (WeierstrassCurve.Affine.exists_isSingular_of_Δ_eq_zero), so the Weierstrass curve of a genus-one function field is elliptic. Over an imperfect field a singular point need not be rational (for y² = x³ + t over 𝔽₂(t) it is (0, √t)), and the argument gives no information there. For two of the normal forms, nonsingularity has a form that needs no perfectness: the cubic of Y² = X³ + a₂X² + a₄X + a₆ is squarefree, because a double root of it is a rational singular point, and a₆ ≠ 0 in Y² + XY = X³ + a₂X² + a₆, because otherwise the origin is singular.

Main results

• TauCeti.Place.IsWeierstrassCoordinates.adjoin_div_eq_top_of_isSingular: at a rational singular point (x₀, y₀) of W, the slope (y - y₀) / (x - x₀) generates F.
• TauCeti.Place.IsWeierstrassCoordinates.genus_eq_zero_of_isSingular: so F has genus zero.
• TauCeti.Place.IsWeierstrassCoordinates.isElliptic: over a perfect field, the Weierstrass curve of a function field of nonzero genus is elliptic.
• TauCeti.Place.IsWeierstrassCoordinates.squarefree_of_isCharNeTwoNF and TauCeti.Place.IsWeierstrassCoordinates.a₆_ne_zero_of_isCharTwoJNeZeroNF: the nonsingularity conditions of the normal forms Y² = X³ + a₂X² + a₄X + a₆ and Y² + XY = X³ + a₂X² + a₆, over an arbitrary field.
• TauCeti.Place.exists_isWeierstrassCoordinates_isElliptic_of_genus_eq_one: over a perfect exact constant field, a genus-one function field has Weierstrass coordinates for an elliptic curve at every place of degree one.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Proposition 6.1.2.
• J. H. Silverman, The Arithmetic of Elliptic Curves, 2nd ed., Springer, 2009, Proposition III.1.4.

theorem TauCeti.Place.IsWeierstrassCoordinates.adjoin_div_eq_top_of_isSingular {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {P : Place k F} {W : WeierstrassCurve k} {x y : F} (h : P.IsWeierstrassCoordinates W x y) (hF : IsFunctionField k F) (hP : P.degree = 1) {x₀ y₀ : k} (hs : W.toAffine.IsSingular x₀ y₀) : k⟮(y - (algebraMap k F) y₀) / (x - (algebraMap k F) x₀)⟯ = ⊤

At a rational singular point the slope generates the function field: if (x₀, y₀) is a singular point of W over k, then F = k(z) for z = (y - y₀) / (x - x₀).

theorem TauCeti.Place.IsWeierstrassCoordinates.genus_eq_zero_of_isSingular {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {P : Place k F} {W : WeierstrassCurve k} {x y : F} (h : P.IsWeierstrassCoordinates W x y) (hF : IsFunctionField k F) (hP : P.degree = 1) {x₀ y₀ : k} (hs : W.toAffine.IsSingular x₀ y₀) : genus k F = 0

A Weierstrass equation with a rational singular point defines a rational function field: if W has a singular point over k, then F has genus zero.

theorem TauCeti.Place.IsWeierstrassCoordinates.isElliptic {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {P : Place k F} {W : WeierstrassCurve k} {x y : F} (h : P.IsWeierstrassCoordinates W x y) [PerfectField k] (hF : IsFunctionField k F) (hP : P.degree = 1) (hg : genus k F ≠ 0) : W.IsElliptic

The Weierstrass curve of a function field of nonzero genus is elliptic, over a perfect field.

theorem TauCeti.Place.IsWeierstrassCoordinates.squarefree_of_isCharNeTwoNF {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {P : Place k F} {W : WeierstrassCurve k} {x y : F} (h : P.IsWeierstrassCoordinates W x y) [W.IsCharNeTwoNF] (hF : IsFunctionField k F) (hP : P.degree = 1) (hg : genus k F ≠ 0) : Squarefree (Polynomial.X ^ 3 + Polynomial.C W.a₂ * Polynomial.X ^ 2 + Polynomial.C W.a₄ * Polynomial.X + Polynomial.C W.a₆)

The nonsingularity condition of the normal form Y² = X³ + a₂X² + a₄X + a₆: for a function field of nonzero genus the cubic is squarefree, over an arbitrary field.

theorem TauCeti.Place.IsWeierstrassCoordinates.a₆_ne_zero_of_isCharTwoJNeZeroNF {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {P : Place k F} {W : WeierstrassCurve k} {x y : F} (h : P.IsWeierstrassCoordinates W x y) [W.IsCharTwoJNeZeroNF] (hF : IsFunctionField k F) (hP : P.degree = 1) (hg : genus k F ≠ 0) : W.a₆ ≠ 0

The nonsingularity condition of the normal form Y² + XY = X³ + a₂X² + a₆: for a function field of nonzero genus, a₆ ≠ 0, over an arbitrary field.

theorem TauCeti.Place.exists_isWeierstrassCoordinates_isElliptic_of_genus_eq_one {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] [PerfectField k] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hg : genus k F = 1) {P : Place k F} (hP : P.degree = 1) : ∃ (W : WeierstrassCurve k) (x : F) (y : F), W.IsElliptic ∧ P.IsWeierstrassCoordinates W x y

Nonsingular Weierstrass coordinates (Stichtenoth, Proposition 6.1.2): over a perfect exact constant field, at every place of degree one of a genus-one function field there are Weierstrass coordinates for an elliptic curve.

theorem TauCeti.IsEllipticFunctionField.exists_isWeierstrassCoordinates_isElliptic {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] [PerfectField k] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (he : IsEllipticFunctionField k F) : ∃ (P : Place k F) (W : WeierstrassCurve k) (x : F) (y : F), P.degree = 1 ∧ W.IsElliptic ∧ P.IsWeierstrassCoordinates W x y

An elliptic function field over a perfect exact constant field has a place of degree one with Weierstrass coordinates for an elliptic curve.