The function with divisor n(T) - n(O) at an n-torsion point

The sum of (T) - (O) is T, so the sum of n(T) - n(O) is n • T, and a degree-zero divisor is principal exactly when its sum is O. At an n-torsion point, therefore, n(T) - n(O) is principal.

This is the first input to the divisor construction of the Weil pairing (Silverman III.8): the pairing is built from such a function together with a second one whose n-th power is its pullback along [n].

Main results

• WeierstrassCurve.Affine.exists_principal_eq_zsmul_ofPoint_sub_infinity: at an n-torsion point T, the divisor n(T) - n(O) is the divisor of a function.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.8.1.
• H. Stichtenoth, Algebraic Function Fields and Codes, I.4.

theorem WeierstrassCurve.Affine.exists_principal_eq_zsmul_ofPoint_sub_infinity {F : Type u_1} [Field F] (W : Affine F) [IsDedekindDomain W.CoordinateRing] [DecidableEq F] [WeierstrassCurve.IsElliptic W] {n : ℤ} {T : W.Point} (hT : n • T = 0) : ∃ (z : W.FunctionFieldˣ), TauCeti.Divisor.principal ⋯ z = n • (TauCeti.AlgebraicGeometry.WeilDivisor.ofPoint ↑(W.pointEquivDegreeOnePlace T) - TauCeti.AlgebraicGeometry.WeilDivisor.ofPoint (TauCeti.Place.infinity W))

At an n-torsion point, n(T) - n(O) is the divisor of a function (Silverman III.8.1).