Negation and addition formulae for nonsingular points in Jacobian coordinates

Let W be a Weierstrass curve over a field F. 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/Formula.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.

This file defines polynomials associated to negation, doubling, and addition of Jacobian point representatives. The group operations and the group law on actual nonsingular Jacobian points will be defined in Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Point.lean.

Main definitions

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

Implementation notes

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

References

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

Tags

elliptic curve, Jacobian, negation, doubling, addition, group law

Negation formulae in Jacobian coordinates

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.

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 = 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 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 = 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 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 in Jacobian coordinates

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.

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.

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.

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} [DecidableEq 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 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.

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} [DecidableEq 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 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.

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} [DecidableEq 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 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.

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} [DecidableEq 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 in Jacobian coordinates

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.

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.

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.

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} [DecidableEq 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 = 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 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.

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} [DecidableEq 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 = 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 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.

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} [DecidableEq 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 = 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 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].

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} [DecidableEq 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 • ![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]

Maps and base changes

@[simp]

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

@[simp]

theorem WeierstrassCurve.Jacobian.map_dblU {R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : Jacobian R} (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} {S : Type s} [CommRing R] [CommRing S] {W' : Jacobian R} (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} {S : Type s} [CommRing R] [CommRing S] {W' : Jacobian R} (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} {S : Type s} [CommRing R] [CommRing S] {W' : Jacobian R} (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} {S : Type s} [CommRing R] [CommRing S] {W' : Jacobian R} (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} {S : Type s} [CommRing R] [CommRing S] {W' : Jacobian R} (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} {K : Type v} [Field F] [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} {S : Type s} [CommRing R] [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} {S : Type s} [CommRing R] [CommRing S] {W' : Jacobian R} (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} {S : Type s} [CommRing R] [CommRing S] {W' : Jacobian R} (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} {S : Type s} [CommRing R] [CommRing S] {W' : Jacobian R} (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} {S : Type s} [CommRing R] [CommRing S] {W' : Jacobian R} (f : R →+* S) (P Q : Fin 3 → R) : (map W' f).toJacobian.addXYZ (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W'.addXYZ P Q

theorem WeierstrassCurve.Jacobian.baseChange_negY {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Jacobian R} [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [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_dblU {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Jacobian R} [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [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} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Jacobian R} [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [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} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Jacobian R} [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [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} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Jacobian R} [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [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} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Jacobian R} [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [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} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Jacobian R} [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [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} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Jacobian R} [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [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} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Jacobian R} [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [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} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Jacobian R} [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [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} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Jacobian R} [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [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