Jacobian coordinates for Weierstrass curves

This file defines the type of points on a Weierstrass curve as a tuple, consisting of an equivalence class of triples up to scaling by weights, satisfying a Weierstrass equation with a nonsingular condition.

Mathematical background

Let W be a Weierstrass curve over a field F. A point on the weighted projective plane with weights $(2, 3, 1)$ is an equivalence class of triples $[x:y:z]$ with coordinates in F such that $(x, y, z) \sim (x', y', z')$ precisely if there is some unit $u$ of F such that $(x, y, z) = (u^2x', u^3y', uz')$, with an extra condition that $(x, y, z) \ne (0, 0, 0)$. A rational point is a point on the $(2, 3, 1)$-projective plane satisfying a $(2, 3, 1)$-homogeneous Weierstrass equation $Y^2 + a_1XYZ + a_3YZ^3 = X^3 + a_2X^2Z^2 + a_4XZ^4 + a_6Z^6$, and being nonsingular means the partial derivatives $W_X(X, Y, Z)$, $W_Y(X, Y, Z)$, and $W_Z(X, Y, Z)$ do not vanish simultaneously. Note that the vanishing of the Weierstrass equation and its partial derivatives are independent of the representative for $[x:y:z]$, and the nonsingularity condition already implies that $(x, y, z) \ne (0, 0, 0)$, so a nonsingular rational point on W can simply be given by a tuple consisting of $[x:y:z]$ and the nonsingular condition on any representative. In cryptography, as well as in this file, this is often called the Jacobian coordinates of W.

Main definitions

• WeierstrassCurve.Jacobian.PointClass: the equivalence class of a point representative.
• WeierstrassCurve.Jacobian.toAffine: the Weierstrass curve in affine coordinates.
• WeierstrassCurve.Jacobian.Nonsingular: the nonsingular condition on a point representative.
• WeierstrassCurve.Jacobian.NonsingularLift: the nonsingular condition on a point class.

Implementation notes

A point representative is implemented as a term P of type Fin 3 → R, which allows for the vector notation ![x, y, z]. However, P is not definitionally equivalent to the expanded vector ![P x, P y, P z], so the auxiliary lemma fin3_def can be used to convert between the two forms. The equivalence of two point representatives P and Q is implemented as an equivalence of orbits of the action of Rˣ, or equivalently that there is some unit u of R such that P = u • Q. However, u • Q is again not definitionally equal to ![u² * Q x, u³ * Q y, u * Q z], so the auxiliary lemmas smul_fin3 and smul_fin3_ext can be used to convert between the two forms.

References

[J Silverman, The Arithmetic of Elliptic Curves][silverman2009]

Tags

elliptic curve, rational point, Jacobian coordinates

Weierstrass curves

@[reducible, inline]

abbrev WeierstrassCurve.Jacobian (R : Type u_1) : Type u_1

An abbreviation for a Weierstrass curve in Jacobian coordinates.

Equations

• WeierstrassCurve.Jacobian = WeierstrassCurve

theorem WeierstrassCurve.Jacobian.fin3_def {R : Type u} (P : Fin 3 → R) : P = ![P 0, P 1, P 2]

def WeierstrassCurve.Jacobian.instSMulPoint {R : Type u} [CommRing R] : SMul Rˣ (Fin 3 → R)

The scalar multiplication on a point representative.

Equations

• WeierstrassCurve.Jacobian.instSMulPoint = { smul := fun (u : Rˣ) (P : Fin 3 → R) => ![↑u ^ 2 * P 0, ↑u ^ 3 * P 1, ↑u * P 2] }

theorem WeierstrassCurve.Jacobian.smul_fin3 {R : Type u} [CommRing R] (P : Fin 3 → R) (u : Rˣ) : u • P = ![↑u ^ 2 * P 0, ↑u ^ 3 * P 1, ↑u * P 2]

theorem WeierstrassCurve.Jacobian.smul_fin3_ext {R : Type u} [CommRing R] (P : Fin 3 → R) (u : Rˣ) : (u • P) 0 = ↑u ^ 2 * P 0 ∧ (u • P) 1 = ↑u ^ 3 * P 1 ∧ (u • P) 2 = ↑u * P 2

def WeierstrassCurve.Jacobian.instMulActionPoint {R : Type u} [CommRing R] : MulAction Rˣ (Fin 3 → R)

The multiplicative action on a point representative.

Equations

• WeierstrassCurve.Jacobian.instMulActionPoint = MulAction.mk ⋯ ⋯

def WeierstrassCurve.Jacobian.instSetoidPoint {R : Type u} [CommRing R] : Setoid (Fin 3 → R)

The equivalence setoid for a point representative.

Equations

• WeierstrassCurve.Jacobian.instSetoidPoint = MulAction.orbitRel Rˣ (Fin 3 → R)

@[reducible, inline]

abbrev WeierstrassCurve.Jacobian.PointClass (R : Type u) [CommRing R] : Type u

The equivalence class of a point representative.

Equations

• WeierstrassCurve.Jacobian.PointClass R = MulAction.orbitRel.Quotient Rˣ (Fin 3 → R)

@[reducible, inline]

abbrev WeierstrassCurve.Jacobian.toAffine {R : Type u} (W : WeierstrassCurve.Jacobian R) : WeierstrassCurve.Affine R

The coercion to a Weierstrass curve in affine coordinates.

Equations

• W.toAffine = W

Equations and nonsingularity

noncomputable def WeierstrassCurve.Jacobian.polynomial {R : Type u} [CommRing R] (W : WeierstrassCurve.Jacobian R) : MvPolynomial (Fin 3) R

The polynomial $W(X, Y, Z) := Y^2 + a_1XYZ + a_3YZ^3 - (X^3 + a_2X^2Z^2 + a_4XZ^4 + a_6Z^6)$ associated to a Weierstrass curve W over R. This is represented as a term of type MvPolynomial (Fin 3) R, where X 0, X 1, and X 2 represent $X$, $Y$, and $Z$ respectively.

Equations

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

theorem WeierstrassCurve.Jacobian.eval_polynomial {R : Type u} [CommRing R] (W : WeierstrassCurve.Jacobian R) (P : Fin 3 → R) : (MvPolynomial.eval P) W.polynomial = P 1 ^ 2 + W.a₁ * P 0 * P 1 * P 2 + W.a₃ * P 1 * P 2 ^ 3 - (P 0 ^ 3 + W.a₂ * P 0 ^ 2 * P 2 ^ 2 + W.a₄ * P 0 * P 2 ^ 4 + W.a₆ * P 2 ^ 6)

def WeierstrassCurve.Jacobian.Equation {R : Type u} [CommRing R] (W : WeierstrassCurve.Jacobian R) (P : Fin 3 → R) : Prop

The proposition that a point representative $(x, y, z)$ lies in W. In other words, $W(x, y, z) = 0$.

Equations

• W.Equation P = ((MvPolynomial.eval P) W.polynomial = 0)

theorem WeierstrassCurve.Jacobian.equation_iff {R : Type u} [CommRing R] (W : WeierstrassCurve.Jacobian R) (P : Fin 3 → R) : W.Equation P ↔ P 1 ^ 2 + W.a₁ * P 0 * P 1 * P 2 + W.a₃ * P 1 * P 2 ^ 3 = P 0 ^ 3 + W.a₂ * P 0 ^ 2 * P 2 ^ 2 + W.a₄ * P 0 * P 2 ^ 4 + W.a₆ * P 2 ^ 6

theorem WeierstrassCurve.Jacobian.equation_zero {R : Type u} [CommRing R] (W : WeierstrassCurve.Jacobian R) : W.Equation ![1, 1, 0]

theorem WeierstrassCurve.Jacobian.equation_zero' {R : Type u} [CommRing R] (W : WeierstrassCurve.Jacobian R) (Y : R) : W.Equation ![Y ^ 2, Y ^ 3, 0]

theorem WeierstrassCurve.Jacobian.equation_some {R : Type u} [CommRing R] (W : WeierstrassCurve.Jacobian R) (X : R) (Y : R) : W.Equation ![X, Y, 1] ↔ W.toAffine.equation X Y

theorem WeierstrassCurve.Jacobian.equation_smul_iff {R : Type u} [CommRing R] (W : WeierstrassCurve.Jacobian R) (P : Fin 3 → R) (u : Rˣ) : W.Equation (u • P) ↔ W.Equation P

noncomputable def WeierstrassCurve.Jacobian.polynomialX {R : Type u} [CommRing R] (W : WeierstrassCurve.Jacobian R) : MvPolynomial (Fin 3) R

The partial derivative $W_X(X, Y, Z)$ of $W(X, Y, Z)$ with respect to $X$.

Equations

• W.polynomialX = (MvPolynomial.pderiv 0) W.polynomial

theorem WeierstrassCurve.Jacobian.polynomialX_eq {R : Type u} [CommRing R] (W : WeierstrassCurve.Jacobian R) : W.polynomialX = MvPolynomial.C W.a₁ * MvPolynomial.X 1 * MvPolynomial.X 2 - (MvPolynomial.C 3 * MvPolynomial.X 0 ^ 2 + MvPolynomial.C (2 * W.a₂) * MvPolynomial.X 0 * MvPolynomial.X 2 ^ 2 + MvPolynomial.C W.a₄ * MvPolynomial.X 2 ^ 4)

theorem WeierstrassCurve.Jacobian.eval_polynomialX {R : Type u} [CommRing R] (W : WeierstrassCurve.Jacobian R) (P : Fin 3 → R) : (MvPolynomial.eval P) W.polynomialX = W.a₁ * P 1 * P 2 - (3 * P 0 ^ 2 + 2 * W.a₂ * P 0 * P 2 ^ 2 + W.a₄ * P 2 ^ 4)

noncomputable def WeierstrassCurve.Jacobian.polynomialY {R : Type u} [CommRing R] (W : WeierstrassCurve.Jacobian R) : MvPolynomial (Fin 3) R

The partial derivative $W_Y(X, Y, Z)$ of $W(X, Y, Z)$ with respect to $Y$.

Equations

• W.polynomialY = (MvPolynomial.pderiv 1) W.polynomial

theorem WeierstrassCurve.Jacobian.polynomialY_eq {R : Type u} [CommRing R] (W : WeierstrassCurve.Jacobian R) : W.polynomialY = MvPolynomial.C 2 * MvPolynomial.X 1 + MvPolynomial.C W.a₁ * MvPolynomial.X 0 * MvPolynomial.X 2 + MvPolynomial.C W.a₃ * MvPolynomial.X 2 ^ 3

theorem WeierstrassCurve.Jacobian.eval_polynomialY {R : Type u} [CommRing R] (W : WeierstrassCurve.Jacobian R) (P : Fin 3 → R) : (MvPolynomial.eval P) W.polynomialY = 2 * P 1 + W.a₁ * P 0 * P 2 + W.a₃ * P 2 ^ 3

noncomputable def WeierstrassCurve.Jacobian.polynomialZ {R : Type u} [CommRing R] (W : WeierstrassCurve.Jacobian R) : MvPolynomial (Fin 3) R

The partial derivative $W_Z(X, Y, Z)$ of $W(X, Y, Z)$ with respect to $Z$.

Equations

• W.polynomialZ = (MvPolynomial.pderiv 2) W.polynomial

theorem WeierstrassCurve.Jacobian.polynomialZ_eq {R : Type u} [CommRing R] (W : WeierstrassCurve.Jacobian R) : W.polynomialZ = MvPolynomial.C W.a₁ * MvPolynomial.X 0 * MvPolynomial.X 1 + MvPolynomial.C (3 * W.a₃) * MvPolynomial.X 1 * MvPolynomial.X 2 ^ 2 - (MvPolynomial.C (2 * W.a₂) * MvPolynomial.X 0 ^ 2 * MvPolynomial.X 2 + MvPolynomial.C (4 * W.a₄) * MvPolynomial.X 0 * MvPolynomial.X 2 ^ 3 + MvPolynomial.C (6 * W.a₆) * MvPolynomial.X 2 ^ 5)

theorem WeierstrassCurve.Jacobian.eval_polynomialZ {R : Type u} [CommRing R] (W : WeierstrassCurve.Jacobian R) (P : Fin 3 → R) : (MvPolynomial.eval P) W.polynomialZ = W.a₁ * P 0 * P 1 + 3 * W.a₃ * P 1 * P 2 ^ 2 - (2 * W.a₂ * P 0 ^ 2 * P 2 + 4 * W.a₄ * P 0 * P 2 ^ 3 + 6 * W.a₆ * P 2 ^ 5)

def WeierstrassCurve.Jacobian.Nonsingular {R : Type u} [CommRing R] (W : WeierstrassCurve.Jacobian R) (P : Fin 3 → R) : Prop

The proposition that a point representative $(x, y, z)$ in W is nonsingular. In other words, either $W_X(x, y, z) \ne 0$, $W_Y(x, y, z) \ne 0$, or $W_Z(x, y, z) \ne 0$.

Equations

• W.Nonsingular P = (W.Equation P ∧ ((MvPolynomial.eval P) W.polynomialX ≠ 0 ∨ (MvPolynomial.eval P) W.polynomialY ≠ 0 ∨ (MvPolynomial.eval P) W.polynomialZ ≠ 0))

theorem WeierstrassCurve.Jacobian.nonsingular_iff {R : Type u} [CommRing R] (W : WeierstrassCurve.Jacobian R) (P : Fin 3 → R) : W.Nonsingular P ↔ W.Equation P ∧ (W.a₁ * P 1 * P 2 ≠ 3 * P 0 ^ 2 + 2 * W.a₂ * P 0 * P 2 ^ 2 + W.a₄ * P 2 ^ 4 ∨ P 1 ≠ -P 1 - W.a₁ * P 0 * P 2 - W.a₃ * P 2 ^ 3 ∨ W.a₁ * P 0 * P 1 + 3 * W.a₃ * P 1 * P 2 ^ 2 ≠ 2 * W.a₂ * P 0 ^ 2 * P 2 + 4 * W.a₄ * P 0 * P 2 ^ 3 + 6 * W.a₆ * P 2 ^ 5)

theorem WeierstrassCurve.Jacobian.nonsingular_zero {R : Type u} [CommRing R] (W : WeierstrassCurve.Jacobian R) [Nontrivial R] : W.Nonsingular ![1, 1, 0]

theorem WeierstrassCurve.Jacobian.nonsingular_zero' {R : Type u} [CommRing R] (W : WeierstrassCurve.Jacobian R) [NoZeroDivisors R] {Y : R} (hy : Y ≠ 0) : W.Nonsingular ![Y ^ 2, Y ^ 3, 0]

theorem WeierstrassCurve.Jacobian.nonsingular_some {R : Type u} [CommRing R] (W : WeierstrassCurve.Jacobian R) (X : R) (Y : R) : W.Nonsingular ![X, Y, 1] ↔ W.toAffine.nonsingular X Y

theorem WeierstrassCurve.Jacobian.nonsingular_smul_iff {R : Type u} [CommRing R] (W : WeierstrassCurve.Jacobian R) (P : Fin 3 → R) (u : Rˣ) : W.Nonsingular (u • P) ↔ W.Nonsingular P

theorem WeierstrassCurve.Jacobian.nonsingular_of_equiv {R : Type u} [CommRing R] (W : WeierstrassCurve.Jacobian R) {P : Fin 3 → R} {Q : Fin 3 → R} (h : P ≈ Q) : W.Nonsingular P ↔ W.Nonsingular Q

def WeierstrassCurve.Jacobian.NonsingularLift {R : Type u} [CommRing R] (W : WeierstrassCurve.Jacobian R) (P : WeierstrassCurve.Jacobian.PointClass R) : Prop

The proposition that a point class on W is nonsingular. If P is a point representative, then W.NonsingularLift ⟦P⟧ is definitionally equivalent to W.Nonsingular P.

Equations

• W.NonsingularLift P = Quotient.lift W.Nonsingular ⋯ P

@[simp]

theorem WeierstrassCurve.Jacobian.nonsingularLift_iff {R : Type u} [CommRing R] (W : WeierstrassCurve.Jacobian R) (P : Fin 3 → R) : W.NonsingularLift ⟦P⟧ ↔ W.Nonsingular P

theorem WeierstrassCurve.Jacobian.nonsingularLift_zero {R : Type u} [CommRing R] (W : WeierstrassCurve.Jacobian R) [Nontrivial R] : W.NonsingularLift ⟦![1, 1, 0]⟧

theorem WeierstrassCurve.Jacobian.nonsingularLift_zero' {R : Type u} [CommRing R] (W : WeierstrassCurve.Jacobian R) [NoZeroDivisors R] {Y : R} (hy : Y ≠ 0) : W.NonsingularLift ⟦![Y ^ 2, Y ^ 3, 0]⟧

theorem WeierstrassCurve.Jacobian.nonsingularLift_some {R : Type u} [CommRing R] (W : WeierstrassCurve.Jacobian R) (X : R) (Y : R) : W.NonsingularLift ⟦![X, Y, 1]⟧ ↔ W.toAffine.nonsingular X Y

theorem WeierstrassCurve.Jacobian.equiv_of_Z_eq_zero {F : Type u} [Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} {Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) (hPz : P 2 = 0) (hQz : Q 2 = 0) : P ≈ Q

theorem WeierstrassCurve.Jacobian.equiv_zero_of_Z_eq_zero {F : Type u} [Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} (h : W.Nonsingular P) (hPz : P 2 = 0) : P ≈ ![1, 1, 0]

theorem WeierstrassCurve.Jacobian.equiv_some_of_Z_ne_zero {F : Type u} [Field F] {P : Fin 3 → F} (hPz : P 2 ≠ 0) : P ≈ ![P 0 / P 2 ^ 2, P 1 / P 2 ^ 3, 1]

theorem WeierstrassCurve.Jacobian.nonsingular_iff_affine_of_Z_ne_zero {F : Type u} [Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} (hPz : P 2 ≠ 0) : W.Nonsingular P ↔ W.toAffine.nonsingular (P 0 / P 2 ^ 2) (P 1 / P 2 ^ 3)

theorem WeierstrassCurve.Jacobian.nonsingular_of_affine_of_Z_ne_zero {F : Type u} [Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} (h : W.toAffine.nonsingular (P 0 / P 2 ^ 2) (P 1 / P 2 ^ 3)) (hPz : P 2 ≠ 0) : W.Nonsingular P

theorem WeierstrassCurve.Jacobian.nonsingular_affine_of_Z_ne_zero {F : Type u} [Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} (h : W.Nonsingular P) (hPz : P 2 ≠ 0) : W.toAffine.nonsingular (P 0 / P 2 ^ 2) (P 1 / P 2 ^ 3)