Negation and addition formulae for nonsingular points in projective coordinates

Let W be a Weierstrass curve over a field F. The nonsingular projective 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 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 projective point representatives. The group operations and the group law on actual nonsingular projective points will be defined in Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Point.lean.

Main definitions

• WeierstrassCurve.Projective.negY: the Y-coordinate of -P.
• WeierstrassCurve.Projective.dblZ: the Z-coordinate of 2 • P.
• WeierstrassCurve.Projective.dblX: the X-coordinate of 2 • P.
• WeierstrassCurve.Projective.negDblY: the Y-coordinate of -(2 • P).
• WeierstrassCurve.Projective.dblY: the Y-coordinate of 2 • P.
• WeierstrassCurve.Projective.addZ: the Z-coordinate of P + Q.
• WeierstrassCurve.Projective.addX: the X-coordinate of P + Q.
• WeierstrassCurve.Projective.negAddY: the Y-coordinate of -(P + Q).
• WeierstrassCurve.Projective.addY: the Y-coordinate of P + Q.

Implementation notes

The definitions of WeierstrassCurve.Projective.dblX, WeierstrassCurve.Projective.negDblY, WeierstrassCurve.Projective.addZ, WeierstrassCurve.Projective.addX, and WeierstrassCurve.Projective.negAddY are given explicitly by large polynomials that are homogeneous of degree 4. Clearing the denominators of their corresponding affine rational functions in Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean would give polynomials that are homogeneous of degrees 5, 6, 6, 8, and 8 respectively, so their actual definitions are off by powers of certain polynomial factors that are homogeneous of degree 1 or 2. These factors divide their corresponding affine polynomials only modulo the 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.Projective.dblXYZ and WeierstrassCurve.Projective.addXYZ are homogeneous of degree 4.

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

References

J Silverman, The Arithmetic of Elliptic Curves

Tags

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

Negation formulae in projective coordinates

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

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

Equations

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

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

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

theorem WeierstrassCurve.Projective.negY_of_Z_eq_zero {R : Type r} [CommRing R] {W' : Projective R} [NoZeroDivisors R] {P : Fin 3 → R} (hP : W'.Equation P) (hPz : P 2 = 0) : W'.negY P = -P 1

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

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

theorem WeierstrassCurve.Projective.Y_eq_of_Y_ne {R : Type r} [CommRing R] {W' : Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 ≠ Q 1 * P 2) : P 1 * Q 2 = W'.negY Q * P 2

theorem WeierstrassCurve.Projective.Y_eq_of_Y_ne' {R : Type r} [CommRing R] {W' : Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 ≠ W'.negY Q * P 2) : P 1 * Q 2 = Q 1 * P 2

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

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

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

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

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

theorem WeierstrassCurve.Projective.nonsingular_iff_of_Y_eq_negY {F : Type u} [Field F] {W : Projective 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 projective coordinates

noncomputable def WeierstrassCurve.Projective.dblU {F : Type u} [Field F] (W : Projective F) (P : Fin 3 → F) : F

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

More specifically, the unit u such that W.add P P = u • ![0, 1, 0] where P = W.neg P.

Equations

• W.dblU P = (MvPolynomial.eval P) W.polynomialX ^ 3 / P 2 ^ 2

theorem WeierstrassCurve.Projective.dblU_eq {F : Type u} [Field F] {W : Projective F} (P : Fin 3 → F) : W.dblU P = (W.a₁ * P 1 * P 2 - (3 * P 0 ^ 2 + 2 * W.a₂ * P 0 * P 2 + W.a₄ * P 2 ^ 2)) ^ 3 / P 2 ^ 2

theorem WeierstrassCurve.Projective.dblU_smul {F : Type u} [Field F] {W : Projective F} {P : Fin 3 → F} (hPz : P 2 ≠ 0) {u : F} (hu : u ≠ 0) : W.dblU (u • P) = u ^ 4 * W.dblU P

theorem WeierstrassCurve.Projective.dblU_of_Z_eq_zero {F : Type u} [Field F] {W : Projective F} {P : Fin 3 → F} (hPz : P 2 = 0) : W.dblU P = 0

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

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

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

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

Equations

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

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

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

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

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

theorem WeierstrassCurve.Projective.isUnit_dblZ_of_Y_ne {F : Type u} [Field F] {W : Projective 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 = Q 0 * P 2) (hy : P 1 * Q 2 ≠ Q 1 * P 2) : IsUnit (W.dblZ P)

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

theorem WeierstrassCurve.Projective.isUnit_dblZ_of_Y_ne' {F : Type u} [Field F] {W : Projective 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 = Q 0 * P 2) (hy : P 1 * Q 2 ≠ W.negY Q * P 2) : IsUnit (W.dblZ P)

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

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

Equations

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

theorem WeierstrassCurve.Projective.dblX_eq' {R : Type r} [CommRing R] {W' : Projective R} {P : Fin 3 → R} (hP : W'.Equation P) : W'.dblX P * P 2 = ((MvPolynomial.eval P) W'.polynomialX ^ 2 - W'.a₁ * (MvPolynomial.eval P) W'.polynomialX * P 2 * (P 1 - W'.negY P) - W'.a₂ * P 2 ^ 2 * (P 1 - W'.negY P) ^ 2 - 2 * P 0 * P 2 * (P 1 - W'.negY P) ^ 2) * (P 1 - W'.negY P)

theorem WeierstrassCurve.Projective.dblX_eq {F : Type u} [Field F] {W : Projective F} {P : Fin 3 → F} (hP : W.Equation P) (hPz : P 2 ≠ 0) : W.dblX P = ((MvPolynomial.eval P) W.polynomialX ^ 2 - W.a₁ * (MvPolynomial.eval P) W.polynomialX * P 2 * (P 1 - W.negY P) - W.a₂ * P 2 ^ 2 * (P 1 - W.negY P) ^ 2 - 2 * P 0 * P 2 * (P 1 - W.negY P) ^ 2) * (P 1 - W.negY P) / P 2

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

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

theorem WeierstrassCurve.Projective.dblX_of_Y_eq {R : Type r} [CommRing R] {W' : Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 = Q 1 * P 2) (hy' : P 1 * Q 2 = W'.negY Q * P 2) : W'.dblX P = 0

theorem WeierstrassCurve.Projective.dblX_of_Z_ne_zero {F : Type u} [Field F] {W : Projective 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 = Q 0 * P 2) (hy : P 1 * Q 2 ≠ W.negY Q * P 2) : W.dblX P / W.dblZ P = (toAffine W).addX (P 0 / P 2) (Q 0 / Q 2) ((toAffine W).slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2))

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

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

Equations

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

theorem WeierstrassCurve.Projective.negDblY_eq' {R : Type r} [CommRing R] {W' : Projective R} {P : Fin 3 → R} (hP : W'.Equation P) : W'.negDblY P * P 2 ^ 2 = -(MvPolynomial.eval P) W'.polynomialX * ((MvPolynomial.eval P) W'.polynomialX ^ 2 - W'.a₁ * (MvPolynomial.eval P) W'.polynomialX * P 2 * (P 1 - W'.negY P) - W'.a₂ * P 2 ^ 2 * (P 1 - W'.negY P) ^ 2 - 2 * P 0 * P 2 * (P 1 - W'.negY P) ^ 2 - P 0 * P 2 * (P 1 - W'.negY P) ^ 2) + P 1 * P 2 ^ 2 * (P 1 - W'.negY P) ^ 3

theorem WeierstrassCurve.Projective.negDblY_eq {F : Type u} [Field F] {W : Projective F} {P : Fin 3 → F} (hP : W.Equation P) (hPz : P 2 ≠ 0) : W.negDblY P = (-(MvPolynomial.eval P) W.polynomialX * ((MvPolynomial.eval P) W.polynomialX ^ 2 - W.a₁ * (MvPolynomial.eval P) W.polynomialX * P 2 * (P 1 - W.negY P) - W.a₂ * P 2 ^ 2 * (P 1 - W.negY P) ^ 2 - 2 * P 0 * P 2 * (P 1 - W.negY P) ^ 2 - P 0 * P 2 * (P 1 - W.negY P) ^ 2) + P 1 * P 2 ^ 2 * (P 1 - W.negY P) ^ 3) / P 2 ^ 2

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

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

theorem WeierstrassCurve.Projective.negDblY_of_Y_eq' {R : Type r} [CommRing R] {W' : Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 = Q 1 * P 2) (hy' : P 1 * Q 2 = W'.negY Q * P 2) : W'.negDblY P * P 2 ^ 2 = -(MvPolynomial.eval P) W'.polynomialX ^ 3

theorem WeierstrassCurve.Projective.negDblY_of_Y_eq {F : Type u} [Field F] {W : Projective F} {P Q : Fin 3 → F} (hP : W.Equation P) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 = Q 1 * P 2) (hy' : P 1 * Q 2 = W.negY Q * P 2) : W.negDblY P = -W.dblU P

theorem WeierstrassCurve.Projective.negDblY_of_Z_ne_zero {F : Type u} [Field F] {W : Projective 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 = Q 0 * P 2) (hy : P 1 * Q 2 ≠ W.negY Q * P 2) : W.negDblY P / W.dblZ P = (toAffine W).negAddY (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) ((toAffine W).slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2))

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

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

Equations

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

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

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

theorem WeierstrassCurve.Projective.dblY_of_Y_eq' {R : Type r} [CommRing R] {W' : Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 = Q 1 * P 2) (hy' : P 1 * Q 2 = W'.negY Q * P 2) : W'.dblY P * P 2 ^ 2 = (MvPolynomial.eval P) W'.polynomialX ^ 3

theorem WeierstrassCurve.Projective.dblY_of_Y_eq {F : Type u} [Field F] {W : Projective F} {P Q : Fin 3 → F} (hP : W.Equation P) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 = Q 1 * P 2) (hy' : P 1 * Q 2 = W.negY Q * P 2) : W.dblY P = W.dblU P

theorem WeierstrassCurve.Projective.dblY_of_Z_ne_zero {F : Type u} [Field F] {W : Projective 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 = Q 0 * P 2) (hy : P 1 * Q 2 ≠ W.negY Q * P 2) : W.dblY P / W.dblZ P = (toAffine W).addY (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) ((toAffine W).slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2))

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

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

Equations

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

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

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

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

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

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

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

theorem WeierstrassCurve.Projective.dblXYZ_of_Z_ne_zero {F : Type u} [Field F] {W : Projective 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 = Q 0 * P 2) (hy : P 1 * Q 2 ≠ W.negY Q * P 2) : W.dblXYZ P = W.dblZ P • ![(toAffine W).addX (P 0 / P 2) (Q 0 / Q 2) ((toAffine W).slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)), (toAffine W).addY (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) ((toAffine W).slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)), 1]

Addition formulae in projective coordinates

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

The unit associated to a representative of P + Q for two projective 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 • ![0, 1, 0] where P x / P z = Q x / Q z but P ≠ W.neg P.

Equations

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

theorem WeierstrassCurve.Projective.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.Projective.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.Projective.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.Projective.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 ≠ Q 1 * P 2) : addU P Q ≠ 0

theorem WeierstrassCurve.Projective.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 ≠ Q 1 * P 2) : IsUnit (addU P Q)

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

The Z-coordinate of a representative of P + Q for two distinct projective 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.Projective.addZ_eq' {R : Type r} [CommRing R] {W' : Projective R} {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) : W'.addZ P Q * (P 2 * Q 2) = (P 0 * Q 2 - Q 0 * P 2) ^ 3

theorem WeierstrassCurve.Projective.addZ_eq {F : Type u} [Field F] {W : Projective F} {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) : W.addZ P Q = (P 0 * Q 2 - Q 0 * P 2) ^ 3 / (P 2 * Q 2)

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

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

theorem WeierstrassCurve.Projective.addZ_of_Z_eq_zero_left {R : Type r} [CommRing R] {W' : Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hPz : P 2 = 0) : W'.addZ P Q = P 1 ^ 2 * Q 2 * Q 2

theorem WeierstrassCurve.Projective.addZ_of_Z_eq_zero_right {R : Type r} [CommRing R] {W' : Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R} (hQ : W'.Equation Q) (hQz : Q 2 = 0) : W'.addZ P Q = -(Q 1 ^ 2 * P 2) * P 2

theorem WeierstrassCurve.Projective.addZ_of_X_eq {R : Type r} [CommRing R] {W' : Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 = Q 0 * P 2) : W'.addZ P Q = 0

theorem WeierstrassCurve.Projective.addZ_ne_zero_of_X_ne {R : Type r} [CommRing R] {W' : Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hx : P 0 * Q 2 ≠ Q 0 * P 2) : W'.addZ P Q ≠ 0

theorem WeierstrassCurve.Projective.isUnit_addZ_of_X_ne {F : Type u} [Field F] {W : Projective F} {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hx : P 0 * Q 2 ≠ Q 0 * P 2) : IsUnit (W.addZ P Q)

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

The X-coordinate of a representative of P + Q for two distinct projective 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.Projective.addX_eq' {R : Type r} [CommRing R] {W' : Projective 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 - Q 1 * P 2) ^ 2 * P 2 * Q 2 + W'.a₁ * (P 1 * Q 2 - Q 1 * P 2) * P 2 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) - W'.a₂ * P 2 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2 - P 0 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2 - Q 0 * P 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2) * (P 0 * Q 2 - Q 0 * P 2)

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

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

theorem WeierstrassCurve.Projective.addX_self {R : Type r} [CommRing R] {W' : Projective R} (P : Fin 3 → R) : W'.addX P P = 0

theorem WeierstrassCurve.Projective.addX_of_Z_eq_zero_left {R : Type r} [CommRing R] {W' : Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hPz : P 2 = 0) : W'.addX P Q = P 1 ^ 2 * Q 2 * Q 0

theorem WeierstrassCurve.Projective.addX_of_Z_eq_zero_right {R : Type r} [CommRing R] {W' : Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R} (hQ : W'.Equation Q) (hQz : Q 2 = 0) : W'.addX P Q = -(Q 1 ^ 2 * P 2) * P 0

theorem WeierstrassCurve.Projective.addX_of_X_eq {R : Type r} [CommRing R] {W' : Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 = Q 0 * P 2) : W'.addX P Q = 0

theorem WeierstrassCurve.Projective.addX_of_Z_ne_zero {F : Type u} [Field F] {W : Projective 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 ≠ Q 0 * P 2) : W.addX P Q / W.addZ P Q = (toAffine W).addX (P 0 / P 2) (Q 0 / Q 2) ((toAffine W).slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2))

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

The Y-coordinate of a representative of -(P + Q) for two distinct projective 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.Projective.negAddY_eq' {R : Type r} [CommRing R] {W' : Projective R} {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) : W'.negAddY P Q * (P 2 * Q 2) ^ 2 = (P 1 * Q 2 - Q 1 * P 2) * ((P 1 * Q 2 - Q 1 * P 2) ^ 2 * P 2 * Q 2 + W'.a₁ * (P 1 * Q 2 - Q 1 * P 2) * P 2 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) - W'.a₂ * P 2 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2 - P 0 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2 - Q 0 * P 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2 - P 0 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2) + P 1 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 3

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

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

theorem WeierstrassCurve.Projective.negAddY_self {R : Type r} [CommRing R] {W' : Projective R} (P : Fin 3 → R) : W'.negAddY P P = 0

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

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

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

theorem WeierstrassCurve.Projective.negAddY_of_X_eq {F : Type u} [Field F] {W : Projective 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 = Q 0 * P 2) : W.negAddY P Q = -addU P Q

theorem WeierstrassCurve.Projective.negAddY_of_Z_ne_zero {F : Type u} [Field F] {W : Projective 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 ≠ Q 0 * P 2) : W.negAddY P Q / W.addZ P Q = (toAffine W).negAddY (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) ((toAffine W).slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2))

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

The Y-coordinate of a representative of P + Q for two distinct projective 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, W'.addZ P Q]

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

theorem WeierstrassCurve.Projective.addY_self {R : Type r} [CommRing R] {W' : Projective R} (P : Fin 3 → R) : W'.addY P P = 0

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

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

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

theorem WeierstrassCurve.Projective.addY_of_X_eq {F : Type u} [Field F] {W : Projective 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 = Q 0 * P 2) : W.addY P Q = addU P Q

theorem WeierstrassCurve.Projective.addY_of_Z_ne_zero {F : Type u} [Field F] {W : Projective 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 ≠ Q 0 * P 2) : W.addY P Q / W.addZ P Q = (toAffine W).addY (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) ((toAffine W).slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2))

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

The coordinates of a representative of P + Q for two distinct projective 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, W'.addZ P Q]

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

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

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

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

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

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

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

theorem WeierstrassCurve.Projective.addXYZ_of_X_eq {F : Type u} [Field F] {W : Projective 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 = Q 0 * P 2) : W.addXYZ P Q = addU P Q • ![0, 1, 0]

theorem WeierstrassCurve.Projective.addXYZ_of_Z_ne_zero {F : Type u} [Field F] {W : Projective 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 ≠ Q 0 * P 2) : W.addXYZ P Q = W.addZ P Q • ![(toAffine W).addX (P 0 / P 2) (Q 0 / Q 2) ((toAffine W).slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)), (toAffine W).addY (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) ((toAffine W).slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)), 1]

Maps and base changes

@[simp]

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

@[simp]

theorem WeierstrassCurve.Projective.map_dblU {F : Type u} {K : Type v} [Field F] [Field K] {W : Projective F} (f : F →+* K) (P : Fin 3 → F) : (map W f).toProjective.dblU (⇑f ∘ P) = f (W.dblU P)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem WeierstrassCurve.Projective.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.Projective.map_addZ {R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : Projective R} (f : R →+* S) (P Q : Fin 3 → R) : (map W' f).toProjective.addZ (⇑f ∘ P) (⇑f ∘ Q) = f (W'.addZ P Q)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem WeierstrassCurve.Projective.baseChange_negY {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Projective 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).toProjective.negY (⇑f ∘ P) = f ((baseChange W' A).toProjective.negY P)

theorem WeierstrassCurve.Projective.baseChange_dblU {R : Type r} {S : Type s} {F : Type u} {K : Type v} [CommRing R] [CommRing S] [Field F] [Field K] {W' : Projective R} [Algebra R S] [Algebra R F] [Algebra S F] [IsScalarTower R S F] [Algebra R K] [Algebra S K] [IsScalarTower R S K] (f : F →ₐ[S] K) (P : Fin 3 → F) : (baseChange W' K).toProjective.dblU (⇑f ∘ P) = f ((baseChange W' F).toProjective.dblU P)

theorem WeierstrassCurve.Projective.baseChange_dblZ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Projective 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).toProjective.dblZ (⇑f ∘ P) = f ((baseChange W' A).toProjective.dblZ P)

theorem WeierstrassCurve.Projective.baseChange_dblX {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Projective 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).toProjective.dblX (⇑f ∘ P) = f ((baseChange W' A).toProjective.dblX P)

theorem WeierstrassCurve.Projective.baseChange_negDblY {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Projective 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).toProjective.negDblY (⇑f ∘ P) = f ((baseChange W' A).toProjective.negDblY P)

theorem WeierstrassCurve.Projective.baseChange_dblY {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Projective 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).toProjective.dblY (⇑f ∘ P) = f ((baseChange W' A).toProjective.dblY P)

theorem WeierstrassCurve.Projective.baseChange_dblXYZ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Projective 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).toProjective.dblXYZ (⇑f ∘ P) = ⇑f ∘ (baseChange W' A).toProjective.dblXYZ P

theorem WeierstrassCurve.Projective.baseChange_addX {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Projective 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).toProjective.addX (⇑f ∘ P) (⇑f ∘ Q) = f ((baseChange W' A).toProjective.addX P Q)

theorem WeierstrassCurve.Projective.baseChange_negAddY {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Projective 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).toProjective.negAddY (⇑f ∘ P) (⇑f ∘ Q) = f ((baseChange W' A).toProjective.negAddY P Q)

theorem WeierstrassCurve.Projective.baseChange_addY {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Projective 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).toProjective.addY (⇑f ∘ P) (⇑f ∘ Q) = f ((baseChange W' A).toProjective.addY P Q)

theorem WeierstrassCurve.Projective.baseChange_addXYZ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Projective 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).toProjective.addXYZ (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ (baseChange W' A).toProjective.addXYZ P Q