Functions on the affine curve with a pole of order at most three

Let W be a Weierstrass curve over a field F, with coordinate ring R[W] and coordinate functions x and y. Every element of R[W] is p(x) + q(x) y for polynomials p and q, and at the place at infinity the two summands have pole orders 2 deg p and 2 deg q + 3, of different parities. So the pole orders of the elements of R[W] are 0, 2, 3, 4, …, and the elements of small pole order are explicit:

• an element with a pole at infinity has a pole of order at least two;
• an element with a pole of order less than three is αx + β;
• an element with a pole of order at most three is γy + αx + β.

These are the computations L(2O) = ⟨1, x⟩ and L(3O) = ⟨1, x, y⟩ behind the proof that an isomorphism of elliptic curves fixing the point at infinity is a change of variables. They are stated for any valuation v of the function field that is trivial on F and gives x a pole, so that they apply to a valuation transported along a map of function fields before that map is known to identify the places at infinity. For the place at infinity itself and an elliptic curve, the spaces L(n · O) are computed in full in Affine/FunctionField/Genus.lean.

Main results

• WeierstrassCurve.Affine.val_mk_Y_lt_val_X_sq: v y < (v x) ^ 2.
• WeierstrassCurve.Affine.val_X_le_of_one_lt: 1 < v z implies v x ≤ v z.
• WeierstrassCurve.Affine.exists_eq_of_val_lt_val_mk_Y: v z < v y implies z = αx + β.
• WeierstrassCurve.Affine.exists_eq_of_val_le_val_mk_Y: v z ≤ v y implies z = γy + αx + β.

References

• J. Silverman, The Arithmetic of Elliptic Curves, the proof of III.3.1.

theorem WeierstrassCurve.Affine.val_mk_Y_lt_val_X_sq {F : Type u_1} [Field F] {W : Affine F} {Γ : Type u_2} [LinearOrderedCommGroupWithZero Γ] (v : Valuation W.FunctionField Γ) [Valuation.IsTrivialOn F v] (hx : 1 < v ((algebraMap (Polynomial F) W.FunctionField) Polynomial.X)) : v ((algebraMap W.CoordinateRing W.FunctionField) ((CoordinateRing.mk W) Polynomial.X)) < v ((algebraMap (Polynomial F) W.FunctionField) Polynomial.X) ^ 2

y has a pole of order less than twice that of x: v y < (v x) ^ 2, since (v y) ^ 2 = (v x) ^ 3.

theorem WeierstrassCurve.Affine.val_X_le_of_one_lt {F : Type u_1} [Field F] {W : Affine F} {Γ : Type u_2} [LinearOrderedCommGroupWithZero Γ] (v : Valuation W.FunctionField Γ) [Valuation.IsTrivialOn F v] (hx : 1 < v ((algebraMap (Polynomial F) W.FunctionField) Polynomial.X)) {z : W.CoordinateRing} (hz : 1 < v ((algebraMap W.CoordinateRing W.FunctionField) z)) : v ((algebraMap (Polynomial F) W.FunctionField) Polynomial.X) ≤ v ((algebraMap W.CoordinateRing W.FunctionField) z)

No function on the affine curve has a pole of order one at infinity: if z has a pole, its pole is at least that of x.

theorem WeierstrassCurve.Affine.exists_eq_of_val_lt_val_mk_Y {F : Type u_1} [Field F] {W : Affine F} {Γ : Type u_2} [LinearOrderedCommGroupWithZero Γ] (v : Valuation W.FunctionField Γ) [Valuation.IsTrivialOn F v] (hx : 1 < v ((algebraMap (Polynomial F) W.FunctionField) Polynomial.X)) {z : W.CoordinateRing} (hz : v ((algebraMap W.CoordinateRing W.FunctionField) z) < v ((algebraMap W.CoordinateRing W.FunctionField) ((CoordinateRing.mk W) Polynomial.X))) : ∃ (α : F) (β : F), z = (algebraMap F W.CoordinateRing) α * (AdjoinRoot.of W.polynomial) Polynomial.X + (algebraMap F W.CoordinateRing) β

A function on the affine curve with a pole of order less than three is αx + β: if v z < v y, then z = αx + β for constants α and β.

theorem WeierstrassCurve.Affine.exists_eq_of_val_le_val_mk_Y {F : Type u_1} [Field F] {W : Affine F} {Γ : Type u_2} [LinearOrderedCommGroupWithZero Γ] (v : Valuation W.FunctionField Γ) [Valuation.IsTrivialOn F v] (hx : 1 < v ((algebraMap (Polynomial F) W.FunctionField) Polynomial.X)) {z : W.CoordinateRing} (hz : v ((algebraMap W.CoordinateRing W.FunctionField) z) ≤ v ((algebraMap W.CoordinateRing W.FunctionField) ((CoordinateRing.mk W) Polynomial.X))) : ∃ (α : F) (β : F) (γ : F), z = (algebraMap F W.CoordinateRing) γ * AdjoinRoot.root W.polynomial + (algebraMap F W.CoordinateRing) α * (AdjoinRoot.of W.polynomial) Polynomial.X + (algebraMap F W.CoordinateRing) β

A function on the affine curve with a pole of order at most three is γy + αx + β: if v z ≤ v y, then z = γy + αx + β for constants α, β and γ.