The addition-and-subtraction map on x-coordinates

We set up the endomorphism of ℙ² that on affine points with affine sum is equal to

(x(P) * x(Q) : x(P) + x(Q) : 1) ↦ (x(P+Q) * x(P-Q) : x(P+Q) + x(P-Q) : 1);

see WeierstrassCurve.addSubMap (this is on coordinate vectors).

TODO: Show that the map really does what it is claimed to do.

This will be used to eventually show the approximate parallelogram law for K-points on an elliptic curve E: ∃ C, ∀ P Q : E(K), |h(P+Q) + h(P-Q) - 2*h(P) - 2*h(Q)| ≤ C, where K is a field with a height and h denotes the (logarithmic) naïve height on E(K).

The addition-and-subtraction map on x-coordinates

noncomputable def WeierstrassCurve.addSubMap {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : Fin 3 → MvPolynomial (Fin 3) R

The polynomial map on coordinate vectors giving (x(P) * x(Q) : x(P) + x(Q) : 1) ↦ (x(P+Q) * x(P-Q) : x(P+Q) + x(P-Q) : 1) for points P, Q on the Weierstrass curve W.

Equations

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

noncomputable def WeierstrassCurve.addSubMapCoeff {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : Fin 3 × Fin 3 → MvPolynomial (Fin 3) R

The coefficient polynomials in linear combinations of the polynomials in addSubMap that result in the fourth powers of the variables, multiplied by W.Δ.

Equations

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

theorem WeierstrassCurve.isHomogeneous_addSubMap {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (i : Fin 3) : (W.addSubMap i).IsHomogeneous 2

theorem WeierstrassCurve.isHomogeneous_addSubMapCoeff {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (ij : Fin 3 × Fin 3) : (W.addSubMapCoeff ij).IsHomogeneous 2

theorem WeierstrassCurve.addSubMapCoeff_condition {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] (x : Fin 3 → R) (i : Fin 3) : ∑ j : Fin 3, (MvPolynomial.eval x) (MvPolynomial.C ↑W.Δ'⁻¹ * W.addSubMapCoeff (i, j)) * (MvPolynomial.eval x) (W.addSubMap j) = x i ^ 4

theorem WeierstrassCurve.addSubMap_ne_zero {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] [IsReduced R] {x : Fin 3 → R} (hx : x ≠ 0) : (fun (x_1 : Fin 3) => (MvPolynomial.eval x) (W.addSubMap x_1)) ≠ 0

The symmetric square of the x-coordinate map

We define Weierstrass.Affine.Point.sym2x, which sends a pair P, Q of nonsingular points in affine coordinates on a Weierstrass curve to a triple projectively equal to (x(P)*x(Q), x(P)+x(Q), 1), and provide some API.

noncomputable def WeierstrassCurve.Affine.Point.sym2x {R : Type u_1} [CommRing R] {W' : Affine R} (P Q : W'.Point) : Fin 3 → R

This map sends a pair P, Q of nonsingular points in affine coordinates on W to a triple projectively equivalent to ![x(P) * x(Q), x(P) + x(Q), 1].

In more geometric terms, this is the map Sym² W → Sym² ℙ¹ ≃ ℙ² induced by x : W → ℙ¹.

Equations

• P.sym2x Q = ![P.xRep 0 * Q.xRep 0, P.xRep 0 * Q.xRep 1 + P.xRep 1 * Q.xRep 0, P.xRep 1 * Q.xRep 1]

@[simp]

theorem WeierstrassCurve.Affine.Point.sym2x_zero_zero {R : Type u_1} [CommRing R] {W' : Affine R} : sym2x 0 0 = ![1, 0, 0]

@[simp]

theorem WeierstrassCurve.Affine.Point.sym2x_zero_some {R : Type u_1} [CommRing R] {W' : Affine R} {x y : R} (h : W'.Nonsingular x y) : sym2x 0 (some x y h) = ![x, 1, 0]

@[simp]

theorem WeierstrassCurve.Affine.Point.sym2x_some_zero {R : Type u_1} [CommRing R] {W' : Affine R} {x y : R} (h : W'.Nonsingular x y) : (some x y h).sym2x 0 = ![x, 1, 0]

@[simp]

theorem WeierstrassCurve.Affine.Point.sym2x_some_some {R : Type u_1} [CommRing R] {W' : Affine R} {x y x' y' : R} (h : W'.Nonsingular x y) (h' : W'.Nonsingular x' y') : (some x y h).sym2x (some x' y' h') = ![x * x', x + x', 1]

theorem WeierstrassCurve.Affine.Point.sym2x_ne_zero {R : Type u_1} [CommRing R] {W' : Affine R} [Nontrivial R] (P Q : W'.Point) : P.sym2x Q ≠ 0

theorem WeierstrassCurve.Affine.Point.sym2x_comm {R : Type u_1} [CommRing R] {W' : Affine R} (P Q : W'.Point) : P.sym2x Q = Q.sym2x P

@[simp]

theorem WeierstrassCurve.Affine.Point.sym2x_neg_left {R : Type u_1} [CommRing R] {W' : Affine R} (P Q : W'.Point) : (-P).sym2x Q = P.sym2x Q

@[simp]

theorem WeierstrassCurve.Affine.Point.sym2x_neg_right {R : Type u_1} [CommRing R] {W' : Affine R} (P Q : W'.Point) : P.sym2x (-Q) = P.sym2x Q

theorem WeierstrassCurve.Affine.Point.sym2x_self_eq_addSubMap {R : Type u_1} [CommRing R] {W' : Affine R} (P : W'.Point) : P.sym2x P = fun (x : Fin 3) => (MvPolynomial.eval (P.sym2x 0)) (addSubMap W' x)

theorem WeierstrassCurve.Affine.Point.addSubMap_sym2x_some_some {F : Type u_2} [Field F] {W : Affine F} {xP yP xQ yQ : F} (hP : W.Nonsingular xP yP) (hQ : W.Nonsingular xQ yQ) : (fun (x : Fin 3) => (MvPolynomial.eval ((some xP yP hP).sym2x (some xQ yQ hQ))) (addSubMap W x)) = ![(xP * xQ) ^ 2 - b₄ W * (xP * xQ) - b₆ W * (xP + xQ) - b₈ W, 2 * (xP + xQ) * (xP * xQ) + b₂ W * (xP * xQ) + b₄ W * (xP + xQ) + b₆ W, (xP - xQ) ^ 2]

theorem WeierstrassCurve.Affine.Point.addSubMap_sym2x_some_self {F : Type u_2} [Field F] {W : Affine F} {x y : F} (h : W.Nonsingular x y) : (fun (x_1 : Fin 3) => (MvPolynomial.eval ((some x y h).sym2x (some x y h))) (addSubMap W x_1)) = ![x ^ 4 - b₄ W * x ^ 2 - 2 * b₆ W * x - b₈ W, 4 * x ^ 3 + b₂ W * x ^ 2 + 2 * b₄ W * x + b₆ W, 0]

theorem WeierstrassCurve.Affine.Point.sym2x_add_sub_eq_addSubMap_sym2x {F : Type u_2} [Field F] {W : Affine F} [DecidableEq F] (P Q : W.Point) : ∃ (t : F), t ≠ 0 ∧ t • (P + Q).sym2x (P - Q) = fun (x : Fin 3) => (MvPolynomial.eval (P.sym2x Q)) (addSubMap W x)

sym2x (P + Q) (P - Q) is equal, up to scaling by a nonzero constant, to addSubMap W applied to sym2x P Q.