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 (i : Fin 3) => (MvPolynomial.eval x) (W.addSubMap i)) ≠ 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

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

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