The Bosma–Lenstra addition laws land on the curve over any ring #

Let W' be a Weierstrass curve in projective coordinates over a commutative ring R, and let P and Q be solutions of its homogeneous equation. This file shows that the two Bosma–Lenstra addition laws attached to the lines Z = 0 and Y = 0, namely Mathlib's WeierstrassCurve.Projective.addXYZ and Tau Ceti's WeierstrassCurve.Projective.dblAddXYZ, take P and Q to solutions of the equation again. The curve W' is arbitrary, possibly singular, and P and Q are arbitrary solutions, not necessarily nonsingular and not necessarily with coordinates generating the unit ideal.

Main results #

WeierstrassCurve.Projective.Equation.addXYZ: if P and Q satisfy the equation of W', so does W'.addXYZ P Q.
WeierstrassCurve.Projective.Equation.dblAddXYZ: if P and Q satisfy the equation of W', so does W'.dblAddXYZ P Q.

References #

W. Bosma and H. W. Lenstra, Jr., Complete systems of two addition laws for elliptic curves, J. Number Theory 53 (1995), 229–240.

Provenance #

New in Tau Ceti; no code was ported. AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0, commit c3415f32a313e19ace43e05479aeaa0d56ca287a, file projects/ModularCurves/ModularCurves/EllipticCurve/AdditionLawOnCurve.lean) has the two statements as equation_addXYZ_of_isJacobsonRing and equation_dblAddXYZ_of_isJacobsonRing, for curves with unit discriminant over reduced Jacobson rings.

The universal pair of solutions #

The addition laws on the curve #

source

theorem WeierstrassCurve.Projective.Equation.addXYZ {R : Type u_1} [CommRing R] {W' : Projective R} {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) :

W'.Equation (W'.addXYZ P Q)

Mathlib's addition law addXYZ, attached to the line Z = 0, takes two solutions of the projective Weierstrass equation to a solution of the equation. This holds for every Weierstrass curve over every commutative ring, singular or not, and for all solutions P and Q.

source

theorem WeierstrassCurve.Projective.Equation.dblAddXYZ {R : Type u_1} [CommRing R] {W' : Projective R} {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) :

W'.Equation (W'.dblAddXYZ P Q)

The addition law dblAddXYZ, attached to the line Y = 0, takes two solutions of the projective Weierstrass equation to a solution of the equation. This holds for every Weierstrass curve over every commutative ring, singular or not, and for all solutions P and Q.