The second Bosma–Lenstra addition law on a projective Weierstrass curve

Bosma and Lenstra attach to each line aX + bY + cZ = 0 in ℙ² an addition law of bidegree (2, 2) on a Weierstrass curve: a triple of polynomials in two point representatives P and Q that represents P + Q unless P - Q lies on the line, in which case all three vanish. The laws attached to two lines meeting off the curve therefore form a complete system.

Mathlib's WeierstrassCurve.Projective.addXYZ is, up to a constant factor, the law attached to the line Z = 0, which meets the curve only at the point at infinity; it vanishes on the diagonal (WeierstrassCurve.Projective.addXYZ_self). This file defines the law attached to the line Y = 0, which meets the line Z = 0 at (1 : 0 : 0), a point not on the curve. Its coordinates are given as explicit polynomials in the coefficients of the curve and the coordinates of P and Q. On the curve its diagonal is the doubling formula, so its coordinates are named dblAddX, dblAddY and dblAddZ.

Main definitions

• WeierstrassCurve.Projective.dblAddX, dblAddY, dblAddZ: the coordinates of the addition law attached to the line Y = 0.
• WeierstrassCurve.Projective.dblAddXYZ: the triple of these coordinates.

Main results

• WeierstrassCurve.Projective.dblAddXYZ_smul: the law is bihomogeneous of bidegree (2, 2).
• WeierstrassCurve.Projective.dblAddXYZ_self: on the curve, the diagonal of the law is Mathlib's doubling formula dblXYZ.
• WeierstrassCurve.Projective.addX_mul_dblAddY, addX_mul_dblAddZ, addY_mul_dblAddZ and addXYZ_cross_dblAddXYZ: for two point representatives on the curve, the 2 × 2 minors of the matrix with rows addXYZ P Q and dblAddXYZ P Q vanish, that is, the cross product of the two rows is zero.
• WeierstrassCurve.Projective.equation_dblAddXYZ_of_nonsingular: over a field, the law takes two nonsingular point representatives to a solution of the Weierstrass equation.
• WeierstrassCurve.Projective.addXYZ_ne_zero_or_dblAddXYZ_ne_zero: over a field, the laws addXYZ and dblAddXYZ do not vanish simultaneously at two nonsingular point representatives, which is the non-vanishing condition for the two laws to form a complete system.
• WeierstrassCurve.Projective.add_of_addXYZ_ne_zero and WeierstrassCurve.Projective.dblAddXYZ_equiv_add: a nonzero value of either law represents the sum add P Q, the second over a field and at nonsingular point representatives.
• WeierstrassCurve.Projective.map_dblAddXYZ: the law commutes with ring homomorphisms.
• WeierstrassCurve.Projective.span_range_addXYZ_union_range_dblAddXYZ_eq_top: over a commutative ring, at two unimodular solutions of the equation of an elliptic curve, the six coordinates of addXYZ and dblAddXYZ generate the unit ideal.

References

• W. Bosma and H. W. Lenstra, Jr., Complete systems of two addition laws for elliptic curves, J. Number Theory 53 (1995), 229–240: Theorem 2, the remark following it, and §5.

Provenance

Ported from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit c3415f32a313e19ace43e05479aeaa0d56ca287a, directory projects/ModularCurves/ModularCurves/EllipticCurve/:

• from AdditionLaw.lean: dblAddX, dblAddY, dblAddZ, dblAddXYZ, their _smul and _self lemmas, addX_mul_dblAddY, addX_mul_dblAddZ and addY_mul_dblAddZ. Statements and polynomials are those of the source; each polynomial is regrouped by the monomials in the coordinates of one of the two points. The XZ certificate is the source's. The XY and YZ minors are instead reduced to minors involving negY (dblAddXYZ P Q), whose certificates are linear combinations of the source's.
• from AdditionLawField.lean: equation_dblAddXYZ (as equation_dblAddXYZ_of_nonsingular) and addXYZ_ne_zero_or_dblAddXYZ_ne_zero. The source's proportionality lemma for vectors with vanishing 2 × 2 minors is replaced by Mathlib's Projectivization.mk_eq_mk_iff_crossProduct_eq_zero, through addXYZ_cross_dblAddXYZ.
• from AdditionLawOnCurve.lean: map_dblAddX, map_dblAddY, map_dblAddZ and map_dblAddXYZ, and map_addXYZ_ne_zero_or_map_dblAddXYZ_ne_zero, within span_range_addXYZ_union_range_dblAddXYZ_eq_top.
• from AdditionChartDomain.lean: span_lawOneTriple_union_lawTwoTriple_eq_top, as span_range_addXYZ_union_range_dblAddXYZ_eq_top. The source states it at the universal points of a product of two charts; here the points are arbitrary solutions whose coordinates generate the unit ideal.
• from AdditionSpecPoints.lean: descended_lawOne_eq_add and descended_lawTwo_smul_add, as add_of_addXYZ_ne_zero and dblAddXYZ_equiv_add. The source states them at the images in a field of the universal points of a product of two charts, the second as an equality up to a nonzero scalar; here the points are arbitrary representatives (nonsingular, for the second), and the first holds over any commutative ring.

The addition law attached to the line Y = 0

def WeierstrassCurve.Projective.dblAddX {R : Type u_1} [CommRing R] (W' : Projective R) (P Q : Fin 3 → R) : R

The X-coordinate of the addition law attached to the line Y = 0, evaluated at two projective point representatives P and Q on a Weierstrass curve. On the curve, its diagonal is dblX (dblAddX_self).

With P = (X₁ : Y₁ : Z₁) and Q = (X₂ : Y₂ : Z₂), the a₃a₄ term of this polynomial, viewed as a polynomial in the curve coefficients, is -a₃a₄(2X₁Z₂ + X₂Z₁)X₂Z₁, as printed in Bosma–Lenstra, p. 237.

Equations

• One or more equations did not get rendered due to their size.

def WeierstrassCurve.Projective.dblAddY {R : Type u_1} [CommRing R] (W' : Projective R) (P Q : Fin 3 → R) : R

The Y-coordinate of the addition law attached to the line Y = 0, evaluated at two projective point representatives P and Q on a Weierstrass curve. On the curve, its diagonal is dblY (dblAddY_self).

Equations

• One or more equations did not get rendered due to their size.

def WeierstrassCurve.Projective.dblAddZ {R : Type u_1} [CommRing R] (W' : Projective R) (P Q : Fin 3 → R) : R

The Z-coordinate of the addition law attached to the line Y = 0, evaluated at two projective point representatives P and Q on a Weierstrass curve. On the curve, its diagonal is dblZ (dblAddZ_self).

Equations

• One or more equations did not get rendered due to their size.

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

The coordinates of the addition law attached to the line Y = 0, evaluated at two projective point representatives P and Q on a Weierstrass curve. On the curve, its diagonal is dblXYZ (dblAddXYZ_self).

Equations

• W'.dblAddXYZ P Q = ![W'.dblAddX P Q, W'.dblAddY P Q, W'.dblAddZ P Q]

@[simp]

theorem WeierstrassCurve.Projective.dblAddXYZ_X {R : Type u_1} [CommRing R] {W' : Projective R} (P Q : Fin 3 → R) : W'.dblAddXYZ P Q 0 = W'.dblAddX P Q

The X-coordinate of dblAddXYZ P Q is dblAddX P Q.

@[simp]

theorem WeierstrassCurve.Projective.dblAddXYZ_Y {R : Type u_1} [CommRing R] {W' : Projective R} (P Q : Fin 3 → R) : W'.dblAddXYZ P Q 1 = W'.dblAddY P Q

The Y-coordinate of dblAddXYZ P Q is dblAddY P Q.

@[simp]

theorem WeierstrassCurve.Projective.dblAddXYZ_Z {R : Type u_1} [CommRing R] {W' : Projective R} (P Q : Fin 3 → R) : W'.dblAddXYZ P Q 2 = W'.dblAddZ P Q

The Z-coordinate of dblAddXYZ P Q is dblAddZ P Q.

Bihomogeneity

theorem WeierstrassCurve.Projective.dblAddX_smul {R : Type u_1} [CommRing R] {W' : Projective R} (P Q : Fin 3 → R) (u v : R) : W'.dblAddX (u • P) (v • Q) = (u * v) ^ 2 * W'.dblAddX P Q

The X-coordinate of the addition law attached to the line Y = 0 is bihomogeneous of bidegree (2, 2).

theorem WeierstrassCurve.Projective.dblAddY_smul {R : Type u_1} [CommRing R] {W' : Projective R} (P Q : Fin 3 → R) (u v : R) : W'.dblAddY (u • P) (v • Q) = (u * v) ^ 2 * W'.dblAddY P Q

The Y-coordinate of the addition law attached to the line Y = 0 is bihomogeneous of bidegree (2, 2).

theorem WeierstrassCurve.Projective.dblAddZ_smul {R : Type u_1} [CommRing R] {W' : Projective R} (P Q : Fin 3 → R) (u v : R) : W'.dblAddZ (u • P) (v • Q) = (u * v) ^ 2 * W'.dblAddZ P Q

The Z-coordinate of the addition law attached to the line Y = 0 is bihomogeneous of bidegree (2, 2).

theorem WeierstrassCurve.Projective.dblAddXYZ_smul {R : Type u_1} [CommRing R] {W' : Projective R} (P Q : Fin 3 → R) (u v : R) : W'.dblAddXYZ (u • P) (v • Q) = (u * v) ^ 2 • W'.dblAddXYZ P Q

The addition law attached to the line Y = 0 is bihomogeneous of bidegree (2, 2): rescaling the representatives P and Q by u and v rescales its value by (u * v) ^ 2.

The diagonal is the doubling formula

theorem WeierstrassCurve.Projective.dblAddX_self {R : Type u_1} [CommRing R] {W' : Projective R} {P : Fin 3 → R} (hP : W'.Equation P) : W'.dblAddX P P = W'.dblX P

On the curve, the X-coordinate of the addition law attached to the line Y = 0 agrees on the diagonal with the X-coordinate dblX of Mathlib's doubling formula.

theorem WeierstrassCurve.Projective.dblAddY_self {R : Type u_1} [CommRing R] {W' : Projective R} {P : Fin 3 → R} (hP : W'.Equation P) : W'.dblAddY P P = W'.dblY P

On the curve, the Y-coordinate of the addition law attached to the line Y = 0 agrees on the diagonal with the Y-coordinate dblY of Mathlib's doubling formula.

theorem WeierstrassCurve.Projective.dblAddZ_self {R : Type u_1} [CommRing R] {W' : Projective R} {P : Fin 3 → R} (hP : W'.Equation P) : W'.dblAddZ P P = W'.dblZ P

On the curve, the Z-coordinate of the addition law attached to the line Y = 0 agrees on the diagonal with the Z-coordinate dblZ of Mathlib's doubling formula.

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

On the curve, the diagonal of the addition law attached to the line Y = 0 is Mathlib's doubling formula dblXYZ.

The two laws are proportional on the curve

theorem WeierstrassCurve.Projective.addX_mul_dblAddZ {R : Type u_1} [CommRing R] {W' : Projective R} {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) : W'.addX P Q * W'.dblAddZ P Q = W'.addZ P Q * W'.dblAddX P Q

For two point representatives on the curve, the XZ minor of the matrix with rows addXYZ P Q and dblAddXYZ P Q vanishes.

theorem WeierstrassCurve.Projective.addX_mul_dblAddY {R : Type u_1} [CommRing R] {W' : Projective R} {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) : W'.addX P Q * W'.dblAddY P Q = W'.addY P Q * W'.dblAddX P Q

For two point representatives on the curve, the XY minor of the matrix with rows addXYZ P Q and dblAddXYZ P Q vanishes.

theorem WeierstrassCurve.Projective.addY_mul_dblAddZ {R : Type u_1} [CommRing R] {W' : Projective R} {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) : W'.addY P Q * W'.dblAddZ P Q = W'.addZ P Q * W'.dblAddY P Q

For two point representatives on the curve, the YZ minor of the matrix with rows addXYZ P Q and dblAddXYZ P Q vanishes.

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

For two point representatives on the curve, the cross product of addXYZ P Q and dblAddXYZ P Q vanishes; equivalently, the three 2 × 2 minors of the matrix with these rows vanish (addX_mul_dblAddY, addX_mul_dblAddZ, addY_mul_dblAddZ). Over a field, when both vectors are nonzero, this means that they represent the same point of ℙ² (Projectivization.mk_eq_mk_iff_crossProduct_eq_zero).

theorem WeierstrassCurve.Projective.add_of_addXYZ_ne_zero {R : Type u_1} [CommRing R] {W' : Projective R} {P Q : Fin 3 → R} (h : W'.addXYZ P Q ≠ 0) : W'.add P Q = W'.addXYZ P Q

If the addition law addXYZ attached to the line Z = 0 does not vanish at two point representatives P and Q, then its value addXYZ P Q is their sum add P Q. Unlike dblAddXYZ_equiv_add for the law attached to Y = 0, this is an equality rather than an equivalence, and it holds over any commutative ring, for representatives not necessarily on the curve.

Over a field

theorem WeierstrassCurve.Projective.dblAddXYZ_equiv_add {F : Type u_2} [Field F] {W : Projective F} {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) (hd : W.dblAddXYZ P Q ≠ 0) : W.dblAddXYZ P Q ≈ W.add P Q

Over a field, a nonzero value of the addition law dblAddXYZ P Q attached to the line Y = 0, at two nonsingular point representatives P and Q, represents their sum add P Q. For the law addXYZ attached to the line Z = 0, a nonzero value is equal to add P Q, over any commutative ring and at any point representatives (add_of_addXYZ_ne_zero).

theorem WeierstrassCurve.Projective.equation_dblAddXYZ_of_nonsingular {F : Type u_2} [Field F] {W : Projective F} {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) : W.Equation (W.dblAddXYZ P Q)

Over a field, the value of the addition law attached to the line Y = 0 at two nonsingular point representatives satisfies the Weierstrass equation. For solutions over an arbitrary commutative ring, see WeierstrassCurve.Projective.Equation.dblAddXYZ.

theorem WeierstrassCurve.Projective.addXYZ_ne_zero_or_dblAddXYZ_ne_zero {F : Type u_2} [Field F] {W : Projective F} {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) : W.addXYZ P Q ≠ 0 ∨ W.dblAddXYZ P Q ≠ 0

Over a field, the addition laws addXYZ and dblAddXYZ, attached to the lines Z = 0 and Y = 0, do not vanish simultaneously at two nonsingular point representatives. This is the non-vanishing condition in the definition of a complete system of addition laws; that the two values are linearly dependent is addXYZ_cross_dblAddXYZ.

Maps

@[simp]

theorem WeierstrassCurve.Projective.map_dblAddX {R : Type u_1} [CommRing R] {W' : Projective R} {S : Type u_2} [CommRing S] (f : R →+* S) (P Q : Fin 3 → R) : (W'.map f).dblAddX (⇑f ∘ P) (⇑f ∘ Q) = f (W'.dblAddX P Q)

The X-coordinate of the addition law attached to the line Y = 0 commutes with a ring homomorphism applied to the coefficients of the curve and to the point representatives.

@[simp]

theorem WeierstrassCurve.Projective.map_dblAddY {R : Type u_1} [CommRing R] {W' : Projective R} {S : Type u_2} [CommRing S] (f : R →+* S) (P Q : Fin 3 → R) : (W'.map f).dblAddY (⇑f ∘ P) (⇑f ∘ Q) = f (W'.dblAddY P Q)

The Y-coordinate of the addition law attached to the line Y = 0 commutes with a ring homomorphism applied to the coefficients of the curve and to the point representatives.

@[simp]

theorem WeierstrassCurve.Projective.map_dblAddZ {R : Type u_1} [CommRing R] {W' : Projective R} {S : Type u_2} [CommRing S] (f : R →+* S) (P Q : Fin 3 → R) : (W'.map f).dblAddZ (⇑f ∘ P) (⇑f ∘ Q) = f (W'.dblAddZ P Q)

The Z-coordinate of the addition law attached to the line Y = 0 commutes with a ring homomorphism applied to the coefficients of the curve and to the point representatives.

@[simp]

theorem WeierstrassCurve.Projective.map_dblAddXYZ {R : Type u_1} [CommRing R] {W' : Projective R} {S : Type u_2} [CommRing S] (f : R →+* S) (P Q : Fin 3 → R) : (W'.map f).dblAddXYZ (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W'.dblAddXYZ P Q

The addition law attached to the line Y = 0 commutes with a ring homomorphism applied to the coefficients of the curve and to the point representatives.

Non-vanishing over a ring

theorem WeierstrassCurve.Projective.span_range_addXYZ_union_range_dblAddXYZ_eq_top {R : Type u_1} [CommRing R] {W' : Projective R} [WeierstrassCurve.IsElliptic W'] {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hP₁ : Module.IsUnimodular R P) (hQ₁ : Module.IsUnimodular R Q) : Ideal.span (Set.range (W'.addXYZ P Q) ∪ Set.range (W'.dblAddXYZ P Q)) = ⊤

Let P and Q be unimodular solutions of the Weierstrass equation of an elliptic curve over a commutative ring. Then the six coordinates of the two addition laws addXYZ P Q and dblAddXYZ P Q generate the unit ideal; equivalently, at every prime ideal, some coordinate of one of the two laws does not vanish. The analogue over a field, for nonsingular point representatives, is addXYZ_ne_zero_or_dblAddXYZ_ne_zero.