The sum of a degree-zero divisor as a point

A degree-zero divisor of F(W) has a divisor class, and Divisor/Class.lean identifies the degree-zero classes with the points of W. Composing the two gives the sum map σ, which reads a degree-zero divisor as a point, and the principal divisors are exactly those it sends to O.

That last statement is the principal-divisor characterisation: Σ nᵢ (Pᵢ) is the divisor of a function exactly when Σ nᵢ = 0 and Σ [nᵢ] Pᵢ = O. It is where the divisor calculus meets the group law, and it is the existence criterion the divisor construction of the Weil pairing uses to produce its functions.

Main definitions

• WeierstrassCurve.Affine.divisorSum: the sum of a degree-zero divisor, as a point of W. It is TauCeti.Divisor.degreeZeroClassHom followed by the identification of the degree-zero classes with the points.

Main results

• WeierstrassCurve.Affine.divisorSum_pointPlace_sub_infinity: σ((P) - (O)) = P, the computation rule that fixes divisorSum on the divisors it is read off from.
• WeierstrassCurve.Affine.divisorSum_ofPoint_sub_ofPoint: σ((P) - (Q)) = P - Q, read through the point--place dictionary.
• WeierstrassCurve.Affine.divisorSum_eq_zero_iff: a degree-zero divisor is principal exactly when its sum is O.
• WeierstrassCurve.Affine.exists_principal_eq_ofPoint_add_sub: the divisor (P + Q) - (P) - ((Q) - (O)) is principal; a function with this divisor is the reciprocal of Miller's addition function for P and Q.

References

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

Provenance

The principality criterion was previously formalized in the AINTLIB HasseWeil project (Chris Birkbeck), Apache-2.0, at commit a302aeacd86053f9d5f991fbbf664e1cc1051d08, as projIsPrincipal_of_degZero_of_sigma_eq_zero and its torsion specialization weilFunction_exists, both in projects/HasseWeil/HasseWeil/HasseBound/WeilPairing/WeilFunction.lean. Those are stated for the projective divisors of a smooth plane curve and are derived from a linear-equivalence reduction D ∼ (σD) - (O); divisorSum_eq_zero_iff below is the function-field statement, obtained from the degree-zero class group instead.

noncomputable def WeierstrassCurve.Affine.divisorSum {F : Type u_1} [Field F] (W : Affine F) [IsDedekindDomain W.CoordinateRing] [DecidableEq F] : ↥TauCeti.Divisor.degree.ker →+ W.Point

The sum of a degree-zero divisor, as a point of W: the point whose class is the class of the divisor. On (P) - (O) it is P, and it is additive, so on Σ nᵢ (Pᵢ) it is Σ [nᵢ] Pᵢ.

Equations

• W.divisorSum = W.pointEquivDegreeZeroDivisorClass.symm.toAddMonoidHom.comp (TauCeti.Divisor.degreeZeroClassHom ⋯)

theorem WeierstrassCurve.Affine.divisorSum_apply {F : Type u_1} [Field F] (W : Affine F) [IsDedekindDomain W.CoordinateRing] [DecidableEq F] (D : ↥TauCeti.Divisor.degree.ker) : W.divisorSum D = W.pointEquivDegreeZeroDivisorClass.symm ((TauCeti.Divisor.degreeZeroClassHom ⋯) D)

The defining formula for divisorSum: the degree-zero class map, read back as a point.

Not @[simp]: the characterisation divisorSum_eq_zero_iff below is the simp form, and unfolding the composite first would keep it from firing.

@[simp]

theorem WeierstrassCurve.Affine.divisorSum_pointPlace_sub_infinity {F : Type u_1} [Field F] (W : Affine F) [IsDedekindDomain W.CoordinateRing] [DecidableEq F] {x y : F} (h : W.Nonsingular x y) : W.divisorSum ⟨TauCeti.AlgebraicGeometry.WeilDivisor.ofPoint (TauCeti.Place.ofPrime F W.FunctionField (CoordinateRing.pointPlace ⋯)) - TauCeti.AlgebraicGeometry.WeilDivisor.ofPoint (TauCeti.Place.infinity W), ⋯⟩ = Point.some x y h

σ((P) - (O)) = P.

@[simp]

theorem WeierstrassCurve.Affine.divisorSum_eq_zero_iff {F : Type u_1} [Field F] (W : Affine F) [IsDedekindDomain W.CoordinateRing] [DecidableEq F] {D : ↥TauCeti.Divisor.degree.ker} : W.divisorSum D = 0 ↔ ∃ (z : W.FunctionFieldˣ), TauCeti.Divisor.principal ⋯ z = ↑D

A degree-zero divisor is principal exactly when its sum is O (Silverman III.3.5).

theorem WeierstrassCurve.Affine.ofPoint_sub_ofPoint_mem_ker_degree {F : Type u_1} [Field F] (W : Affine F) [WeierstrassCurve.IsElliptic W] (P Q : W.Point) : TauCeti.AlgebraicGeometry.WeilDivisor.ofPoint ↑(W.pointEquivDegreeOnePlace P) - TauCeti.AlgebraicGeometry.WeilDivisor.ofPoint ↑(W.pointEquivDegreeOnePlace Q) ∈ TauCeti.Divisor.degree.ker

The divisor (P) - (Q) of two points has degree zero.

@[simp]

theorem WeierstrassCurve.Affine.divisorSum_ofPoint_sub_ofPoint {F : Type u_1} [Field F] (W : Affine F) [IsDedekindDomain W.CoordinateRing] [DecidableEq F] [WeierstrassCurve.IsElliptic W] (P Q : W.Point) : W.divisorSum ⟨TauCeti.AlgebraicGeometry.WeilDivisor.ofPoint ↑(W.pointEquivDegreeOnePlace P) - TauCeti.AlgebraicGeometry.WeilDivisor.ofPoint ↑(W.pointEquivDegreeOnePlace Q), ⋯⟩ = P - Q

σ((P) - (Q)) = P - Q, for the places the point--place dictionary attaches to P and Q.

theorem WeierstrassCurve.Affine.exists_principal_eq_ofPoint_add_sub {F : Type u_1} [Field F] (W : Affine F) [IsDedekindDomain W.CoordinateRing] [DecidableEq F] [WeierstrassCurve.IsElliptic W] (P Q : W.Point) : ∃ (z : W.FunctionFieldˣ), TauCeti.Divisor.principal ⋯ z = TauCeti.AlgebraicGeometry.WeilDivisor.ofPoint ↑(W.pointEquivDegreeOnePlace (P + Q)) - TauCeti.AlgebraicGeometry.WeilDivisor.ofPoint ↑(W.pointEquivDegreeOnePlace P) - (TauCeti.AlgebraicGeometry.WeilDivisor.ofPoint ↑(W.pointEquivDegreeOnePlace Q) - TauCeti.AlgebraicGeometry.WeilDivisor.ofPoint (TauCeti.Place.infinity W))

(P + Q) - (P) - ((Q) - (O)) is the divisor of a function, its sum being (P + Q) - P - Q = O (Silverman III.3.5). Such a function is the reciprocal v / ℓ of Miller's addition function ℓ / v, for ℓ the line through P and Q (the tangent line if P = Q) and v the vertical line through P + Q.