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. This file also defines the negation and addition operations of the group law for this type, and proves that they respect the Weierstrass equation and the nonsingular condition. The fact that they form an abelian group is proven in Mathlib.AlgebraicGeometry.EllipticCurve.Group.

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.

As in Mathlib.AlgebraicGeometry.EllipticCurve.Affine, the set of nonsingular rational points forms an abelian group under the same secant-and-tangent process, but the polynomials involved are $(2, 3, 1)$-homogeneous, and any instances of division become multiplication in the $Z$-coordinate. Note that most computational proofs follow from their analogous proofs for affine coordinates.

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.
• WeierstrassCurve.Jacobian.neg: the negation operation on a point representative.
• WeierstrassCurve.Jacobian.negMap: the negation operation on a point class.
• WeierstrassCurve.Jacobian.add: the addition operation on a point representative.
• WeierstrassCurve.Jacobian.addMap: the addition operation on a point class.
• WeierstrassCurve.Jacobian.Point: a nonsingular rational point.
• WeierstrassCurve.Jacobian.Point.neg: the negation operation on a nonsingular rational point.
• WeierstrassCurve.Jacobian.Point.add: the addition operation on a nonsingular rational point.
• WeierstrassCurve.Jacobian.Point.toAffineAddEquiv: the equivalence between the nonsingular rational points on a Weierstrass curve in Jacobian coordinates with those in affine coordinates.

Main statements

• WeierstrassCurve.Jacobian.NonsingularNeg: negation preserves the nonsingular condition.
• WeierstrassCurve.Jacobian.NonsingularAdd: addition preserves the nonsingular condition.

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 syntactically equivalent to the expanded vector ![P x, P y, P z], so the lemmas fin3_def and fin3_def_ext 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 not syntactically equal to ![u² * Q x, u³ * Q y, u * Q z], so the lemmas smul_fin3 and smul_fin3_ext can be used to convert between the two forms.

References

J Silverman, The Arithmetic of Elliptic Curves

Tags

elliptic curve, rational point, Jacobian coordinates

Weierstrass curves

@[reducible, inline]

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

An abbreviation for a Weierstrass curve in Jacobian coordinates.

Equations

• WeierstrassCurve.Jacobian R = WeierstrassCurve R

@[reducible, inline]

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

The coercion to a Weierstrass curve in Jacobian coordinates.

Equations

• W.toJacobian = W

Jacobian coordinates

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

theorem WeierstrassCurve.Jacobian.fin3_def_ext {R : Type u} (X Y Z : R) : ![X, Y, Z] 0 = X ∧ ![X, Y, Z] 1 = Y ∧ ![X, Y, Z] 2 = Z

theorem WeierstrassCurve.Jacobian.comp_fin3 {R : Type u} {S : Type u_1} (f : R → S) (X Y Z : R) : f ∘ ![X, Y, Z] = ![f X, f Y, f Z]

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)

theorem WeierstrassCurve.Jacobian.smul_equiv {R : Type u} [CommRing R] (P : Fin 3 → R) {u : R} (hu : IsUnit u) : u • P ≈ P

@[simp]

theorem WeierstrassCurve.Jacobian.smul_eq {R : Type u} [CommRing R] (P : Fin 3 → R) {u : R} (hu : IsUnit u) : ⟦u • P⟧ = ⟦P⟧

@[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'

theorem WeierstrassCurve.Jacobian.equiv_iff_eq_of_Z_eq' {R : Type u} [CommRing R] {P Q : Fin 3 → R} (hz : P 2 = Q 2) (mem : Q 2 ∈ nonZeroDivisors R) : P ≈ Q ↔ P = Q

theorem WeierstrassCurve.Jacobian.equiv_iff_eq_of_Z_eq {R : Type u} [CommRing R] [NoZeroDivisors R] {P Q : Fin 3 → R} (hz : P 2 = Q 2) (hQz : Q 2 ≠ 0) : P ≈ Q ↔ P = Q

theorem WeierstrassCurve.Jacobian.Z_eq_zero_of_equiv {R : Type u} [CommRing R] {P Q : Fin 3 → R} (h : P ≈ Q) : P 2 = 0 ↔ Q 2 = 0

theorem WeierstrassCurve.Jacobian.X_eq_of_equiv {R : Type u} [CommRing R] {P Q : Fin 3 → R} (h : P ≈ Q) : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2

theorem WeierstrassCurve.Jacobian.Y_eq_of_equiv {R : Type u} [CommRing R] {P Q : Fin 3 → R} (h : P ≈ Q) : P 1 * Q 2 ^ 3 = Q 1 * P 2 ^ 3

theorem WeierstrassCurve.Jacobian.not_equiv_of_Z_eq_zero_left {R : Type u} [CommRing R] {P Q : Fin 3 → R} (hPz : P 2 = 0) (hQz : Q 2 ≠ 0) : ¬P ≈ Q

theorem WeierstrassCurve.Jacobian.not_equiv_of_Z_eq_zero_right {R : Type u} [CommRing R] {P Q : Fin 3 → R} (hPz : P 2 ≠ 0) (hQz : Q 2 = 0) : ¬P ≈ Q

theorem WeierstrassCurve.Jacobian.not_equiv_of_X_ne {R : Type u} [CommRing R] {P Q : Fin 3 → R} (hx : P 0 * Q 2 ^ 2 ≠ Q 0 * P 2 ^ 2) : ¬P ≈ Q

theorem WeierstrassCurve.Jacobian.not_equiv_of_Y_ne {R : Type u} [CommRing R] {P Q : Fin 3 → R} (hy : P 1 * Q 2 ^ 3 ≠ Q 1 * P 2 ^ 3) : ¬P ≈ Q

theorem WeierstrassCurve.Jacobian.equiv_of_X_eq_of_Y_eq {F : Type v} [Field F] {P Q : Fin 3 → F} (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) (hy : P 1 * Q 2 ^ 3 = Q 1 * P 2 ^ 3) : P ≈ Q

theorem WeierstrassCurve.Jacobian.equiv_some_of_Z_ne_zero {F : Type v} [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.X_eq_iff {F : Type v} [Field F] {P Q : Fin 3 → F} (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 ↔ P 0 / P 2 ^ 2 = Q 0 / Q 2 ^ 2

theorem WeierstrassCurve.Jacobian.Y_eq_iff {F : Type v} [Field F] {P Q : Fin 3 → F} (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) : P 1 * Q 2 ^ 3 = Q 1 * P 2 ^ 3 ↔ P 1 / P 2 ^ 3 = Q 1 / Q 2 ^ 3

Weierstrass equations

noncomputable def WeierstrassCurve.Jacobian.polynomial {R : Type u} (W' : WeierstrassCurve.Jacobian R) [CommRing 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} {W' : WeierstrassCurve.Jacobian R} [CommRing 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)

theorem WeierstrassCurve.Jacobian.eval_polynomial_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} (hPz : P 2 ≠ 0) : (MvPolynomial.eval P) W.polynomial / P 2 ^ 6 = Polynomial.evalEval (P 0 / P 2 ^ 2) (P 1 / P 2 ^ 3) W.toAffine.polynomial

def WeierstrassCurve.Jacobian.Equation {R : Type u} (W' : WeierstrassCurve.Jacobian R) [CommRing 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} {W' : WeierstrassCurve.Jacobian R} [CommRing 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) = 0

theorem WeierstrassCurve.Jacobian.equation_smul {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] (P : Fin 3 → R) {u : R} (hu : IsUnit u) : W'.Equation (u • P) ↔ W'.Equation P

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

theorem WeierstrassCurve.Jacobian.equation_of_Z_eq_zero {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P : Fin 3 → R} (hPz : P 2 = 0) : W'.Equation P ↔ P 1 ^ 2 = P 0 ^ 3

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

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

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

Nonsingular Weierstrass equations

noncomputable def WeierstrassCurve.Jacobian.polynomialX {R : Type u} (W' : WeierstrassCurve.Jacobian R) [CommRing 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} {W' : WeierstrassCurve.Jacobian R} [CommRing 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} {W' : WeierstrassCurve.Jacobian R} [CommRing 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)

theorem WeierstrassCurve.Jacobian.eval_polynomialX_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} (hPz : P 2 ≠ 0) : (MvPolynomial.eval P) W.polynomialX / P 2 ^ 4 = Polynomial.evalEval (P 0 / P 2 ^ 2) (P 1 / P 2 ^ 3) W.toAffine.polynomialX

noncomputable def WeierstrassCurve.Jacobian.polynomialY {R : Type u} (W' : WeierstrassCurve.Jacobian R) [CommRing 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} {W' : WeierstrassCurve.Jacobian R} [CommRing 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} {W' : WeierstrassCurve.Jacobian R} [CommRing R] (P : Fin 3 → R) : (MvPolynomial.eval P) W'.polynomialY = 2 * P 1 + W'.a₁ * P 0 * P 2 + W'.a₃ * P 2 ^ 3

theorem WeierstrassCurve.Jacobian.eval_polynomialY_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} (hPz : P 2 ≠ 0) : (MvPolynomial.eval P) W.polynomialY / P 2 ^ 3 = Polynomial.evalEval (P 0 / P 2 ^ 2) (P 1 / P 2 ^ 3) W.toAffine.polynomialY

noncomputable def WeierstrassCurve.Jacobian.polynomialZ {R : Type u} (W' : WeierstrassCurve.Jacobian R) [CommRing 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} {W' : WeierstrassCurve.Jacobian R} [CommRing 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} {W' : WeierstrassCurve.Jacobian R} [CommRing 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} (W' : WeierstrassCurve.Jacobian R) [CommRing 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$.

Note that this definition is only mathematically accurate for fields.

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} {W' : WeierstrassCurve.Jacobian R} [CommRing 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) ≠ 0 ∨ 2 * P 1 + W'.a₁ * P 0 * P 2 + W'.a₃ * P 2 ^ 3 ≠ 0 ∨ 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) ≠ 0)

theorem WeierstrassCurve.Jacobian.nonsingular_smul {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] (P : Fin 3 → R) {u : R} (hu : IsUnit u) : W'.Nonsingular (u • P) ↔ W'.Nonsingular P

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

theorem WeierstrassCurve.Jacobian.nonsingular_of_Z_eq_zero {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P : Fin 3 → R} (hPz : P 2 = 0) : W'.Nonsingular P ↔ W'.Equation P ∧ (3 * P 0 ^ 2 ≠ 0 ∨ 2 * P 1 ≠ 0 ∨ W'.a₁ * P 0 * P 1 ≠ 0)

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

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

theorem WeierstrassCurve.Jacobian.nonsingular_of_Z_ne_zero {F : Type v} [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_iff_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} (hPz : P 2 ≠ 0) : W.Nonsingular P ↔ W.Equation P ∧ ((MvPolynomial.eval P) W.polynomialX ≠ 0 ∨ (MvPolynomial.eval P) W.polynomialY ≠ 0)

theorem WeierstrassCurve.Jacobian.X_ne_zero_of_Z_eq_zero {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] [NoZeroDivisors R] {P : Fin 3 → R} (hP : W'.Nonsingular P) (hPz : P 2 = 0) : P 0 ≠ 0

theorem WeierstrassCurve.Jacobian.isUnit_X_of_Z_eq_zero {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} (hP : W.Nonsingular P) (hPz : P 2 = 0) : IsUnit (P 0)

theorem WeierstrassCurve.Jacobian.Y_ne_zero_of_Z_eq_zero {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] [NoZeroDivisors R] {P : Fin 3 → R} (hP : W'.Nonsingular P) (hPz : P 2 = 0) : P 1 ≠ 0

theorem WeierstrassCurve.Jacobian.isUnit_Y_of_Z_eq_zero {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} (hP : W.Nonsingular P) (hPz : P 2 = 0) : IsUnit (P 1)

theorem WeierstrassCurve.Jacobian.equiv_of_Z_eq_zero {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P 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 v} [Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} (hP : W.Nonsingular P) (hPz : P 2 = 0) : P ≈ ![1, 1, 0]

def WeierstrassCurve.Jacobian.NonsingularLift {R : Type u} (W' : WeierstrassCurve.Jacobian R) [CommRing 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

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

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

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

Negation formulae

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

The $Y$-coordinate of the negation of a point representative.

Equations

• W'.negY P = -P 1 - W'.a₁ * P 0 * P 2 - W'.a₃ * P 2 ^ 3

theorem WeierstrassCurve.Jacobian.negY_smul {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] (P : Fin 3 → R) {u : R} : W'.negY (u • P) = u ^ 3 * W'.negY P

theorem WeierstrassCurve.Jacobian.negY_of_Z_eq_zero {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P : Fin 3 → R} (hPz : P 2 = 0) : W'.negY P = -P 1

theorem WeierstrassCurve.Jacobian.negY_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} (hPz : P 2 ≠ 0) : W.negY P / P 2 ^ 3 = W.toAffine.negY (P 0 / P 2 ^ 2) (P 1 / P 2 ^ 3)

theorem WeierstrassCurve.Jacobian.Y_sub_Y_mul_Y_sub_negY {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) : (P 1 * Q 2 ^ 3 - Q 1 * P 2 ^ 3) * (P 1 * Q 2 ^ 3 - W'.negY Q * P 2 ^ 3) = 0

theorem WeierstrassCurve.Jacobian.Y_eq_of_Y_ne {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) (hy : P 1 * Q 2 ^ 3 ≠ Q 1 * P 2 ^ 3) : P 1 * Q 2 ^ 3 = W.negY Q * P 2 ^ 3

theorem WeierstrassCurve.Jacobian.Y_eq_of_Y_ne' {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) (hy : P 1 * Q 2 ^ 3 ≠ W.negY Q * P 2 ^ 3) : P 1 * Q 2 ^ 3 = Q 1 * P 2 ^ 3

theorem WeierstrassCurve.Jacobian.Y_eq_iff' {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) : P 1 * Q 2 ^ 3 = W.negY Q * P 2 ^ 3 ↔ P 1 / P 2 ^ 3 = W.toAffine.negY (Q 0 / Q 2 ^ 2) (Q 1 / Q 2 ^ 3)

theorem WeierstrassCurve.Jacobian.Y_sub_Y_add_Y_sub_negY {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] (P Q : Fin 3 → R) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) : P 1 * Q 2 ^ 3 - Q 1 * P 2 ^ 3 + (P 1 * Q 2 ^ 3 - W'.negY Q * P 2 ^ 3) = (P 1 - W'.negY P) * Q 2 ^ 3

theorem WeierstrassCurve.Jacobian.Y_ne_negY_of_Y_ne {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) (hy : P 1 * Q 2 ^ 3 ≠ Q 1 * P 2 ^ 3) : P 1 ≠ W'.negY P

theorem WeierstrassCurve.Jacobian.Y_ne_negY_of_Y_ne' {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) (hy : P 1 * Q 2 ^ 3 ≠ W'.negY Q * P 2 ^ 3) : P 1 ≠ W'.negY P

theorem WeierstrassCurve.Jacobian.Y_eq_negY_of_Y_eq {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] [NoZeroDivisors R] {P Q : Fin 3 → R} (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) (hy : P 1 * Q 2 ^ 3 = Q 1 * P 2 ^ 3) (hy' : P 1 * Q 2 ^ 3 = W'.negY Q * P 2 ^ 3) : P 1 = W'.negY P

theorem WeierstrassCurve.Jacobian.nonsingular_iff_of_Y_eq_negY {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} (hPz : P 2 ≠ 0) (hy : P 1 = W.negY P) : W.Nonsingular P ↔ W.Equation P ∧ (MvPolynomial.eval P) W.polynomialX ≠ 0

Doubling formulae

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

The unit associated to the doubling of a 2-torsion point. More specifically, the unit u such that W.add P P = u • ![1, 1, 0] where P = W.neg P.

Equations

• W'.dblU P = (MvPolynomial.eval P) W'.polynomialX

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

theorem WeierstrassCurve.Jacobian.dblU_smul {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] (P : Fin 3 → R) (u : R) : W'.dblU (u • P) = u ^ 4 * W'.dblU P

theorem WeierstrassCurve.Jacobian.dblU_of_Z_eq_zero {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P : Fin 3 → R} (hPz : P 2 = 0) : W'.dblU P = -3 * P 0 ^ 2

theorem WeierstrassCurve.Jacobian.dblU_ne_zero_of_Y_eq {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) (hy : P 1 * Q 2 ^ 3 = Q 1 * P 2 ^ 3) (hy' : P 1 * Q 2 ^ 3 = W.negY Q * P 2 ^ 3) : W.dblU P ≠ 0

theorem WeierstrassCurve.Jacobian.isUnit_dblU_of_Y_eq {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) (hy : P 1 * Q 2 ^ 3 = Q 1 * P 2 ^ 3) (hy' : P 1 * Q 2 ^ 3 = W.negY Q * P 2 ^ 3) : IsUnit (W.dblU P)

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

The $Z$-coordinate of the doubling of a point representative.

Equations

• W'.dblZ P = P 2 * (P 1 - W'.negY P)

theorem WeierstrassCurve.Jacobian.dblZ_smul {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] (P : Fin 3 → R) (u : R) : W'.dblZ (u • P) = u ^ 4 * W'.dblZ P

theorem WeierstrassCurve.Jacobian.dblZ_of_Z_eq_zero {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P : Fin 3 → R} (hPz : P 2 = 0) : W'.dblZ P = 0

theorem WeierstrassCurve.Jacobian.dblZ_of_Y_eq {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] [NoZeroDivisors R] {P Q : Fin 3 → R} (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) (hy : P 1 * Q 2 ^ 3 = Q 1 * P 2 ^ 3) (hy' : P 1 * Q 2 ^ 3 = W'.negY Q * P 2 ^ 3) : W'.dblZ P = 0

theorem WeierstrassCurve.Jacobian.dblZ_ne_zero_of_Y_ne {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hPz : P 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) (hy : P 1 * Q 2 ^ 3 ≠ Q 1 * P 2 ^ 3) : W'.dblZ P ≠ 0

theorem WeierstrassCurve.Jacobian.isUnit_dblZ_of_Y_ne {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) (hy : P 1 * Q 2 ^ 3 ≠ Q 1 * P 2 ^ 3) : IsUnit (W.dblZ P)

theorem WeierstrassCurve.Jacobian.dblZ_ne_zero_of_Y_ne' {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hPz : P 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) (hy : P 1 * Q 2 ^ 3 ≠ W'.negY Q * P 2 ^ 3) : W'.dblZ P ≠ 0

theorem WeierstrassCurve.Jacobian.isUnit_dblZ_of_Y_ne' {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) (hy : P 1 * Q 2 ^ 3 ≠ W.negY Q * P 2 ^ 3) : IsUnit (W.dblZ P)

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

The $X$-coordinate of the doubling of a point representative.

Equations

• W'.dblX P = W'.dblU P ^ 2 - W'.a₁ * W'.dblU P * P 2 * (P 1 - W'.negY P) - W'.a₂ * P 2 ^ 2 * (P 1 - W'.negY P) ^ 2 - 2 * P 0 * (P 1 - W'.negY P) ^ 2

theorem WeierstrassCurve.Jacobian.dblX_smul {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] (P : Fin 3 → R) (u : R) : W'.dblX (u • P) = (u ^ 4) ^ 2 * W'.dblX P

theorem WeierstrassCurve.Jacobian.dblX_of_Z_eq_zero {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P : Fin 3 → R} (hP : W'.Equation P) (hPz : P 2 = 0) : W'.dblX P = (P 0 ^ 2) ^ 2

theorem WeierstrassCurve.Jacobian.dblX_of_Y_eq {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] [NoZeroDivisors R] {P Q : Fin 3 → R} (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) (hy : P 1 * Q 2 ^ 3 = Q 1 * P 2 ^ 3) (hy' : P 1 * Q 2 ^ 3 = W'.negY Q * P 2 ^ 3) : W'.dblX P = W'.dblU P ^ 2

theorem WeierstrassCurve.Jacobian.dblX_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) (hy : P 1 * Q 2 ^ 3 ≠ W.negY Q * P 2 ^ 3) : W.dblX P / W.dblZ P ^ 2 = W.toAffine.addX (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3))

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

The $Y$-coordinate of the negated doubling of a point representative.

Equations

• W'.negDblY P = -W'.dblU P * (W'.dblX P - P 0 * (P 1 - W'.negY P) ^ 2) + P 1 * (P 1 - W'.negY P) ^ 3

theorem WeierstrassCurve.Jacobian.negDblY_smul {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] (P : Fin 3 → R) (u : R) : W'.negDblY (u • P) = (u ^ 4) ^ 3 * W'.negDblY P

theorem WeierstrassCurve.Jacobian.negDblY_of_Z_eq_zero {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P : Fin 3 → R} (hP : W'.Equation P) (hPz : P 2 = 0) : W'.negDblY P = -(P 0 ^ 2) ^ 3

theorem WeierstrassCurve.Jacobian.negDblY_of_Y_eq {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] [NoZeroDivisors R] {P Q : Fin 3 → R} (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) (hy : P 1 * Q 2 ^ 3 = Q 1 * P 2 ^ 3) (hy' : P 1 * Q 2 ^ 3 = W'.negY Q * P 2 ^ 3) : W'.negDblY P = (-W'.dblU P) ^ 3

theorem WeierstrassCurve.Jacobian.negDblY_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) (hy : P 1 * Q 2 ^ 3 ≠ W.negY Q * P 2 ^ 3) : W.negDblY P / W.dblZ P ^ 3 = W.toAffine.negAddY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3))

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

The $Y$-coordinate of the doubling of a point representative.

Equations

• W'.dblY P = W'.negY ![W'.dblX P, W'.negDblY P, W'.dblZ P]

theorem WeierstrassCurve.Jacobian.dblY_smul {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] (P : Fin 3 → R) (u : R) : W'.dblY (u • P) = (u ^ 4) ^ 3 * W'.dblY P

theorem WeierstrassCurve.Jacobian.dblY_of_Z_eq_zero {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P : Fin 3 → R} (hP : W'.Equation P) (hPz : P 2 = 0) : W'.dblY P = (P 0 ^ 2) ^ 3

theorem WeierstrassCurve.Jacobian.dblY_of_Y_eq {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] [NoZeroDivisors R] {P Q : Fin 3 → R} (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) (hy : P 1 * Q 2 ^ 3 = Q 1 * P 2 ^ 3) (hy' : P 1 * Q 2 ^ 3 = W'.negY Q * P 2 ^ 3) : W'.dblY P = W'.dblU P ^ 3

theorem WeierstrassCurve.Jacobian.dblY_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) (hy : P 1 * Q 2 ^ 3 ≠ W.negY Q * P 2 ^ 3) : W.dblY P / W.dblZ P ^ 3 = W.toAffine.addY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3))

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

The coordinates of the doubling of a point representative.

Equations

• W'.dblXYZ P = ![W'.dblX P, W'.dblY P, W'.dblZ P]

theorem WeierstrassCurve.Jacobian.dblXYZ_smul {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] (P : Fin 3 → R) (u : R) : W'.dblXYZ (u • P) = u ^ 4 • W'.dblXYZ P

theorem WeierstrassCurve.Jacobian.dblXYZ_of_Z_eq_zero {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P : Fin 3 → R} (hP : W'.Equation P) (hPz : P 2 = 0) : W'.dblXYZ P = P 0 ^ 2 • ![1, 1, 0]

theorem WeierstrassCurve.Jacobian.dblXYZ_of_Y_eq' {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] [NoZeroDivisors R] {P Q : Fin 3 → R} (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) (hy : P 1 * Q 2 ^ 3 = Q 1 * P 2 ^ 3) (hy' : P 1 * Q 2 ^ 3 = W'.negY Q * P 2 ^ 3) : W'.dblXYZ P = ![W'.dblU P ^ 2, W'.dblU P ^ 3, 0]

theorem WeierstrassCurve.Jacobian.dblXYZ_of_Y_eq {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) (hy : P 1 * Q 2 ^ 3 = Q 1 * P 2 ^ 3) (hy' : P 1 * Q 2 ^ 3 = W.negY Q * P 2 ^ 3) : W.dblXYZ P = W.dblU P • ![1, 1, 0]

theorem WeierstrassCurve.Jacobian.dblXYZ_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) (hy : P 1 * Q 2 ^ 3 ≠ W.negY Q * P 2 ^ 3) : W.dblXYZ P = W.dblZ P • ![W.toAffine.addX (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)), W.toAffine.addY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)), 1]

Addition formulae

def WeierstrassCurve.Jacobian.addU {F : Type v} [Field F] (P Q : Fin 3 → F) : F

The unit associated to the addition of a non-2-torsion point with its negation. More specifically, the unit u such that W.add P Q = u • ![1, 1, 0] where P x / P z ^ 2 = Q x / Q z ^ 2 but P ≠ W.neg P.

Equations

• WeierstrassCurve.Jacobian.addU P Q = -((P 1 * Q 2 ^ 3 - Q 1 * P 2 ^ 3) / (P 2 * Q 2))

theorem WeierstrassCurve.Jacobian.addU_smul {F : Type v} [Field F] {P Q : Fin 3 → F} (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) {u v : F} (hu : u ≠ 0) (hv : v ≠ 0) : WeierstrassCurve.Jacobian.addU (u • P) (v • Q) = (u * v) ^ 2 * WeierstrassCurve.Jacobian.addU P Q

theorem WeierstrassCurve.Jacobian.addU_of_Z_eq_zero_left {F : Type v} [Field F] {P Q : Fin 3 → F} (hPz : P 2 = 0) : WeierstrassCurve.Jacobian.addU P Q = 0

theorem WeierstrassCurve.Jacobian.addU_of_Z_eq_zero_right {F : Type v} [Field F] {P Q : Fin 3 → F} (hQz : Q 2 = 0) : WeierstrassCurve.Jacobian.addU P Q = 0

theorem WeierstrassCurve.Jacobian.addU_ne_zero_of_Y_ne {F : Type v} [Field F] {P Q : Fin 3 → F} (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hy : P 1 * Q 2 ^ 3 ≠ Q 1 * P 2 ^ 3) : WeierstrassCurve.Jacobian.addU P Q ≠ 0

theorem WeierstrassCurve.Jacobian.isUnit_addU_of_Y_ne {F : Type v} [Field F] {P Q : Fin 3 → F} (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hy : P 1 * Q 2 ^ 3 ≠ Q 1 * P 2 ^ 3) : IsUnit (WeierstrassCurve.Jacobian.addU P Q)

def WeierstrassCurve.Jacobian.addZ {R : Type u} [CommRing R] (P Q : Fin 3 → R) : R

The $Z$-coordinate of the addition of two distinct point representatives.

Equations

• WeierstrassCurve.Jacobian.addZ P Q = P 0 * Q 2 ^ 2 - Q 0 * P 2 ^ 2

theorem WeierstrassCurve.Jacobian.addZ_self {R : Type u} [CommRing R] {P : Fin 3 → R} : WeierstrassCurve.Jacobian.addZ P P = 0

theorem WeierstrassCurve.Jacobian.addZ_smul {R : Type u} [CommRing R] (P Q : Fin 3 → R) (u v : R) : WeierstrassCurve.Jacobian.addZ (u • P) (v • Q) = (u * v) ^ 2 * WeierstrassCurve.Jacobian.addZ P Q

theorem WeierstrassCurve.Jacobian.addZ_of_Z_eq_zero_left {R : Type u} [CommRing R] {P Q : Fin 3 → R} (hPz : P 2 = 0) : WeierstrassCurve.Jacobian.addZ P Q = P 0 * Q 2 * Q 2

theorem WeierstrassCurve.Jacobian.addZ_of_Z_eq_zero_right {R : Type u} [CommRing R] {P Q : Fin 3 → R} (hQz : Q 2 = 0) : WeierstrassCurve.Jacobian.addZ P Q = -(Q 0 * P 2) * P 2

theorem WeierstrassCurve.Jacobian.addZ_of_X_eq {R : Type u} [CommRing R] {P Q : Fin 3 → R} (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) : WeierstrassCurve.Jacobian.addZ P Q = 0

theorem WeierstrassCurve.Jacobian.addZ_ne_zero_of_X_ne {R : Type u} [CommRing R] {P Q : Fin 3 → R} (hx : P 0 * Q 2 ^ 2 ≠ Q 0 * P 2 ^ 2) : WeierstrassCurve.Jacobian.addZ P Q ≠ 0

theorem WeierstrassCurve.Jacobian.isUnit_addZ_of_X_ne {F : Type v} [Field F] {P Q : Fin 3 → F} (hx : P 0 * Q 2 ^ 2 ≠ Q 0 * P 2 ^ 2) : IsUnit (WeierstrassCurve.Jacobian.addZ P Q)

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

The $X$-coordinate of the addition of two distinct point representatives.

Equations

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

theorem WeierstrassCurve.Jacobian.addX_self {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P : Fin 3 → R} (hP : W'.Equation P) : W'.addX P P = 0

theorem WeierstrassCurve.Jacobian.addX_eq' {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) : W'.addX P Q * (P 2 * Q 2) ^ 2 = (P 1 * Q 2 ^ 3 - Q 1 * P 2 ^ 3) ^ 2 + W'.a₁ * (P 1 * Q 2 ^ 3 - Q 1 * P 2 ^ 3) * P 2 * Q 2 * WeierstrassCurve.Jacobian.addZ P Q - W'.a₂ * P 2 ^ 2 * Q 2 ^ 2 * WeierstrassCurve.Jacobian.addZ P Q ^ 2 - P 0 * Q 2 ^ 2 * WeierstrassCurve.Jacobian.addZ P Q ^ 2 - Q 0 * P 2 ^ 2 * WeierstrassCurve.Jacobian.addZ P Q ^ 2

theorem WeierstrassCurve.Jacobian.addX_eq {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) : W.addX P Q = ((P 1 * Q 2 ^ 3 - Q 1 * P 2 ^ 3) ^ 2 + W.a₁ * (P 1 * Q 2 ^ 3 - Q 1 * P 2 ^ 3) * P 2 * Q 2 * WeierstrassCurve.Jacobian.addZ P Q - W.a₂ * P 2 ^ 2 * Q 2 ^ 2 * WeierstrassCurve.Jacobian.addZ P Q ^ 2 - P 0 * Q 2 ^ 2 * WeierstrassCurve.Jacobian.addZ P Q ^ 2 - Q 0 * P 2 ^ 2 * WeierstrassCurve.Jacobian.addZ P Q ^ 2) / (P 2 * Q 2) ^ 2

theorem WeierstrassCurve.Jacobian.addX_smul {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] (P Q : Fin 3 → R) (u v : R) : W'.addX (u • P) (v • Q) = ((u * v) ^ 2) ^ 2 * W'.addX P Q

theorem WeierstrassCurve.Jacobian.addX_of_Z_eq_zero_left {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P Q : Fin 3 → R} (hPz : P 2 = 0) : W'.addX P Q = (P 0 * Q 2) ^ 2 * Q 0

theorem WeierstrassCurve.Jacobian.addX_of_Z_eq_zero_right {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P Q : Fin 3 → R} (hQz : Q 2 = 0) : W'.addX P Q = (-(Q 0 * P 2)) ^ 2 * P 0

theorem WeierstrassCurve.Jacobian.addX_of_X_eq' {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) : W'.addX P Q * (P 2 * Q 2) ^ 2 = (P 1 * Q 2 ^ 3 - Q 1 * P 2 ^ 3) ^ 2

theorem WeierstrassCurve.Jacobian.addX_of_X_eq {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) : W.addX P Q = WeierstrassCurve.Jacobian.addU P Q ^ 2

theorem WeierstrassCurve.Jacobian.addX_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 ≠ Q 0 * P 2 ^ 2) : W.addX P Q / WeierstrassCurve.Jacobian.addZ P Q ^ 2 = W.toAffine.addX (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3))

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

The $Y$-coordinate of the negated addition of two distinct point representatives.

Equations

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

theorem WeierstrassCurve.Jacobian.negAddY_self {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P : Fin 3 → R} : W'.negAddY P P = 0

theorem WeierstrassCurve.Jacobian.negAddY_eq' {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P Q : Fin 3 → R} : W'.negAddY P Q * (P 2 * Q 2) ^ 3 = (P 1 * Q 2 ^ 3 - Q 1 * P 2 ^ 3) * (W'.addX P Q * (P 2 * Q 2) ^ 2 - P 0 * Q 2 ^ 2 * WeierstrassCurve.Jacobian.addZ P Q ^ 2) + P 1 * Q 2 ^ 3 * WeierstrassCurve.Jacobian.addZ P Q ^ 3

theorem WeierstrassCurve.Jacobian.negAddY_eq {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) : W.negAddY P Q = ((P 1 * Q 2 ^ 3 - Q 1 * P 2 ^ 3) * (W.addX P Q * (P 2 * Q 2) ^ 2 - P 0 * Q 2 ^ 2 * WeierstrassCurve.Jacobian.addZ P Q ^ 2) + P 1 * Q 2 ^ 3 * WeierstrassCurve.Jacobian.addZ P Q ^ 3) / (P 2 * Q 2) ^ 3

theorem WeierstrassCurve.Jacobian.negAddY_smul {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] (P Q : Fin 3 → R) (u v : R) : W'.negAddY (u • P) (v • Q) = ((u * v) ^ 2) ^ 3 * W'.negAddY P Q

theorem WeierstrassCurve.Jacobian.negAddY_of_Z_eq_zero_left {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hPz : P 2 = 0) : W'.negAddY P Q = (P 0 * Q 2) ^ 3 * W'.negY Q

theorem WeierstrassCurve.Jacobian.negAddY_of_Z_eq_zero_right {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P Q : Fin 3 → R} (hQ : W'.Equation Q) (hQz : Q 2 = 0) : W'.negAddY P Q = (-(Q 0 * P 2)) ^ 3 * W'.negY P

theorem WeierstrassCurve.Jacobian.negAddY_of_X_eq' {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) : W'.negAddY P Q * (P 2 * Q 2) ^ 3 = (P 1 * Q 2 ^ 3 - Q 1 * P 2 ^ 3) ^ 3

theorem WeierstrassCurve.Jacobian.negAddY_of_X_eq {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) : W.negAddY P Q = (-WeierstrassCurve.Jacobian.addU P Q) ^ 3

theorem WeierstrassCurve.Jacobian.negAddY_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 ≠ Q 0 * P 2 ^ 2) : W.negAddY P Q / WeierstrassCurve.Jacobian.addZ P Q ^ 3 = W.toAffine.negAddY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3))

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

The $Y$-coordinate of the addition of two distinct point representatives.

Equations

• W'.addY P Q = W'.negY ![W'.addX P Q, W'.negAddY P Q, WeierstrassCurve.Jacobian.addZ P Q]

theorem WeierstrassCurve.Jacobian.addY_self {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P : Fin 3 → R} (hP : W'.Equation P) : W'.addY P P = 0

theorem WeierstrassCurve.Jacobian.addY_smul {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] (P Q : Fin 3 → R) (u v : R) : W'.addY (u • P) (v • Q) = ((u * v) ^ 2) ^ 3 * W'.addY P Q

theorem WeierstrassCurve.Jacobian.addY_of_Z_eq_zero_left {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hPz : P 2 = 0) : W'.addY P Q = (P 0 * Q 2) ^ 3 * Q 1

theorem WeierstrassCurve.Jacobian.addY_of_Z_eq_zero_right {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P Q : Fin 3 → R} (hQ : W'.Equation Q) (hQz : Q 2 = 0) : W'.addY P Q = (-(Q 0 * P 2)) ^ 3 * P 1

theorem WeierstrassCurve.Jacobian.addY_of_X_eq' {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) : W'.addY P Q * (P 2 * Q 2) ^ 3 = (-(P 1 * Q 2 ^ 3 - Q 1 * P 2 ^ 3)) ^ 3

theorem WeierstrassCurve.Jacobian.addY_of_X_eq {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) : W.addY P Q = WeierstrassCurve.Jacobian.addU P Q ^ 3

theorem WeierstrassCurve.Jacobian.addY_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 ≠ Q 0 * P 2 ^ 2) : W.addY P Q / WeierstrassCurve.Jacobian.addZ P Q ^ 3 = W.toAffine.addY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3))

noncomputable def WeierstrassCurve.Jacobian.addXYZ {R : Type u} (W' : WeierstrassCurve.Jacobian R) [CommRing R] (P Q : Fin 3 → R) : Fin 3 → R

The coordinates of the addition of two distinct point representatives.

Equations

• W'.addXYZ P Q = ![W'.addX P Q, W'.addY P Q, WeierstrassCurve.Jacobian.addZ P Q]

theorem WeierstrassCurve.Jacobian.addXYZ_self {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P : Fin 3 → R} (hP : W'.Equation P) : W'.addXYZ P P = ![0, 0, 0]

theorem WeierstrassCurve.Jacobian.addXYZ_smul {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] (P Q : Fin 3 → R) (u v : R) : W'.addXYZ (u • P) (v • Q) = (u * v) ^ 2 • W'.addXYZ P Q

theorem WeierstrassCurve.Jacobian.addXYZ_of_Z_eq_zero_left {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hPz : P 2 = 0) : W'.addXYZ P Q = (P 0 * Q 2) • Q

theorem WeierstrassCurve.Jacobian.addXYZ_of_Z_eq_zero_right {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P Q : Fin 3 → R} (hQ : W'.Equation Q) (hQz : Q 2 = 0) : W'.addXYZ P Q = -(Q 0 * P 2) • P

theorem WeierstrassCurve.Jacobian.addXYZ_of_X_eq {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) : W.addXYZ P Q = WeierstrassCurve.Jacobian.addU P Q • ![1, 1, 0]

theorem WeierstrassCurve.Jacobian.addXYZ_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 ≠ Q 0 * P 2 ^ 2) : W.addXYZ P Q = WeierstrassCurve.Jacobian.addZ P Q • ![W.toAffine.addX (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)), W.toAffine.addY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)), 1]

Negation on point representatives

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

The negation of a point representative.

Equations

• W'.neg P = ![P 0, W'.negY P, P 2]

theorem WeierstrassCurve.Jacobian.neg_smul {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] (P : Fin 3 → R) (u : R) : W'.neg (u • P) = u • W'.neg P

theorem WeierstrassCurve.Jacobian.neg_smul_equiv {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] (P : Fin 3 → R) {u : R} (hu : IsUnit u) : W'.neg (u • P) ≈ W'.neg P

theorem WeierstrassCurve.Jacobian.neg_equiv {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P Q : Fin 3 → R} (h : P ≈ Q) : W'.neg P ≈ W'.neg Q

theorem WeierstrassCurve.Jacobian.neg_of_Z_eq_zero' {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P : Fin 3 → R} (hPz : P 2 = 0) : W'.neg P = ![P 0, -P 1, 0]

theorem WeierstrassCurve.Jacobian.neg_of_Z_eq_zero {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} (hP : W.Nonsingular P) (hPz : P 2 = 0) : W.neg P = -(P 1 / P 0) • ![1, 1, 0]

theorem WeierstrassCurve.Jacobian.neg_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} (hPz : P 2 ≠ 0) : W.neg P = P 2 • ![P 0 / P 2 ^ 2, W.toAffine.negY (P 0 / P 2 ^ 2) (P 1 / P 2 ^ 3), 1]

theorem WeierstrassCurve.Jacobian.nonsingular_neg {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} (hP : W.Nonsingular P) : W.Nonsingular (W.neg P)

theorem WeierstrassCurve.Jacobian.addZ_neg {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P : Fin 3 → R} : WeierstrassCurve.Jacobian.addZ P (W'.neg P) = 0

theorem WeierstrassCurve.Jacobian.addX_neg {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P : Fin 3 → R} (hP : W'.Equation P) : W'.addX P (W'.neg P) = W'.dblZ P ^ 2

theorem WeierstrassCurve.Jacobian.negAddY_neg {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P : Fin 3 → R} (hP : W'.Equation P) : W'.negAddY P (W'.neg P) = W'.dblZ P ^ 3

theorem WeierstrassCurve.Jacobian.addY_neg {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P : Fin 3 → R} (hP : W'.Equation P) : W'.addY P (W'.neg P) = -W'.dblZ P ^ 3

theorem WeierstrassCurve.Jacobian.addXYZ_neg {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P : Fin 3 → R} (hP : W'.Equation P) : W'.addXYZ P (W'.neg P) = -W'.dblZ P • ![1, 1, 0]

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

The negation of a point class. If P is a point representative, then W'.negMap ⟦P⟧ is definitionally equivalent to W'.neg P.

Equations

• W'.negMap P = Quotient.map W'.neg ⋯ P

theorem WeierstrassCurve.Jacobian.negMap_eq {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P : Fin 3 → R} : W'.negMap ⟦P⟧ = ⟦W'.neg P⟧

theorem WeierstrassCurve.Jacobian.negMap_of_Z_eq_zero {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} (hP : W.Nonsingular P) (hPz : P 2 = 0) : W.negMap ⟦P⟧ = ⟦![1, 1, 0]⟧

theorem WeierstrassCurve.Jacobian.negMap_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} (hPz : P 2 ≠ 0) : W.negMap ⟦P⟧ = ⟦![P 0 / P 2 ^ 2, W.toAffine.negY (P 0 / P 2 ^ 2) (P 1 / P 2 ^ 3), 1]⟧

theorem WeierstrassCurve.Jacobian.nonsingularLift_negMap {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P : WeierstrassCurve.Jacobian.PointClass F} (hP : W.NonsingularLift P) : W.NonsingularLift (W.negMap P)

Addition on point representatives

noncomputable def WeierstrassCurve.Jacobian.add {R : Type u} (W' : WeierstrassCurve.Jacobian R) [CommRing R] (P Q : Fin 3 → R) : Fin 3 → R

The addition of two point representatives.

Equations

• W'.add P Q = if P ≈ Q then W'.dblXYZ P else W'.addXYZ P Q

theorem WeierstrassCurve.Jacobian.add_of_equiv {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P Q : Fin 3 → R} (h : P ≈ Q) : W'.add P Q = W'.dblXYZ P

theorem WeierstrassCurve.Jacobian.add_smul_of_equiv {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P Q : Fin 3 → R} (h : P ≈ Q) {u v : R} (hu : IsUnit u) (hv : IsUnit v) : W'.add (u • P) (v • Q) = u ^ 4 • W'.add P Q

theorem WeierstrassCurve.Jacobian.add_self {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] (P : Fin 3 → R) : W'.add P P = W'.dblXYZ P

theorem WeierstrassCurve.Jacobian.add_of_eq {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P Q : Fin 3 → R} (h : P = Q) : W'.add P Q = W'.dblXYZ P

theorem WeierstrassCurve.Jacobian.add_of_not_equiv {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P Q : Fin 3 → R} (h : ¬P ≈ Q) : W'.add P Q = W'.addXYZ P Q

theorem WeierstrassCurve.Jacobian.add_smul_of_not_equiv {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P Q : Fin 3 → R} (h : ¬P ≈ Q) {u v : R} (hu : IsUnit u) (hv : IsUnit v) : W'.add (u • P) (v • Q) = (u * v) ^ 2 • W'.add P Q

theorem WeierstrassCurve.Jacobian.add_smul_equiv {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] (P Q : Fin 3 → R) {u v : R} (hu : IsUnit u) (hv : IsUnit v) : W'.add (u • P) (v • Q) ≈ W'.add P Q

theorem WeierstrassCurve.Jacobian.add_equiv {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P P' Q Q' : Fin 3 → R} (hP : P ≈ P') (hQ : Q ≈ Q') : W'.add P Q ≈ W'.add P' Q'

theorem WeierstrassCurve.Jacobian.add_of_Z_eq_zero {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) (hPz : P 2 = 0) (hQz : Q 2 = 0) : W.add P Q = P 0 ^ 2 • ![1, 1, 0]

theorem WeierstrassCurve.Jacobian.add_of_Z_eq_zero_left {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hPz : P 2 = 0) (hQz : Q 2 ≠ 0) : W'.add P Q = (P 0 * Q 2) • Q

theorem WeierstrassCurve.Jacobian.add_of_Z_eq_zero_right {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P Q : Fin 3 → R} (hQ : W'.Equation Q) (hPz : P 2 ≠ 0) (hQz : Q 2 = 0) : W'.add P Q = -(Q 0 * P 2) • P

theorem WeierstrassCurve.Jacobian.add_of_Y_eq {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) (hy : P 1 * Q 2 ^ 3 = Q 1 * P 2 ^ 3) (hy' : P 1 * Q 2 ^ 3 = W.negY Q * P 2 ^ 3) : W.add P Q = W.dblU P • ![1, 1, 0]

theorem WeierstrassCurve.Jacobian.add_of_Y_ne {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) (hy : P 1 * Q 2 ^ 3 ≠ Q 1 * P 2 ^ 3) : W.add P Q = WeierstrassCurve.Jacobian.addU P Q • ![1, 1, 0]

theorem WeierstrassCurve.Jacobian.add_of_Y_ne' {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) (hy : P 1 * Q 2 ^ 3 ≠ W.negY Q * P 2 ^ 3) : W.add P Q = W.dblZ P • ![W.toAffine.addX (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)), W.toAffine.addY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)), 1]

theorem WeierstrassCurve.Jacobian.add_of_X_ne {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 ≠ Q 0 * P 2 ^ 2) : W.add P Q = WeierstrassCurve.Jacobian.addZ P Q • ![W.toAffine.addX (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)), W.toAffine.addY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)), 1]

theorem WeierstrassCurve.Jacobian.nonsingular_add {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) : W.Nonsingular (W.add P Q)

noncomputable def WeierstrassCurve.Jacobian.addMap {R : Type u} (W' : WeierstrassCurve.Jacobian R) [CommRing R] (P Q : WeierstrassCurve.Jacobian.PointClass R) : WeierstrassCurve.Jacobian.PointClass R

The addition of two point classes. If P is a point representative, then W.addMap ⟦P⟧ ⟦Q⟧ is definitionally equivalent to W.add P Q.

Equations

• W'.addMap P Q = Quotient.map₂ W'.add ⋯ P Q

theorem WeierstrassCurve.Jacobian.addMap_eq {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] (P Q : Fin 3 → R) : W'.addMap ⟦P⟧ ⟦Q⟧ = ⟦W'.add P Q⟧

theorem WeierstrassCurve.Jacobian.addMap_of_Z_eq_zero_left {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} {Q : WeierstrassCurve.Jacobian.PointClass F} (hP : W.Nonsingular P) (hQ : W.NonsingularLift Q) (hPz : P 2 = 0) : W.addMap ⟦P⟧ Q = Q

theorem WeierstrassCurve.Jacobian.addMap_of_Z_eq_zero_right {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P : WeierstrassCurve.Jacobian.PointClass F} {Q : Fin 3 → F} (hP : W.NonsingularLift P) (hQ : W.Nonsingular Q) (hQz : Q 2 = 0) : W.addMap P ⟦Q⟧ = P

theorem WeierstrassCurve.Jacobian.addMap_of_Y_eq {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Equation Q) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) (hy' : P 1 * Q 2 ^ 3 = W.negY Q * P 2 ^ 3) : W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![1, 1, 0]⟧

theorem WeierstrassCurve.Jacobian.addMap_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hxy : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 → P 1 * Q 2 ^ 3 ≠ W.negY Q * P 2 ^ 3) : W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![W.toAffine.addX (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)), W.toAffine.addY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)), 1]⟧

theorem WeierstrassCurve.Jacobian.nonsingularLift_addMap {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : WeierstrassCurve.Jacobian.PointClass F} (hP : W.NonsingularLift P) (hQ : W.NonsingularLift Q) : W.NonsingularLift (W.addMap P Q)

Nonsingular rational points

structure WeierstrassCurve.Jacobian.Point {R : Type u} (W' : WeierstrassCurve.Jacobian R) [CommRing R] : Type u

A nonsingular rational point on W'.

• point : WeierstrassCurve.Jacobian.PointClass R

  The point class underlying a nonsingular rational point on W'.

• nonsingular : W'.NonsingularLift self.point

  The nonsingular condition underlying a nonsingular rational point on W'.

theorem WeierstrassCurve.Jacobian.Point.ext {R : Type u} {W' : WeierstrassCurve.Jacobian R} {inst✝ : CommRing R} {x y : W'.Point} (point : x.point = y.point) : x = y

theorem WeierstrassCurve.Jacobian.Point.mk_point {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {P : WeierstrassCurve.Jacobian.PointClass R} (h : W'.NonsingularLift P) : (WeierstrassCurve.Jacobian.Point.mk h).point = P

instance WeierstrassCurve.Jacobian.Point.instZeroPoint {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] [Nontrivial R] : Zero W'.Point

Equations

• WeierstrassCurve.Jacobian.Point.instZeroPoint = { zero := WeierstrassCurve.Jacobian.Point.mk ⋯ }

theorem WeierstrassCurve.Jacobian.Point.zero_def {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] [Nontrivial R] : 0 = WeierstrassCurve.Jacobian.Point.mk ⋯

theorem WeierstrassCurve.Jacobian.Point.zero_point {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] [Nontrivial R] : WeierstrassCurve.Jacobian.Point.point 0 = ⟦![1, 1, 0]⟧

def WeierstrassCurve.Jacobian.Point.fromAffine {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] [Nontrivial R] : W'.toAffine.Point → W'.Point

The map from a nonsingular rational point on a Weierstrass curve W' in affine coordinates to the corresponding nonsingular rational point on W' in Jacobian coordinates.

Equations

• WeierstrassCurve.Jacobian.Point.fromAffine WeierstrassCurve.Affine.Point.zero = 0
• WeierstrassCurve.Jacobian.Point.fromAffine (WeierstrassCurve.Affine.Point.some h) = WeierstrassCurve.Jacobian.Point.mk ⋯

theorem WeierstrassCurve.Jacobian.Point.fromAffine_zero {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] [Nontrivial R] : WeierstrassCurve.Jacobian.Point.fromAffine 0 = 0

theorem WeierstrassCurve.Jacobian.Point.fromAffine_some {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] [Nontrivial R] {X Y : R} (h : W'.toAffine.Nonsingular X Y) : WeierstrassCurve.Jacobian.Point.fromAffine (WeierstrassCurve.Affine.Point.some h) = WeierstrassCurve.Jacobian.Point.mk ⋯

theorem WeierstrassCurve.Jacobian.Point.fromAffine_ne_zero {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] [Nontrivial R] {X Y : R} (h : W'.toAffine.Nonsingular X Y) : WeierstrassCurve.Jacobian.Point.fromAffine (WeierstrassCurve.Affine.Point.some h) ≠ 0

def WeierstrassCurve.Jacobian.Point.neg {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} (P : W.Point) : W.Point

The negation of a nonsingular rational point on W. Given a nonsingular rational point P on W, use -P instead of neg P.

Equations

• P.neg = WeierstrassCurve.Jacobian.Point.mk ⋯

instance WeierstrassCurve.Jacobian.Point.instNegPoint {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} : Neg W.Point

Equations

• WeierstrassCurve.Jacobian.Point.instNegPoint = { neg := WeierstrassCurve.Jacobian.Point.neg }

theorem WeierstrassCurve.Jacobian.Point.neg_def {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} (P : W.Point) : -P = P.neg

theorem WeierstrassCurve.Jacobian.Point.neg_point {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} (P : W.Point) : (-P).point = W.negMap P.point

noncomputable def WeierstrassCurve.Jacobian.Point.add {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} (P Q : W.Point) : W.Point

The addition of two nonsingular rational points on W. Given two nonsingular rational points P and Q on W, use P + Q instead of add P Q.

Equations

• P.add Q = WeierstrassCurve.Jacobian.Point.mk ⋯

noncomputable instance WeierstrassCurve.Jacobian.Point.instAddPoint {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} : Add W.Point

Equations

• WeierstrassCurve.Jacobian.Point.instAddPoint = { add := WeierstrassCurve.Jacobian.Point.add }

theorem WeierstrassCurve.Jacobian.Point.add_def {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} (P Q : W.Point) : P + Q = P.add Q

theorem WeierstrassCurve.Jacobian.Point.add_point {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} (P Q : W.Point) : (P + Q).point = W.addMap P.point Q.point

Equivalence with affine coordinates

noncomputable def WeierstrassCurve.Jacobian.Point.toAffine {F : Type v} [Field F] (W : WeierstrassCurve.Jacobian F) (P : Fin 3 → F) : W.toAffine.Point

The map from a point representative that is nonsingular on a Weierstrass curve W in Jacobian coordinates to the corresponding nonsingular rational point on W in affine coordinates.

Equations

• WeierstrassCurve.Jacobian.Point.toAffine W P = if hP : W.Nonsingular P ∧ P 2 ≠ 0 then WeierstrassCurve.Affine.Point.some ⋯ else 0

theorem WeierstrassCurve.Jacobian.Point.toAffine_of_singular {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} (hP : ¬W.Nonsingular P) : WeierstrassCurve.Jacobian.Point.toAffine W P = 0

theorem WeierstrassCurve.Jacobian.Point.toAffine_of_Z_eq_zero {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} (hPz : P 2 = 0) : WeierstrassCurve.Jacobian.Point.toAffine W P = 0

theorem WeierstrassCurve.Jacobian.Point.toAffine_zero {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} : WeierstrassCurve.Jacobian.Point.toAffine W ![1, 1, 0] = 0

theorem WeierstrassCurve.Jacobian.Point.toAffine_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} (hP : W.Nonsingular P) (hPz : P 2 ≠ 0) : WeierstrassCurve.Jacobian.Point.toAffine W P = WeierstrassCurve.Affine.Point.some ⋯

theorem WeierstrassCurve.Jacobian.Point.toAffine_some {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {X Y : F} (h : W.Nonsingular ![X, Y, 1]) : WeierstrassCurve.Jacobian.Point.toAffine W ![X, Y, 1] = WeierstrassCurve.Affine.Point.some ⋯

theorem WeierstrassCurve.Jacobian.Point.toAffine_smul {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} (P : Fin 3 → F) {u : F} (hu : IsUnit u) : WeierstrassCurve.Jacobian.Point.toAffine W (u • P) = WeierstrassCurve.Jacobian.Point.toAffine W P

theorem WeierstrassCurve.Jacobian.Point.toAffine_of_equiv {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (h : P ≈ Q) : WeierstrassCurve.Jacobian.Point.toAffine W P = WeierstrassCurve.Jacobian.Point.toAffine W Q

theorem WeierstrassCurve.Jacobian.Point.toAffine_neg {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} (hP : W.Nonsingular P) : WeierstrassCurve.Jacobian.Point.toAffine W (W.neg P) = -WeierstrassCurve.Jacobian.Point.toAffine W P

theorem WeierstrassCurve.Jacobian.Point.toAffine_add {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) : WeierstrassCurve.Jacobian.Point.toAffine W (W.add P Q) = WeierstrassCurve.Jacobian.Point.toAffine W P + WeierstrassCurve.Jacobian.Point.toAffine W Q

noncomputable def WeierstrassCurve.Jacobian.Point.toAffineLift {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} (P : W.Point) : W.toAffine.Point

The map from a nonsingular rational point on a Weierstrass curve W in Jacobian coordinates to the corresponding nonsingular rational point on W in affine coordinates.

Equations

• P.toAffineLift = Quotient.lift (fun (x : Fin 3 → F) => WeierstrassCurve.Jacobian.Point.toAffine W x) ⋯ P.point

theorem WeierstrassCurve.Jacobian.Point.toAffineLift_eq {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} (hP : W.NonsingularLift ⟦P⟧) : (WeierstrassCurve.Jacobian.Point.mk hP).toAffineLift = WeierstrassCurve.Jacobian.Point.toAffine W P

theorem WeierstrassCurve.Jacobian.Point.toAffineLift_of_Z_eq_zero {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} (hP : W.NonsingularLift ⟦P⟧) (hPz : P 2 = 0) : (WeierstrassCurve.Jacobian.Point.mk hP).toAffineLift = 0

theorem WeierstrassCurve.Jacobian.Point.toAffineLift_zero {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} : WeierstrassCurve.Jacobian.Point.toAffineLift 0 = 0

theorem WeierstrassCurve.Jacobian.Point.toAffineLift_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} {hP : W.NonsingularLift ⟦P⟧} (hPz : P 2 ≠ 0) : (WeierstrassCurve.Jacobian.Point.mk hP).toAffineLift = WeierstrassCurve.Affine.Point.some ⋯

theorem WeierstrassCurve.Jacobian.Point.toAffineLift_some {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} {X Y : F} (h : W.NonsingularLift ⟦![X, Y, 1]⟧) : (WeierstrassCurve.Jacobian.Point.mk h).toAffineLift = WeierstrassCurve.Affine.Point.some ⋯

theorem WeierstrassCurve.Jacobian.Point.toAffineLift_neg {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} (P : W.Point) : (-P).toAffineLift = -P.toAffineLift

theorem WeierstrassCurve.Jacobian.Point.toAffineLift_add {F : Type v} [Field F] {W : WeierstrassCurve.Jacobian F} (P Q : W.Point) : (P + Q).toAffineLift = P.toAffineLift + Q.toAffineLift

noncomputable def WeierstrassCurve.Jacobian.Point.toAffineAddEquiv {F : Type v} [Field F] (W : WeierstrassCurve.Jacobian F) : W.Point ≃+ W.toAffine.Point

The equivalence between the nonsingular rational points on a Weierstrass curve W in Jacobian coordinates with the nonsingular rational points on W in affine coordinates.

Equations

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

@[simp]

theorem WeierstrassCurve.Jacobian.Point.toAffineAddEquiv_apply {F : Type v} [Field F] (W : WeierstrassCurve.Jacobian F) (P : W.Point) : (WeierstrassCurve.Jacobian.Point.toAffineAddEquiv W) P = P.toAffineLift

@[simp]

theorem WeierstrassCurve.Jacobian.Point.toAffineAddEquiv_symm_apply {F : Type v} [Field F] (W : WeierstrassCurve.Jacobian F) (a✝ : W.toAffine.Point) : (WeierstrassCurve.Jacobian.Point.toAffineAddEquiv W).symm a✝ = WeierstrassCurve.Jacobian.Point.fromAffine a✝

theorem WeierstrassCurve.Jacobian.map_smul {R : Type u} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (P : Fin 3 → R) (u : R) : ⇑f ∘ (u • P) = f u • ⇑f ∘ P

@[simp]

theorem WeierstrassCurve.Jacobian.map_addZ {R : Type u} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (P Q : Fin 3 → R) : WeierstrassCurve.Jacobian.addZ (⇑f ∘ P) (⇑f ∘ Q) = f (WeierstrassCurve.Jacobian.addZ P Q)

@[simp]

theorem WeierstrassCurve.Jacobian.map_addX {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (P Q : Fin 3 → R) : WeierstrassCurve.Jacobian.addX (WeierstrassCurve.map W' f) (⇑f ∘ P) (⇑f ∘ Q) = f (W'.addX P Q)

@[simp]

theorem WeierstrassCurve.Jacobian.map_negAddY {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (P Q : Fin 3 → R) : WeierstrassCurve.Jacobian.negAddY (WeierstrassCurve.map W' f) (⇑f ∘ P) (⇑f ∘ Q) = f (W'.negAddY P Q)

@[simp]

theorem WeierstrassCurve.Jacobian.map_negY {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (P : Fin 3 → R) : WeierstrassCurve.Jacobian.negY (WeierstrassCurve.map W' f) (⇑f ∘ P) = f (W'.negY P)

@[simp]

theorem WeierstrassCurve.Jacobian.map_neg {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (P : Fin 3 → R) : WeierstrassCurve.Jacobian.neg (WeierstrassCurve.map W' f) (⇑f ∘ P) = ⇑f ∘ W'.neg P

@[simp]

theorem WeierstrassCurve.Jacobian.map_addY {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (P Q : Fin 3 → R) : WeierstrassCurve.Jacobian.addY (WeierstrassCurve.map W' f) (⇑f ∘ P) (⇑f ∘ Q) = f (W'.addY P Q)

@[simp]

theorem WeierstrassCurve.Jacobian.map_addXYZ {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (P Q : Fin 3 → R) : WeierstrassCurve.Jacobian.addXYZ (WeierstrassCurve.map W' f) (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W'.addXYZ P Q

theorem WeierstrassCurve.Jacobian.map_polynomial {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) : (WeierstrassCurve.map W' f).toJacobian.polynomial = (MvPolynomial.map f) W'.polynomial

theorem WeierstrassCurve.Jacobian.map_polynomialX {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) : (WeierstrassCurve.map W' f).toJacobian.polynomialX = (MvPolynomial.map f) W'.polynomialX

theorem WeierstrassCurve.Jacobian.map_polynomialY {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) : (WeierstrassCurve.map W' f).toJacobian.polynomialY = (MvPolynomial.map f) W'.polynomialY

theorem WeierstrassCurve.Jacobian.map_polynomialZ {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) : (WeierstrassCurve.map W' f).toJacobian.polynomialZ = (MvPolynomial.map f) W'.polynomialZ

@[simp]

theorem WeierstrassCurve.Jacobian.map_dblZ {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (P : Fin 3 → R) : WeierstrassCurve.Jacobian.dblZ (WeierstrassCurve.map W' f) (⇑f ∘ P) = f (W'.dblZ P)

@[simp]

theorem WeierstrassCurve.Jacobian.map_dblU {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (P : Fin 3 → R) : WeierstrassCurve.Jacobian.dblU (WeierstrassCurve.map W' f) (⇑f ∘ P) = f (W'.dblU P)

@[simp]

theorem WeierstrassCurve.Jacobian.map_dblX {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (P : Fin 3 → R) : WeierstrassCurve.Jacobian.dblX (WeierstrassCurve.map W' f) (⇑f ∘ P) = f (W'.dblX P)

@[simp]

theorem WeierstrassCurve.Jacobian.map_negDblY {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (P : Fin 3 → R) : WeierstrassCurve.Jacobian.negDblY (WeierstrassCurve.map W' f) (⇑f ∘ P) = f (W'.negDblY P)

@[simp]

theorem WeierstrassCurve.Jacobian.map_dblY {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (P : Fin 3 → R) : WeierstrassCurve.Jacobian.dblY (WeierstrassCurve.map W' f) (⇑f ∘ P) = f (W'.dblY P)

@[simp]

theorem WeierstrassCurve.Jacobian.map_dblXYZ {R : Type u} {W' : WeierstrassCurve.Jacobian R} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (P : Fin 3 → R) : WeierstrassCurve.Jacobian.dblXYZ (WeierstrassCurve.map W' f) (⇑f ∘ P) = ⇑f ∘ W'.dblXYZ P

@[reducible, inline]

abbrev WeierstrassCurve.Affine.Point.toJacobian {R : Type u} [CommRing R] [Nontrivial R] {W : WeierstrassCurve.Affine R} (P : W.Point) : (WeierstrassCurve.toJacobian W).Point

An abbreviation for WeierstrassCurve.Jacobian.Point.fromAffine for dot notation.

Equations

• P.toJacobian = WeierstrassCurve.Jacobian.Point.fromAffine P