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.lean.

Mathematical background

A point on the projective plane over a commutative ring R with weights (2, 3, 1) is an equivalence class [x : y : z] of triples (x, y, z) ≠ (0, 0, 0) of elements in R such that (x, y, z) ∼ (x', y', z') if there is some unit u in Rˣ with (x, y, z) = (u²x', u³y', uz').

Let W be a Weierstrass curve over a field F with coefficients aᵢ. A Jacobian point is a point on the projective plane over F with weights (2, 3, 1) satisfying the (2, 3, 1)-homogeneous Weierstrass equation W(X, Y, Z) = 0 in Jacobian coordinates, where W(X, Y, Z) := Y² + a₁XYZ + a₃YZ³ - (X³ + a₂X²Z² + a₄XZ⁴ + a₆Z⁶). It is nonsingular if its partial derivatives W_X(x, y, z), W_Y(x, y, z), and W_Z(x, y, z) do not vanish simultaneously.

The nonsingular Jacobian points on W can be given negation and addition operations defined by an analogue of the secant-and-tangent process in Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean, but the polynomials involved are (2, 3, 1)-homogeneous, so any instances of division become multiplication in the Z-coordinate. Most computational proofs are immediate from their analogous proofs for affine coordinates. They can be endowed with an group law, which is uniquely determined by these formulae and follows from an equivalence with the nonsingular points W⟮F⟯ in affine coordinates.

Main definitions

• WeierstrassCurve.Jacobian.PointClass: the equivalence class of a point representative.

• WeierstrassCurve.Jacobian.Nonsingular: the nonsingular condition on a point representative.

• WeierstrassCurve.Jacobian.NonsingularLift: the nonsingular condition on a point class.

• WeierstrassCurve.Jacobian.negY: the Y-coordinate of -P.

• WeierstrassCurve.Jacobian.dblZ: the Z-coordinate of 2 • P.

• WeierstrassCurve.Jacobian.dblX: the X-coordinate of 2 • P.

• WeierstrassCurve.Jacobian.negDblY: the Y-coordinate of -(2 • P).

• WeierstrassCurve.Jacobian.dblY: the Y-coordinate of 2 • P.

• WeierstrassCurve.Jacobian.addZ: the Z-coordinate of P + Q.

• WeierstrassCurve.Jacobian.addX: the X-coordinate of P + Q.

• WeierstrassCurve.Jacobian.negAddY: the Y-coordinate of -(P + Q).

• WeierstrassCurve.Jacobian.addY: the Y-coordinate of P + Q.

• WeierstrassCurve.Jacobian.neg: the negation of a point representative.

• WeierstrassCurve.Jacobian.negMap: the negation of a point class.

• WeierstrassCurve.Jacobian.add: the addition of two point representatives.

• WeierstrassCurve.Jacobian.addMap: the addition of two point classes.

• WeierstrassCurve.Jacobian.Point: a nonsingular Jacobian point.

• WeierstrassCurve.Jacobian.Point.neg: the negation of a nonsingular Jacobian point.

• WeierstrassCurve.Jacobian.Point.add: the addition of two nonsingular Jacobian points.

• WeierstrassCurve.Jacobian.Point.toAffineAddEquiv: the equivalence between the type of nonsingular Jacobian points with the type of nonsingular points W⟮F⟯ in affine coordinates.

Main statements

• WeierstrassCurve.Jacobian.nonsingular_neg: negation preserves the nonsingular condition.
• WeierstrassCurve.Jacobian.nonsingular_add: addition preserves the nonsingular condition.

Implementation notes

All definitions and lemmas for Weierstrass curves in Jacobian coordinates live in the namespace WeierstrassCurve.Jacobian to distinguish them from those in other coordinates. This is simply an abbreviation for WeierstrassCurve that can be converted using WeierstrassCurve.toJacobian. This can be converted into WeierstrassCurve.Affine using WeierstrassCurve.Jacobian.toAffine. A nonsingular Jacobian point representative can be converted to a nonsingular point in affine coordinates using WeiestrassCurve.Jacobian.Point.toAffine, which lifts to a map on nonsingular Jacobian points using WeiestrassCurve.Jacobian.Point.toAffineLift. Conversely, a nonsingular point in affine coordinates can be converted to a nonsingular Jacobian point using WeierstrassCurve.Jacobian.Point.fromAffine or WeierstrassCurve.Affine.Point.toJacobian.

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. This file makes extensive use of erw to get around this problem. While erw is often an indication of a problem, in this case it is self-contained and should not cause any issues. It would alternatively be possible to add some automation to assist here. Note that W(X, Y, Z) and its partial derivatives are independent of the point representative, and the nonsingularity condition already implies (x, y, z) ≠ (0, 0, 0), so a nonsingular Jacobian point on W can be given by [x : y : z] and the nonsingular condition on any representative.

The definitions of WeierstrassCurve.Jacobian.addX and WeierstrassCurve.Jacobian.negAddY are given explicitly by large polynomials that are homogeneous of degrees 8 and 12 respectively. Clearing the denominators of their corresponding affine rational functions in Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean would give polynomials that are homogeneous of degrees 12 and 18 respectively, so their actual definitions are off by powers of a certain polynomial factor that is homogeneous of degree 2. This factor divides their corresponding affine polynomials only modulo the (2, 3, 1)-homogeneous Weierstrass equation, so their large quotient polynomials are calculated explicitly in a computer algebra system. All of this is done to ensure that the definitions of both WeierstrassCurve.Jacobian.dblXYZ and WeierstrassCurve.Jacobian.addXYZ are (2, 3, 1)-homogeneous of degree 4.

Whenever possible, all changes to documentation and naming of definitions and theorems should be mirrored in Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean.

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 r) : Type r

An abbreviation for a Weierstrass curve in Jacobian coordinates.

Equations

• WeierstrassCurve.Jacobian R = WeierstrassCurve R

@[reducible, inline]

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

The conversion from a Weierstrass curve to Jacobian coordinates.

Equations

• W.toJacobian = W

@[reducible, inline]

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

The conversion from a Weierstrass curve in Jacobian coordinates to affine coordinates.

Equations

• WeierstrassCurve.Jacobian.toAffine W' = W'

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

theorem WeierstrassCurve.Jacobian.fin3_def_ext {R : Type r} (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 r} {S : Type s} (f : R → S) (X Y Z : R) : f ∘ ![X, Y, Z] = ![f X, f Y, f Z]

Jacobian coordinates

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

The scalar multiplication for a Jacobian point representative on a Weierstrass curve.

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 r} [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 r} [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

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

@[deprecated WeierstrassCurve.Jacobian.comp_smul (since := "2025-01-30")]

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

Alias of WeierstrassCurve.Jacobian.comp_smul.

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

The multiplicative action for a Jacobian point representative on a Weierstrass curve.

Equations

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

@[reducible]

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

The equivalence setoid for a Jacobian point representative on a Weierstrass curve.

Equations

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

@[reducible, inline]

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

The equivalence class of a Jacobian point representative on a Weierstrass curve.

Equations

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

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

@[simp]

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

theorem WeierstrassCurve.Jacobian.smul_equiv_smul {R : Type r} [CommRing R] (P Q : Fin 3 → R) {u v : R} (hu : IsUnit u) (hv : IsUnit v) : u • P ≈ v • Q ↔ P ≈ Q

theorem WeierstrassCurve.Jacobian.equiv_iff_eq_of_Z_eq' {R : Type r} [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 r} [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 r} [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 r} [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 r} [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 r} [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 r} [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 r} [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 r} [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 u} [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 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.X_eq_iff {F : Type u} [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 u} [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 r} [CommRing R] (W' : Jacobian R) : MvPolynomial (Fin 3) R

The polynomial W(X, Y, Z) := Y² + a₁XYZ + a₃YZ³ - (X³ + a₂X²Z² + a₄XZ⁴ + a₆Z⁶) associated to a Weierstrass curve W over a ring R in Jacobian coordinates.

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 r} [CommRing R] {W' : 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)

theorem WeierstrassCurve.Jacobian.eval_polynomial_of_Z_ne_zero {F : Type u} [Field F] {W : 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) (toAffine W).polynomial

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

The proposition that a Jacobian point representative (x, y, z) lies in a Weierstrass curve W.

In other words, it satisfies the (2, 3, 1)-homogeneous Weierstrass equation W(X, Y, Z) = 0.

Equations

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

theorem WeierstrassCurve.Jacobian.equation_iff {R : Type r} [CommRing R] {W' : 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) = 0

theorem WeierstrassCurve.Jacobian.equation_smul {R : Type r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian R} : W'.Equation ![1, 1, 0]

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

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

Nonsingular Weierstrass equations

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

The partial derivative W_X(X, Y, Z) with respect to X of the polynomial W(X, Y, Z) associated to a Weierstrass curve W in Jacobian coordinates.

Equations

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

theorem WeierstrassCurve.Jacobian.polynomialX_eq {R : Type r} [CommRing R] {W' : 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 r} [CommRing R] {W' : 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)

theorem WeierstrassCurve.Jacobian.eval_polynomialX_of_Z_ne_zero {F : Type u} [Field F] {W : 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) (toAffine W).polynomialX

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

The partial derivative W_Y(X, Y, Z) with respect to Y of the polynomial W(X, Y, Z) associated to a Weierstrass curve W in Jacobian coordinates.

Equations

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

theorem WeierstrassCurve.Jacobian.polynomialY_eq {R : Type r} [CommRing R] {W' : 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 r} [CommRing R] {W' : 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

theorem WeierstrassCurve.Jacobian.eval_polynomialY_of_Z_ne_zero {F : Type u} [Field F] {W : 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) (toAffine W).polynomialY

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

The partial derivative W_Z(X, Y, Z) with respect to Z of the polynomial W(X, Y, Z) associated to a Weierstrass curve W in Jacobian coordinates.

Equations

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

theorem WeierstrassCurve.Jacobian.polynomialZ_eq {R : Type r} [CommRing R] {W' : 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 r} [CommRing R] {W' : 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 r} [CommRing R] (W' : Jacobian R) (P : Fin 3 → R) : Prop

The proposition that a Jacobian point representative (x, y, z) on a Weierstrass curve W is nonsingular.

In other words, either W_X(x, y, z) ≠ 0, W_Y(x, y, z) ≠ 0, or W_Z(x, y, z) ≠ 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 r} [CommRing R] {W' : 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) ≠ 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 r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian R} [Nontrivial R] : W'.Nonsingular ![1, 1, 0]

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

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

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

theorem WeierstrassCurve.Jacobian.comp_equiv_comp {F : Type u} {K : Type v} [Field F] [Field K] {W : Jacobian F} (f : F →+* K) {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) : ⇑f ∘ P ≈ ⇑f ∘ Q ↔ P ≈ Q

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

The proposition that a Jacobian point class on a Weierstrass curve W is nonsingular.

If P is a Jacobian point representative on W, then W.NonsingularLift ⟦P⟧ is definitionally equivalent to W.Nonsingular P.

Note that this definition is only mathematically accurate for fields.

Equations

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

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

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

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

Negation formulae

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

The Y-coordinate of a representative of -P for a Jacobian point representative P on a Weierstrass curve.

Equations

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

theorem WeierstrassCurve.Jacobian.negY_eq {R : Type r} [CommRing R] {W' : Jacobian R} (X Y Z : R) : W'.negY ![X, Y, Z] = -Y - W'.a₁ * X * Z - W'.a₃ * Z ^ 3

theorem WeierstrassCurve.Jacobian.negY_smul {R : Type r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian R} {P : Fin 3 → R} (hPz : P 2 = 0) : W'.negY P = -P 1

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

theorem WeierstrassCurve.Jacobian.Y_sub_Y_mul_Y_sub_negY {R : Type r} [CommRing R] {W' : Jacobian 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 {R : Type r} [CommRing R] {W' : Jacobian 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 * Q 2 ^ 3 = W'.negY Q * P 2 ^ 3

theorem WeierstrassCurve.Jacobian.Y_eq_of_Y_ne' {R : Type r} [CommRing R] {W' : Jacobian 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 * Q 2 ^ 3 = Q 1 * P 2 ^ 3

theorem WeierstrassCurve.Jacobian.Y_eq_iff' {F : Type u} [Field F] {W : 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 = (toAffine W).negY (Q 0 / Q 2 ^ 2) (Q 1 / Q 2 ^ 3)

theorem WeierstrassCurve.Jacobian.Y_sub_Y_add_Y_sub_negY {R : Type r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 u} [Field F] {W : 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 r} [CommRing R] (W' : Jacobian R) (P : Fin 3 → R) : R

The unit associated to a representative of 2 • P for a Jacobian point representative P on a Weierstrass curve W that is 2-torsion.

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 r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 u} [Field F] {W : 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 u} [Field F] {W : 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 r} [CommRing R] (W' : Jacobian R) (P : Fin 3 → R) : R

The Z-coordinate of a representative of 2 • P for a Jacobian point representative P on a Weierstrass curve.

Equations

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

theorem WeierstrassCurve.Jacobian.dblZ_smul {R : Type r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian R} {P : Fin 3 → R} (hPz : P 2 = 0) : W'.dblZ P = 0

theorem WeierstrassCurve.Jacobian.dblZ_of_Y_eq {R : Type r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 u} [Field F] {W : 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 r} [CommRing R] {W' : Jacobian 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 u} [Field F] {W : 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 r} [CommRing R] (W' : Jacobian R) (P : Fin 3 → R) : R

The X-coordinate of a representative of 2 • P for a Jacobian point representative P on a Weierstrass curve.

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 r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 u} [Field F] {W : 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 = (toAffine W).addX (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) ((toAffine W).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 r} [CommRing R] (W' : Jacobian R) (P : Fin 3 → R) : R

The Y-coordinate of a representative of -(2 • P) for a Jacobian point representative P on a Weierstrass curve.

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 r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 u} [Field F] {W : 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 = (toAffine W).negAddY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) ((toAffine W).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 r} [CommRing R] (W' : Jacobian R) (P : Fin 3 → R) : R

The Y-coordinate of a representative of 2 • P for a Jacobian point representative P on a Weierstrass curve.

Equations

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

theorem WeierstrassCurve.Jacobian.dblY_smul {R : Type r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 u} [Field F] {W : 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 = (toAffine W).addY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) ((toAffine W).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 r} [CommRing R] (W' : Jacobian R) (P : Fin 3 → R) : Fin 3 → R

The coordinates of a representative of 2 • P for a Jacobian point representative P on a Weierstrass curve.

Equations

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

theorem WeierstrassCurve.Jacobian.dblXYZ_X {R : Type r} [CommRing R] {W' : Jacobian R} (P : Fin 3 → R) : W'.dblXYZ P 0 = W'.dblX P

theorem WeierstrassCurve.Jacobian.dblXYZ_Y {R : Type r} [CommRing R] {W' : Jacobian R} (P : Fin 3 → R) : W'.dblXYZ P 1 = W'.dblY P

theorem WeierstrassCurve.Jacobian.dblXYZ_Z {R : Type r} [CommRing R] {W' : Jacobian R} (P : Fin 3 → R) : W'.dblXYZ P 2 = W'.dblZ P

theorem WeierstrassCurve.Jacobian.dblXYZ_smul {R : Type r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 u} [Field F] {W : 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 u} [Field F] {W : 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 • ![(toAffine W).addX (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) ((toAffine W).slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)), (toAffine W).addY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) ((toAffine W).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 u} [Field F] (P Q : Fin 3 → F) : F

The unit associated to a representative of P + Q for two Jacobian point representatives P and Q on a Weierstrass curve W that are not 2-torsion.

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 u} [Field F] {P Q : Fin 3 → F} (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) {u v : F} (hu : u ≠ 0) (hv : v ≠ 0) : addU (u • P) (v • Q) = (u * v) ^ 2 * addU P Q

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

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

theorem WeierstrassCurve.Jacobian.addU_ne_zero_of_Y_ne {F : Type u} [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) : addU P Q ≠ 0

theorem WeierstrassCurve.Jacobian.isUnit_addU_of_Y_ne {F : Type u} [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 (addU P Q)

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

The Z-coordinate of a representative of P + Q for two distinct Jacobian point representatives P and Q on a Weierstrass curve.

If the representatives of P and Q are equal, then this returns the value 0.

Equations

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

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

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

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

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

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

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

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

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

The X-coordinate of a representative of P + Q for two distinct Jacobian point representatives P and Q on a Weierstrass curve.

If the representatives of P and Q are equal, then this returns the value 0.

Equations

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

theorem WeierstrassCurve.Jacobian.addX_eq' {R : Type r} [CommRing R] {W' : Jacobian 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 * addZ P Q - W'.a₂ * P 2 ^ 2 * Q 2 ^ 2 * addZ P Q ^ 2 - P 0 * Q 2 ^ 2 * addZ P Q ^ 2 - Q 0 * P 2 ^ 2 * addZ P Q ^ 2

theorem WeierstrassCurve.Jacobian.addX_eq {F : Type u} [Field F] {W : 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 * addZ P Q - W.a₂ * P 2 ^ 2 * Q 2 ^ 2 * addZ P Q ^ 2 - P 0 * Q 2 ^ 2 * addZ P Q ^ 2 - Q 0 * P 2 ^ 2 * addZ P Q ^ 2) / (P 2 * Q 2) ^ 2

theorem WeierstrassCurve.Jacobian.addX_smul {R : Type r} [CommRing R] {W' : Jacobian 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_self {R : Type r} [CommRing R] {W' : Jacobian R} {P : Fin 3 → R} (hP : W'.Equation P) : W'.addX P P = 0

theorem WeierstrassCurve.Jacobian.addX_of_Z_eq_zero_left {R : Type r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 u} [Field F] {W : 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 = addU P Q ^ 2

theorem WeierstrassCurve.Jacobian.addX_of_Z_ne_zero {F : Type u} [Field F] {W : 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 / addZ P Q ^ 2 = (toAffine W).addX (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) ((toAffine W).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 r} [CommRing R] (W' : Jacobian R) (P Q : Fin 3 → R) : R

The Y-coordinate of a representative of -(P + Q) for two distinct Jacobian point representatives P and Q on a Weierstrass curve.

If the representatives of P and Q are equal, then this returns the value 0.

Equations

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

theorem WeierstrassCurve.Jacobian.negAddY_eq' {R : Type r} [CommRing R] {W' : Jacobian 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 * addZ P Q ^ 2) + P 1 * Q 2 ^ 3 * addZ P Q ^ 3

theorem WeierstrassCurve.Jacobian.negAddY_eq {F : Type u} [Field F] {W : 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 * addZ P Q ^ 2) + P 1 * Q 2 ^ 3 * addZ P Q ^ 3) / (P 2 * Q 2) ^ 3

theorem WeierstrassCurve.Jacobian.negAddY_smul {R : Type r} [CommRing R] {W' : Jacobian 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_self {R : Type r} [CommRing R] {W' : Jacobian R} (P : Fin 3 → R) : W'.negAddY P P = 0

theorem WeierstrassCurve.Jacobian.negAddY_of_Z_eq_zero_left {R : Type r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 u} [Field F] {W : 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 = (-addU P Q) ^ 3

theorem WeierstrassCurve.Jacobian.negAddY_of_Z_ne_zero {F : Type u} [Field F] {W : 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 / addZ P Q ^ 3 = (toAffine W).negAddY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) ((toAffine W).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 r} [CommRing R] (W' : Jacobian R) (P Q : Fin 3 → R) : R

The Y-coordinate of a representative of P + Q for two distinct Jacobian point representatives P and Q on a Weierstrass curve.

If the representatives of P and Q are equal, then this returns the value 0.

Equations

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

theorem WeierstrassCurve.Jacobian.addY_smul {R : Type r} [CommRing R] {W' : Jacobian 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_self {R : Type r} [CommRing R] {W' : Jacobian R} {P : Fin 3 → R} (hP : W'.Equation P) : W'.addY P P = 0

theorem WeierstrassCurve.Jacobian.addY_of_Z_eq_zero_left {R : Type r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 u} [Field F] {W : 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 = addU P Q ^ 3

theorem WeierstrassCurve.Jacobian.addY_of_Z_ne_zero {F : Type u} [Field F] {W : 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 / addZ P Q ^ 3 = (toAffine W).addY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) ((toAffine W).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 r} [CommRing R] (W' : Jacobian R) (P Q : Fin 3 → R) : Fin 3 → R

The coordinates of a representative of P + Q for two distinct Jacobian point representatives P and Q on a Weierstrass curve.

If the representatives of P and Q are equal, then this returns the value ![0, 0, 0].

Equations

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

theorem WeierstrassCurve.Jacobian.addXYZ_X {R : Type r} [CommRing R] {W' : Jacobian R} (P Q : Fin 3 → R) : W'.addXYZ P Q 0 = W'.addX P Q

theorem WeierstrassCurve.Jacobian.addXYZ_Y {R : Type r} [CommRing R] {W' : Jacobian R} (P Q : Fin 3 → R) : W'.addXYZ P Q 1 = W'.addY P Q

theorem WeierstrassCurve.Jacobian.addXYZ_Z {R : Type r} [CommRing R] {W' : Jacobian R} (P Q : Fin 3 → R) : W'.addXYZ P Q 2 = addZ P Q

theorem WeierstrassCurve.Jacobian.addXYZ_smul {R : Type r} [CommRing R] {W' : Jacobian 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_self {R : Type r} [CommRing R] {W' : Jacobian R} {P : Fin 3 → R} (hP : W'.Equation P) : W'.addXYZ P P = ![0, 0, 0]

theorem WeierstrassCurve.Jacobian.addXYZ_of_Z_eq_zero_left {R : Type r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 u} [Field F] {W : 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 = addU P Q • ![1, 1, 0]

theorem WeierstrassCurve.Jacobian.addXYZ_of_Z_ne_zero {F : Type u} [Field F] {W : 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 = addZ P Q • ![(toAffine W).addX (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) ((toAffine W).slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)), (toAffine W).addY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) ((toAffine W).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 r} [CommRing R] (W' : Jacobian R) (P : Fin 3 → R) : Fin 3 → R

The negation of a Jacobian point representative on a Weierstrass curve.

Equations

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

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

theorem WeierstrassCurve.Jacobian.neg_Y {R : Type r} [CommRing R] {W' : Jacobian R} (P : Fin 3 → R) : W'.neg P 1 = W'.negY P

theorem WeierstrassCurve.Jacobian.neg_Z {R : Type r} [CommRing R] {W' : Jacobian R} (P : Fin 3 → R) : W'.neg P 2 = P 2

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

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

theorem WeierstrassCurve.Jacobian.neg_equiv {R : Type r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 u} [Field F] {W : 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 u} [Field F] {W : Jacobian F} {P : Fin 3 → F} (hPz : P 2 ≠ 0) : W.neg P = P 2 • ![P 0 / P 2 ^ 2, (toAffine W).negY (P 0 / P 2 ^ 2) (P 1 / P 2 ^ 3), 1]

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

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

theorem WeierstrassCurve.Jacobian.addX_neg {R : Type r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] (W' : Jacobian R) (P : PointClass R) : PointClass R

The negation of a Jacobian point class on a Weierstrass curve W.

If P is a Jacobian point representative on W, 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 r} [CommRing R] {W' : Jacobian R} (P : Fin 3 → R) : W'.negMap ⟦P⟧ = ⟦W'.neg P⟧

theorem WeierstrassCurve.Jacobian.negMap_of_Z_eq_zero {F : Type u} [Field F] {W : 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 u} [Field F] {W : Jacobian F} {P : Fin 3 → F} (hPz : P 2 ≠ 0) : W.negMap ⟦P⟧ = ⟦![P 0 / P 2 ^ 2, (toAffine W).negY (P 0 / P 2 ^ 2) (P 1 / P 2 ^ 3), 1]⟧

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

Addition on point representatives

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

The addition of two Jacobian point representatives on a Weierstrass curve.

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 r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian R} (P : Fin 3 → R) : W'.add P P = W'.dblXYZ P

theorem WeierstrassCurve.Jacobian.add_of_eq {R : Type r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 u} [Field F] {W : 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 r} [CommRing R] {W' : Jacobian 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 r} [CommRing R] {W' : Jacobian 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 u} [Field F] {W : 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 u} [Field F] {W : 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 = addU P Q • ![1, 1, 0]

theorem WeierstrassCurve.Jacobian.add_of_Y_ne' {F : Type u} [Field F] {W : 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 • ![(toAffine W).addX (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) ((toAffine W).slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)), (toAffine W).addY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) ((toAffine W).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 u} [Field F] {W : 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 = addZ P Q • ![(toAffine W).addX (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) ((toAffine W).slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)), (toAffine W).addY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) ((toAffine W).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 u} [Field F] {W : 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 r} [CommRing R] (W' : Jacobian R) (P Q : PointClass R) : PointClass R

The addition of two Jacobian point classes on a Weierstrass curve W.

If P and Q are two Jacobian point representatives on W, 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 r} [CommRing R] {W' : Jacobian 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 u} [Field F] {W : Jacobian F} {P : Fin 3 → F} {Q : 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 u} [Field F] {W : Jacobian F} {P : 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 u} [Field F] {W : 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 u} [Field F] {W : 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⟧ = ⟦![(toAffine W).addX (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) ((toAffine W).slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)), (toAffine W).addY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) ((toAffine W).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 u} [Field F] {W : Jacobian F} {P Q : 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 r} [CommRing R] (W' : Jacobian R) : Type r

A nonsingular Jacobian point on a Weierstrass curve W.

• point : PointClass R

  The Jacobian point class underlying a nonsingular Jacobian point on W.

• nonsingular : W'.NonsingularLift self.point

  The nonsingular condition underlying a nonsingular Jacobian point on W.

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

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

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

Equations

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

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

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

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

The natural map from a nonsingular point on a Weierstrass curve in affine coordinates to its corresponding nonsingular Jacobian point.

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 r} [CommRing R] {W' : Jacobian R} [Nontrivial R] : fromAffine 0 = 0

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

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

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

The negation of a nonsingular Jacobian point on a Weierstrass curve W.

Given a nonsingular Jacobian point P on W, use -P instead of neg P.

Equations

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

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

Equations

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

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

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

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

The addition of two nonsingular Jacobian points on a Weierstrass curve W.

Given two nonsingular Jacobian 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 u} [Field F] {W : Jacobian F} : Add W.Point

Equations

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

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

theorem WeierstrassCurve.Jacobian.Point.add_point {F : Type u} [Field F] {W : 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 u} [Field F] (W : Jacobian F) (P : Fin 3 → F) : (Jacobian.toAffine W).Point

The natural map from a nonsingular Jacobian point representative on a Weierstrass curve to its corresponding nonsingular point 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 u} [Field F] {W : Jacobian F} {P : Fin 3 → F} (hP : ¬W.Nonsingular P) : toAffine W P = 0

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

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

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

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

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

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

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

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

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

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

If hP is the nonsingular condition underlying a nonsingular Jacobian point P on W, then toAffineLift ⟨hP⟩ is definitionally equivalent to toAffine W P.

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 u} [Field F] {W : Jacobian F} {P : Fin 3 → F} (hP : W.NonsingularLift ⟦P⟧) : (mk hP).toAffineLift = toAffine W P

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

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

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

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

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

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

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

The addition-preserving equivalence between the type of nonsingular Jacobian points on a Weierstrass curve W and the type of nonsingular points W⟮F⟯ in affine coordinates.

Equations

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

@[simp]

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

@[simp]

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

Maps across ring homomorphisms

@[simp]

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

theorem WeierstrassCurve.Jacobian.Equation.map {R : Type r} [CommRing R] {W' : Jacobian R} {S : Type v} [CommRing S] (f : R →+* S) {P : Fin 3 → R} (h : W'.Equation P) : (WeierstrassCurve.map W' f).toJacobian.Equation (⇑f ∘ P)

@[simp]

theorem WeierstrassCurve.Jacobian.map_equation {R : Type r} [CommRing R] {W' : Jacobian R} {S : Type v} [CommRing S] {f : R →+* S} (hf : Function.Injective ⇑f) (P : Fin 3 → R) : (map W' f).toJacobian.Equation (⇑f ∘ P) ↔ W'.Equation P

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem WeierstrassCurve.Jacobian.map_nonsingular {R : Type r} [CommRing R] {W' : Jacobian R} {S : Type v} [CommRing S] {f : R →+* S} (hf : Function.Injective ⇑f) (P : Fin 3 → R) : (map W' f).toJacobian.Nonsingular (⇑f ∘ P) ↔ W'.Nonsingular P

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem WeierstrassCurve.Jacobian.map_addU {F : Type u} [Field F] {K : Type v} [Field K] (f : F →+* K) (P Q : Fin 3 → F) : addU (⇑f ∘ P) (⇑f ∘ Q) = f (addU P Q)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem WeierstrassCurve.Jacobian.map_add {F : Type u} [Field F] {W : Jacobian F} {K : Type v} [Field K] (f : F →+* K) {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) : (map W f).toJacobian.add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W.add P Q

Base changes across algebra homomorphisms

theorem WeierstrassCurve.Jacobian.baseChange_polynomial {R : Type r} [CommRing R] (W' : Jacobian R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) : (baseChange W' B).toJacobian.polynomial = (MvPolynomial.map ↑f) (baseChange W' A).toJacobian.polynomial

theorem WeierstrassCurve.Jacobian.baseChange_equation {R : Type r} [CommRing R] (W' : Jacobian R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] {f : A →ₐ[S] B} (hf : Function.Injective ⇑f) (P : Fin 3 → A) : (baseChange W' B).toJacobian.Equation (⇑f ∘ P) ↔ (baseChange W' A).toJacobian.Equation P

theorem WeierstrassCurve.Jacobian.baseChange_polynomialX {R : Type r} [CommRing R] (W' : Jacobian R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) : (baseChange W' B).toJacobian.polynomialX = (MvPolynomial.map ↑f) (baseChange W' A).toJacobian.polynomialX

theorem WeierstrassCurve.Jacobian.baseChange_polynomialY {R : Type r} [CommRing R] (W' : Jacobian R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) : (baseChange W' B).toJacobian.polynomialY = (MvPolynomial.map ↑f) (baseChange W' A).toJacobian.polynomialY

theorem WeierstrassCurve.Jacobian.baseChange_polynomialZ {R : Type r} [CommRing R] (W' : Jacobian R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) : (baseChange W' B).toJacobian.polynomialZ = (MvPolynomial.map ↑f) (baseChange W' A).toJacobian.polynomialZ

theorem WeierstrassCurve.Jacobian.baseChange_nonsingular {R : Type r} [CommRing R] (W' : Jacobian R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] {f : A →ₐ[S] B} (hf : Function.Injective ⇑f) (P : Fin 3 → A) : (baseChange W' B).toJacobian.Nonsingular (⇑f ∘ P) ↔ (baseChange W' A).toJacobian.Nonsingular P

theorem WeierstrassCurve.Jacobian.baseChange_negY {R : Type r} [CommRing R] (W' : Jacobian R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (P : Fin 3 → A) : (baseChange W' B).toJacobian.negY (⇑f ∘ P) = f ((baseChange W' A).toJacobian.negY P)

theorem WeierstrassCurve.Jacobian.baseChange_neg {R : Type r} [CommRing R] (W' : Jacobian R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (P : Fin 3 → A) : (baseChange W' B).toJacobian.neg (⇑f ∘ P) = ⇑f ∘ (baseChange W' A).toJacobian.neg P

theorem WeierstrassCurve.Jacobian.baseChange_dblU {R : Type r} [CommRing R] (W' : Jacobian R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (P : Fin 3 → A) : (baseChange W' B).toJacobian.dblU (⇑f ∘ P) = f ((baseChange W' A).toJacobian.dblU P)

theorem WeierstrassCurve.Jacobian.baseChange_dblZ {R : Type r} [CommRing R] (W' : Jacobian R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (P : Fin 3 → A) : (baseChange W' B).toJacobian.dblZ (⇑f ∘ P) = f ((baseChange W' A).toJacobian.dblZ P)

theorem WeierstrassCurve.Jacobian.baseChange_dblX {R : Type r} [CommRing R] (W' : Jacobian R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (P : Fin 3 → A) : (baseChange W' B).toJacobian.dblX (⇑f ∘ P) = f ((baseChange W' A).toJacobian.dblX P)

theorem WeierstrassCurve.Jacobian.baseChange_negDblY {R : Type r} [CommRing R] (W' : Jacobian R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (P : Fin 3 → A) : (baseChange W' B).toJacobian.negDblY (⇑f ∘ P) = f ((baseChange W' A).toJacobian.negDblY P)

theorem WeierstrassCurve.Jacobian.baseChange_dblY {R : Type r} [CommRing R] (W' : Jacobian R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (P : Fin 3 → A) : (baseChange W' B).toJacobian.dblY (⇑f ∘ P) = f ((baseChange W' A).toJacobian.dblY P)

theorem WeierstrassCurve.Jacobian.baseChange_dblXYZ {R : Type r} [CommRing R] (W' : Jacobian R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (P : Fin 3 → A) : (baseChange W' B).toJacobian.dblXYZ (⇑f ∘ P) = ⇑f ∘ (baseChange W' A).toJacobian.dblXYZ P

theorem WeierstrassCurve.Jacobian.baseChange_addX {R : Type r} [CommRing R] (W' : Jacobian R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (P Q : Fin 3 → A) : (baseChange W' B).toJacobian.addX (⇑f ∘ P) (⇑f ∘ Q) = f ((baseChange W' A).toJacobian.addX P Q)

theorem WeierstrassCurve.Jacobian.baseChange_negAddY {R : Type r} [CommRing R] (W' : Jacobian R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (P Q : Fin 3 → A) : (baseChange W' B).toJacobian.negAddY (⇑f ∘ P) (⇑f ∘ Q) = f ((baseChange W' A).toJacobian.negAddY P Q)

theorem WeierstrassCurve.Jacobian.baseChange_addY {R : Type r} [CommRing R] (W' : Jacobian R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (P Q : Fin 3 → A) : (baseChange W' B).toJacobian.addY (⇑f ∘ P) (⇑f ∘ Q) = f ((baseChange W' A).toJacobian.addY P Q)

theorem WeierstrassCurve.Jacobian.baseChange_addXYZ {R : Type r} [CommRing R] (W' : Jacobian R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (P Q : Fin 3 → A) : (baseChange W' B).toJacobian.addXYZ (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ (baseChange W' A).toJacobian.addXYZ P Q

theorem WeierstrassCurve.Jacobian.baseChange_add {F : Type u} [Field F] {R : Type r} [CommRing R] (W' : Jacobian R) {S : Type s} [CommRing S] [Algebra R S] [Algebra R F] [Algebra S F] [IsScalarTower R S F] {K : Type v} [Field K] [Algebra R K] [Algebra S K] [IsScalarTower R S K] (f : F →ₐ[S] K) {P Q : Fin 3 → F} (hP : (baseChange W' F).toJacobian.Nonsingular P) (hQ : (baseChange W' F).toJacobian.Nonsingular Q) : (baseChange W' K).toJacobian.add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ (baseChange W' F).toJacobian.add P Q

@[reducible, inline]

abbrev WeierstrassCurve.Affine.Point.toJacobian {R : Type u} [CommRing R] [Nontrivial R] {W : 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