Documentation

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

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 #

source
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.
Instances For
    source
    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.
    Instances For
      source
      theorem WeierstrassCurve.isHomogeneous_addSubMap {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (i : Fin 3) :
      (W.addSubMap i).IsHomogeneous 2
      source
      theorem WeierstrassCurve.isHomogeneous_addSubMapCoeff {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (ij : Fin 3 × Fin 3) :
      (W.addSubMapCoeff ij).IsHomogeneous 2
      source
      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
      source
      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