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. The fact that they form an abelian group is proven in Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean.

Mathematical background

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

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

The nonsingular 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. They can be endowed with an group law, which is uniquely determined by these formulae and follows from an equivalence with the nonsingular points W⟮F⟯ in affine coordinates.

Main definitions

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

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

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

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

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

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

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

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

• WeierstrassCurve.Projective.Point: a nonsingular projective point.

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

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

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

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

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

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

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

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

An abbreviation for a Weierstrass curve in projective coordinates.

Equations

• WeierstrassCurve.Projective R = WeierstrassCurve R

@[reducible, inline]

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

The conversion from a Weierstrass curve to projective coordinates.

Equations

• W.toProjective = W

@[reducible, inline]

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

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

Equations

• WeierstrassCurve.Projective.toAffine W' = W'

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

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

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

Projective coordinates

theorem WeierstrassCurve.Projective.smul_fin3 {R : Type r} [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 r} [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

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

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

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

Equations

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

@[reducible, inline]

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

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

Equations

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

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

@[simp]

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

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

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

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

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

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

theorem WeierstrassCurve.Projective.Y_eq_of_equiv {R : Type r} [CommRing R] {P 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 r} [CommRing R] {P 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 r} [CommRing R] {P Q : Fin 3 → R} (hPz : P 2 ≠ 0) (hQz : Q 2 = 0) : ¬P ≈ Q

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

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

This is represented as a term of type MvPolynomial (Fin 3) R, where X 0, X 1, and X 2 represent X, Y, and Z respectively.

Equations

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

theorem WeierstrassCurve.Projective.eval_polynomial {R : Type r} [CommRing R] {W' : Projective 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 u} [Field F] {W : 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) (toAffine W).polynomial

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

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

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

Equations

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

theorem WeierstrassCurve.Projective.equation_iff {R : Type r} [CommRing R] {W' : Projective 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 r} [CommRing R] {W' : Projective 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 r} [CommRing R] {W' : Projective R} {P Q : Fin 3 → R} (h : P ≈ Q) : W'.Equation P ↔ W'.Equation Q

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

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

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

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

theorem WeierstrassCurve.Projective.X_eq_zero_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) : P 0 = 0

Nonsingular Weierstrass equations

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

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

Equations

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

theorem WeierstrassCurve.Projective.polynomialX_eq {R : Type r} [CommRing R] {W' : Projective 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 r} [CommRing R] {W' : Projective 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 u} [Field F] {W : 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) (toAffine W).polynomialX

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

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

Equations

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

theorem WeierstrassCurve.Projective.polynomialY_eq {R : Type r} [CommRing R] {W' : Projective 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 r} [CommRing R] {W' : Projective 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 u} [Field F] {W : 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) (toAffine W).polynomialY

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

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

Equations

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

theorem WeierstrassCurve.Projective.polynomialZ_eq {R : Type r} [CommRing R] {W' : Projective 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 r} [CommRing R] {W' : Projective 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 r} [CommRing R] {W' : Projective 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 in projective coordinates.

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

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

In other words, either W_X(x, y, z) ≠ 0, W_Y(x, y, z) ≠ 0, or W_Z(x, y, z) ≠ 0.

Note that this definition is only mathematically accurate for fields.

Equations

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

theorem WeierstrassCurve.Projective.nonsingular_iff {R : Type r} [CommRing R] {W' : Projective 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 r} [CommRing R] {W' : Projective 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 r} [CommRing R] {W' : Projective R} {P Q : Fin 3 → R} (h : P ≈ Q) : W'.Nonsingular P ↔ W'.Nonsingular Q

theorem WeierstrassCurve.Projective.nonsingular_of_Z_eq_zero {R : Type r} [CommRing R] {W' : Projective 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 r} [CommRing R] {W' : Projective R} [Nontrivial R] : W'.Nonsingular ![0, 1, 0]

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

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

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

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

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

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

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

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

Note that this definition is only mathematically accurate for fields.

Equations

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

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

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

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

@[deprecated WeierstrassCurve.Projective.equation_smul (since := "2024-08-27")]

theorem WeierstrassCurve.Projective.equation_smul_iff {R : Type r} [CommRing R] {W' : Projective 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 (since := "2024-08-27")]

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

Alias of WeierstrassCurve.Projective.nonsingularLift_zero.

@[deprecated WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero (since := "2024-08-27")]

theorem WeierstrassCurve.Projective.nonsingular_affine_of_Z_ne_zero {F : Type u} [Field F] {W : Projective F} {P : Fin 3 → F} (hPz : P 2 ≠ 0) : W.Nonsingular P ↔ (toAffine W).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 (since := "2024-08-27")]

theorem WeierstrassCurve.Projective.nonsingular_iff_affine_of_Z_ne_zero {F : Type u} [Field F] {W : Projective F} {P : Fin 3 → F} (hPz : P 2 ≠ 0) : W.Nonsingular P ↔ (toAffine W).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 (since := "2024-08-27")]

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

Alias of WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero.

@[deprecated WeierstrassCurve.Projective.nonsingular_smul (since := "2024-08-27")]

theorem WeierstrassCurve.Projective.nonsingular_smul_iff {R : Type r} [CommRing R] {W' : Projective 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 (since := "2024-08-27")]

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

Alias of WeierstrassCurve.Projective.nonsingular_zero.

Negation formulae

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

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

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]

Negation on point representatives

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

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

Equations

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

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

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

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

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

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

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

theorem WeierstrassCurve.Projective.neg_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'.neg P = -P 1 • ![0, 1, 0]

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

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

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

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

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

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

If P is a projective point representative on W, then W.negMap ⟦P⟧ is definitionally equivalent to W.neg P.

Equations

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

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

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

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

Addition on point representatives

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

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

Equations

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

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

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

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

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

theorem WeierstrassCurve.Projective.add_of_not_equiv {R : Type r} [CommRing R] {W' : Projective R} {P 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 r} [CommRing R] {W' : Projective R} {P Q : Fin 3 → R} (h : ¬P ≈ Q) {u v : R} (hu : IsUnit u) (hv : IsUnit v) : W'.add (u • P) (v • Q) = (u * v) ^ 2 • W'.add P Q

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

theorem WeierstrassCurve.Projective.add_equiv {R : Type r} [CommRing R] {W' : Projective R} {P P' Q 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 u} [Field F] {W : Projective F} {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) (hPz : P 2 = 0) (hQz : Q 2 = 0) : W.add P Q = P 1 ^ 4 • ![0, 1, 0]

theorem WeierstrassCurve.Projective.add_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) (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 r} [CommRing R] {W' : Projective R} [NoZeroDivisors R] {P 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 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.add P Q = W.dblU P • ![0, 1, 0]

theorem WeierstrassCurve.Projective.add_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) : W.add P Q = addU P Q • ![0, 1, 0]

theorem WeierstrassCurve.Projective.add_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) : W.add P Q = 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]

theorem WeierstrassCurve.Projective.add_of_X_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) : W.add 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]

theorem WeierstrassCurve.Projective.nonsingular_add {F : Type u} [Field F] {W : Projective F} {P 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 r} [CommRing R] (W' : Projective R) (P Q : PointClass R) : PointClass R

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

If P and Q are two projective point representatives on W, then W.addMap ⟦P⟧ ⟦Q⟧ is definitionally equivalent to W.add P Q.

Equations

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

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

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

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

theorem WeierstrassCurve.Projective.addMap_of_Y_eq {F : Type u} [Field F] {W : Projective F} {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Equation Q) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 = 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 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) (hxy : ¬(P 0 * Q 2 = Q 0 * P 2 ∧ P 1 * Q 2 = W.negY Q * P 2)) : W.addMap ⟦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]⟧

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

Nonsingular rational points

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

A nonsingular projective point on a Weierstrass curve W.

• point : PointClass R

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

• nonsingular : W'.NonsingularLift self.point

  The nonsingular condition underlying a nonsingular projective point on W.

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

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

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

Equations

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

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

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

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

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

Equations

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

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

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

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

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

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

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

Equations

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

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

Equations

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

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

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

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

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

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

Equations

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

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

Equations

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

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

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

Equivalence with affine coordinates

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

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

Equations

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

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

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

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

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

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

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

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

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

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

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

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

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

Equations

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

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

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

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

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

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

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

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

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

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

Equations

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

@[simp]

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

@[simp]

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

Maps across ring homomorphisms

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

Base changes across algebra homomorphisms

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[reducible, inline]

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

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

Equations

• P.toProjective = WeierstrassCurve.Projective.Point.fromAffine P