Normal forms of genus-one function fields

When two is invertible in the constant field, completing the square puts the Weierstrass equation supplied by Riemann–Roch in the form Y² = X³ + a₂X² + a₄X + a₆. The coordinate change preserves the pole orders two and three at the chosen rational place, so the resulting coordinates still generate the function field. The change of the Weierstrass curve itself is Mathlib's WeierstrassCurve.toCharNeTwoNF.

In characteristic two, Mathlib's WeierstrassCurve.toCharTwoNF gives either Y² + XY = X³ + a₂X² + a₆ or Y² + a₃Y = X³ + a₄X + a₆. Transport under an admissible variable change preserves the same pole orders, so these normal forms also have coordinates that generate the function field. These statements concern equations and pole orders; nonsingularity is a separate assertion.

These are the normal-form coordinate changes of Stichtenoth, Proposition 6.1.2.

References

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

theorem TauCeti.Place.IsWeierstrassCoordinates.toCharNeTwoNF {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) (h2 : 2 ≠ 0) : P.IsWeierstrassCoordinates (W.toCharNeTwoNF • W) x (y + (algebraMap k F) (W.a₁ / 2) * x + (algebraMap k F) (W.a₃ / 2))

Completing the square in Weierstrass coordinates preserves the pole orders and gives Mathlib's characteristic-not-two normal form.

theorem TauCeti.Place.exists_isWeierstrassCoordinates_isCharNeTwoNF_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) (h2 : 2 ≠ 0) {P : Place k F} (hP : P.degree = 1) : ∃ (W : WeierstrassCurve k) (x : F) (y : F), W.IsCharNeTwoNF ∧ P.IsWeierstrassCoordinates W x y

At every degree-one place of a genus-one function field in characteristic other than two, there are Weierstrass coordinates in the normal form Y² = X³ + a₂X² + a₄X + a₆. Their pole orders are two and three, so they generate the function field.

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

At every degree-one place of a genus-one function field in characteristic two, there are Weierstrass coordinates in one of Mathlib's two characteristic-two normal forms. Their pole orders are two and three, so they generate the function field.

theorem TauCeti.IsEllipticFunctionField.exists_isWeierstrassCoordinates_isCharNeTwoNF {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) (h2 : 2 ≠ 0) : ∃ (P : Place k F) (W : WeierstrassCurve k) (x : F) (y : F), P.degree = 1 ∧ W.IsCharNeTwoNF ∧ P.IsWeierstrassCoordinates W x y

An elliptic function field in characteristic other than two has a rational place with Weierstrass coordinates in the form Y² = X³ + a₂X² + a₄X + a₆.

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

An elliptic function field in characteristic two has a rational place with Weierstrass coordinates in the form Y² + XY = X³ + a₂X² + a₆ or Y² + a₃Y = X³ + a₄X + a₆.