The Weierstrass equation of an elliptic function field

Let F / k be an algebraic function field of genus one with exact constant field, and let P be a place of degree one. Riemann–Roch gives ℓ(nP) = n for n ≥ 1, and this dimension ladder produces the classical Weierstrass coordinates at P: a function x with pole divisor 2P, a function y with pole divisor 3P, and a relation

y² + a₁xy + a₃y = x³ + a₂x² + a₄x + a₆, aᵢ ∈ k,

because the seven functions 1, x, y, x², xy, x³, y² lie in the six-dimensional space L(6P), and the coefficients of y² and x³ in the resulting relation are nonzero since these two are the only functions of the seven with a pole of order six. Since [F : k(x)] = 2 and [F : k(y)] = 3 are the degrees of the pole divisors, x and y generate F over k. This is the first half of Stichtenoth's Proposition 6.1.2; the normal forms in each characteristic are coordinate changes of this equation.

The relation is recorded as the affine equation of a Weierstrass curve W over k, evaluated in F along the base change W.baseChange F, so that Mathlib's Weierstrass-curve API (variable changes, the discriminant) applies to it.

Main definitions

• TauCeti.Place.IsWeierstrassCoordinates: x and y have pole divisors 2P and 3P and satisfy the Weierstrass equation of W.

Main results

• TauCeti.Place.IsWeierstrassCoordinates.finrank_adjoin_x_eq_two, TauCeti.Place.IsWeierstrassCoordinates.finrank_adjoin_y_eq_three and TauCeti.Place.IsWeierstrassCoordinates.adjoin_eq_top: [F : k(x)] = 2, [F : k(y)] = 3 and F = k(x, y).
• TauCeti.Place.exists_isWeierstrassCoordinates_of_genus_eq_one: a genus-one function field with exact constants has Weierstrass coordinates at every place of degree one (Stichtenoth, Proposition 6.1.2).
• TauCeti.IsEllipticFunctionField.exists_isWeierstrassCoordinates: the same for an elliptic function field, at some place of degree one.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Proposition 6.1.2.

structure TauCeti.Place.IsWeierstrassCoordinates {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) : Prop

Weierstrass coordinates at a place P for a Weierstrass curve W over k: functions x and y with pole divisors 2P and 3P satisfying the affine Weierstrass equation of W in F.

• ord_x : P.ord x = -2

  x has a pole of order two at P.

• ord_x_nonneg (Q : Place k F) : Q ≠ P → 0 ≤ Q.ord x

  x is regular away from P.

• ord_y : P.ord y = -3

  y has a pole of order three at P.

• ord_y_nonneg (Q : Place k F) : Q ≠ P → 0 ≤ Q.ord y

  y is regular away from P.

• equation : (W.baseChange F).toAffine.Equation x y

  (x, y) satisfies the Weierstrass equation of W, read in F.

theorem TauCeti.Place.IsWeierstrassCoordinates.x_ne_zero {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) : x ≠ 0

Weierstrass coordinates are nonzero: x has a pole.

theorem TauCeti.Place.IsWeierstrassCoordinates.y_ne_zero {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) : y ≠ 0

Weierstrass coordinates are nonzero: y has a pole.

theorem TauCeti.Place.IsWeierstrassCoordinates.transcendental_x {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) : Transcendental k x

x is transcendental over k, having a pole.

theorem TauCeti.Place.IsWeierstrassCoordinates.transcendental_y {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) : Transcendental k y

y is transcendental over k, having a pole.

theorem TauCeti.Place.IsWeierstrassCoordinates.poles_x {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) : Divisor.poles hF (Units.mk0 x ⋯) = 2 • AlgebraicGeometry.WeilDivisor.ofPoint P

The pole divisor of x is 2P.

theorem TauCeti.Place.IsWeierstrassCoordinates.poles_y {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) : Divisor.poles hF (Units.mk0 y ⋯) = 3 • AlgebraicGeometry.WeilDivisor.ofPoint P

The pole divisor of y is 3P.

theorem TauCeti.Place.IsWeierstrassCoordinates.finrank_adjoin_x_eq_two {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) : Module.finrank (↥k⟮x⟯) F = 2

[F : k(x)] = 2 at a place of degree one: the degree of the pole divisor of x.

theorem TauCeti.Place.IsWeierstrassCoordinates.finrank_adjoin_y_eq_three {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) : Module.finrank (↥k⟮y⟯) F = 3

[F : k(y)] = 3 at a place of degree one: the degree of the pole divisor of y.

theorem TauCeti.Place.IsWeierstrassCoordinates.adjoin_eq_top {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) : k⟮x, y⟯ = ⊤

Weierstrass coordinates generate the function field: F = k(x, y), because [F : k(x, y)] divides both [F : k(x)] = 2 and [F : k(y)] = 3.

theorem TauCeti.Place.exists_isWeierstrassCoordinates_of_genus_eq_one {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (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), P.IsWeierstrassCoordinates W x y

The Weierstrass equation of a genus-one function field (Stichtenoth, Proposition 6.1.2): over an exact constant field, at every place P of degree one there are functions x and y with pole divisors 2P and 3P satisfying the affine equation of a Weierstrass curve over k. By TauCeti.Place.IsWeierstrassCoordinates.adjoin_eq_top, they generate F over k.

theorem TauCeti.IsEllipticFunctionField.exists_isWeierstrassCoordinates {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (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 ∧ P.IsWeierstrassCoordinates W x y

The Weierstrass equation of an elliptic function field (Stichtenoth, Proposition 6.1.2): over an exact constant field, an elliptic function field has a place P of degree one and Weierstrass coordinates at P.