Projective 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 a unit, 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.

Mathematical background

Let W be a Weierstrass curve over a field F. A point on the projective plane is an equivalence class of triples $[x:y:z]$ with coordinates in F such that $(x, y, z) \sim (x', y', z')$ precisely if there is some unit u of F such that $(x, y, z) = (ux', uy', uz')$, with an extra condition that $(x, y, z) \ne (0, 0, 0)$. As described in Mathlib.AlgebraicGeometry.EllipticCurve.Affine, a rational point is a point on the projective plane satisfying a homogeneous Weierstrass equation, and being nonsingular means the partial derivatives $W_X(X, Y, Z)$, $W_Y(X, Y, Z)$, and $W_Z(X, Y, Z)$ do not vanish simultaneously. Note that the vanishing of the Weierstrass equation and its partial derivatives are independent of the representative for $[x:y:z]$, and the nonsingularity condition already implies that $(x, y, z) \ne (0, 0, 0)$, so a nonsingular rational point on W can simply be given by a tuple consisting of $[x:y:z]$ and the nonsingular condition on any representative.

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

Main definitions

• WeierstrassCurve.Projective.PointClass: the equivalence class of a point representative.
• WeierstrassCurve.Projective.toAffine: the Weierstrass curve in affine coordinates.
• WeierstrassCurve.Projective.Nonsingular: the nonsingular condition on a point representative.
• WeierstrassCurve.Projective.NonsingularLift: the nonsingular condition on a point class.
• WeierstrassCurve.Projective.neg: the negation operation on a point representative.
• WeierstrassCurve.Projective.negMap: the negation operation on a point class.
• WeierstrassCurve.Projective.add: the addition operation on a point representative.
• WeierstrassCurve.Projective.addMap: the addition operation on a point class.

Main statements

• WeierstrassCurve.Projective.polynomial_relation: Euler's homogeneous function theorem.
• WeierstrassCurve.Projective.nonsingular_neg: negation preserves the nonsingular condition.
• WeierstrassCurve.Projective.nonsingular_add: addition preserves the nonsingular condition.

Implementation notes

A point representative is implemented as a term P of type Fin 3 → R, which allows for the vector notation ![x, y, z]. However, P is not definitionally 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 definitionally equal to ![u * Q x, u * Q y, u * Q z], so the lemmas smul_fin3 and smul_fin3_ext can be used to convert between the two forms.

References

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

Tags

elliptic curve, rational point, projective coordinates

Weierstrass curves

@[reducible, inline]

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

An abbreviation for a Weierstrass curve in projective coordinates.

Equations

• WeierstrassCurve.Projective R = WeierstrassCurve R

@[reducible, inline]

abbrev WeierstrassCurve.toProjective {R : Type u} (W : WeierstrassCurve R) : WeierstrassCurve.Projective R

The coercion to a Weierstrass curve in projective coordinates.

Equations

• W.toProjective = W

Projective coordinates

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

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

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

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

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

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

The equivalence setoid for a point representative.

Equations

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

@[reducible, inline]

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

The equivalence class of a point representative.

Equations

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

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

@[simp]

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

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

@[reducible, inline]

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

The coercion to a Weierstrass curve in affine coordinates.

Equations

• W'.toAffine = W'

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

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

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

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

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

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

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

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

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

theorem WeierstrassCurve.Projective.equiv_of_X_eq_of_Y_eq {F : Type v} [Field F] {P : Fin 3 → F} {Q : Fin 3 → F} (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 ≈ Q

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

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

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

Weierstrass equations

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

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

Equations

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

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

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

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

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

Equations

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

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

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

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

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

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

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

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

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

Nonsingular Weierstrass equations

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

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

Equations

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

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

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

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

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

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

Equations

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

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

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

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

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

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

Equations

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

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

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

theorem WeierstrassCurve.Projective.polynomial_relation {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3 → R) : 3 * (MvPolynomial.eval P) W'.polynomial = P 0 * (MvPolynomial.eval P) W'.polynomialX + P 1 * (MvPolynomial.eval P) W'.polynomialY + P 2 * (MvPolynomial.eval P) W'.polynomialZ

Euler's homogeneous function theorem.

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

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

Note that this definition is only mathematically accurate for fields.

Equations

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

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

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

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

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

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

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

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

theorem WeierstrassCurve.Projective.nonsingular_iff_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective 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.Projective.Y_ne_zero_of_Z_eq_zero {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3 → R} (hP : W'.Nonsingular P) (hPz : P 2 = 0) : P 1 ≠ 0

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

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

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

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

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

Equations

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

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

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

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

@[deprecated WeierstrassCurve.Projective.equation_smul]

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

Alias of WeierstrassCurve.Projective.equation_smul.

@[deprecated WeierstrassCurve.Projective.nonsingularLift_zero]

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

Alias of WeierstrassCurve.Projective.nonsingularLift_zero.

@[deprecated WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero]

theorem WeierstrassCurve.Projective.nonsingular_affine_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} (hPz : P 2 ≠ 0) : W.Nonsingular P ↔ W.toAffine.Nonsingular (P 0 / P 2) (P 1 / P 2)

Alias of WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero.

@[deprecated WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero]

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

Alias of WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero.

@[deprecated WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero]

theorem WeierstrassCurve.Projective.nonsingular_of_affine_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} (hPz : P 2 ≠ 0) : W.Nonsingular P ↔ W.toAffine.Nonsingular (P 0 / P 2) (P 1 / P 2)

Alias of WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero.

@[deprecated WeierstrassCurve.Projective.nonsingular_smul]

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

Alias of WeierstrassCurve.Projective.nonsingular_smul.

@[deprecated WeierstrassCurve.Projective.nonsingular_zero]

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

Alias of WeierstrassCurve.Projective.nonsingular_zero.

Negation formulae

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

The $Y$-coordinate of a representative of -P for a point P.

Equations

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

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

theorem WeierstrassCurve.Projective.negY_smul {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing 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 u} {W' : WeierstrassCurve.Projective R} [CommRing 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 v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} (hPz : P 2 ≠ 0) : W.negY P / P 2 = W.toAffine.negY (P 0 / P 2) (P 1 / P 2)

theorem WeierstrassCurve.Projective.Y_sub_Y_mul_Y_sub_negY {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P : Fin 3 → R} {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 u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3 → R} {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 u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3 → R} {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 v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} {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 = W.toAffine.negY (Q 0 / Q 2) (Q 1 / Q 2)

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

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

The unit associated to the doubling of a 2-torsion point P. 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 v} [Field F] {W : WeierstrassCurve.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 v} [Field F] {W : WeierstrassCurve.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 v} [Field F] {W : WeierstrassCurve.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 v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} {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 v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} {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 u} (W' : WeierstrassCurve.Projective R) [CommRing R] (P : Fin 3 → R) : R

The $Z$-coordinate of a representative of 2 • P for a point P.

Equations

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

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

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

The $X$-coordinate of a representative of 2 • P for a point P.

Equations

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

theorem WeierstrassCurve.Projective.dblX_eq' {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing 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 v} [Field F] {W : WeierstrassCurve.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 u} {W' : WeierstrassCurve.Projective R} [CommRing 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 u} {W' : WeierstrassCurve.Projective R} [CommRing 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 u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3 → R} {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 v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} {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 = W.toAffine.addX (P 0 / P 2) (Q 0 / Q 2) (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2))

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

The $Y$-coordinate of a representative of -(2 • P) for a point P.

Equations

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

theorem WeierstrassCurve.Projective.negDblY_eq' {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing 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 v} [Field F] {W : WeierstrassCurve.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 u} {W' : WeierstrassCurve.Projective R} [CommRing 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 u} {W' : WeierstrassCurve.Projective R} [CommRing 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 u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3 → R} {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 v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} {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 v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} {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 = W.toAffine.negAddY (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2))

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

The $Y$-coordinate of a representative of 2 • P for a point P.

Equations

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

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

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

The coordinates of a representative of 2 • P for a point P.

Equations

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

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

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

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

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

Addition formulae

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

The unit associated to the addition of a non-2-torsion point P with its negation. 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 v} [Field F] {P : Fin 3 → F} {Q : Fin 3 → F} (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) {u : F} {v : F} (hu : u ≠ 0) (hv : v ≠ 0) : WeierstrassCurve.Projective.addU (u • P) (v • Q) = (u * v) ^ 2 * WeierstrassCurve.Projective.addU P Q

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

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

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

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

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

The $Z$-coordinate of a representative of P + Q for two distinct points P and Q. Note that this returns the value 0 if the representatives of P and Q are equal.

Equations

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

theorem WeierstrassCurve.Projective.addZ_eq' {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P : Fin 3 → R} {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 v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} {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 u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3 → R) (Q : Fin 3 → R) (u : R) (v : R) : W'.addZ (u • P) (v • Q) = (u * v) ^ 2 * W'.addZ P Q

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

theorem WeierstrassCurve.Projective.addZ_of_Z_eq_zero_left {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3 → R} {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 u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3 → R} {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 u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3 → R} {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 u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3 → R} {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 v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} {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 u} (W' : WeierstrassCurve.Projective R) [CommRing R] (P : Fin 3 → R) (Q : Fin 3 → R) : R

The $X$-coordinate of a representative of P + Q for two distinct points P and Q. Note that this returns the value 0 if the representatives of P and Q are equal.

Equations

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

theorem WeierstrassCurve.Projective.addX_eq' {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P : Fin 3 → R} {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 v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} {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 u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3 → R) (Q : Fin 3 → R) (u : R) (v : R) : W'.addX (u • P) (v • Q) = (u * v) ^ 2 * W'.addX P Q

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

theorem WeierstrassCurve.Projective.addX_of_Z_eq_zero_left {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3 → R} {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 u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3 → R} {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 u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3 → R} {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 v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} {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 = W.toAffine.addX (P 0 / P 2) (Q 0 / Q 2) (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2))

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

The $Y$-coordinate of a representative of -(P + Q) for two distinct points P and Q. Note that this returns the value 0 if the representatives of P and Q are equal.

Equations

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

theorem WeierstrassCurve.Projective.negAddY_eq' {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P : Fin 3 → R} {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 v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} {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 u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3 → R) (Q : Fin 3 → R) (u : R) (v : R) : W'.negAddY (u • P) (v • Q) = (u * v) ^ 2 * W'.negAddY P Q

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

theorem WeierstrassCurve.Projective.negAddY_of_Z_eq_zero_left {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3 → R} {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 u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3 → R} {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 u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P : Fin 3 → R} {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 v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} {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 = -WeierstrassCurve.Projective.addU P Q

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

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

The $Y$-coordinate of a representative of P + Q for two distinct points P and Q. Note that this returns the value 0 if the representatives of P and Q are equal.

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 u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3 → R) (Q : Fin 3 → R) (u : R) (v : R) : W'.addY (u • P) (v • Q) = (u * v) ^ 2 * W'.addY P Q

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

theorem WeierstrassCurve.Projective.addY_of_Z_eq_zero_left {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3 → R} {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 u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3 → R} {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 u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3 → R} {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 v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} {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 = WeierstrassCurve.Projective.addU P Q

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

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

The coordinates of a representative of P + Q for two distinct points P and Q. Note that this returns the value ![0, 0, 0] if the representatives of P and Q are equal.

Equations

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

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

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

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

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

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

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

theorem WeierstrassCurve.Projective.addXYZ_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} {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 • ![W.toAffine.addX (P 0 / P 2) (Q 0 / Q 2) (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)), W.toAffine.addY (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)), 1]

Negation on point representatives

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

The negation of a point representative.

Equations

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Equations

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

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

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

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

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

Addition on point representatives

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

The addition of two point representatives.

Equations

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

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

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

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

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

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

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

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

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

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

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

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

theorem WeierstrassCurve.Projective.add_of_Y_eq {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} {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.add P Q = W.dblU P • ![0, 1, 0]

theorem WeierstrassCurve.Projective.add_of_Y_ne {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} {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) : W.add P Q = WeierstrassCurve.Projective.addU P Q • ![0, 1, 0]

theorem WeierstrassCurve.Projective.add_of_Y_ne' {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} {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.add P Q = W.dblZ P • ![W.toAffine.addX (P 0 / P 2) (Q 0 / Q 2) (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)), W.toAffine.addY (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)), 1]

theorem WeierstrassCurve.Projective.add_of_X_ne {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} {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.add P Q = W.addZ P Q • ![W.toAffine.addX (P 0 / P 2) (Q 0 / Q 2) (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)), W.toAffine.addY (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)), 1]

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

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

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

Equations

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

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

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

theorem WeierstrassCurve.Projective.addMap_of_Z_eq_zero_right {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : WeierstrassCurve.Projective.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.Projective.addMap_of_Y_eq {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} {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 = Q 0 * P 2) (hy' : P 1 * Q 2 = W.negY Q * P 2) : W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![0, 1, 0]⟧

theorem WeierstrassCurve.Projective.addMap_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} {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 = Q 0 * P 2 → P 1 * Q 2 ≠ W.negY Q * P 2) : W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![W.toAffine.addX (P 0 / P 2) (Q 0 / Q 2) (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)), W.toAffine.addY (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)), 1]⟧

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