Nonsingular points and the group law in Jacobian coordinates

Let W be a Weierstrass curve over a field F. The nonsingular Jacobian points of W can be endowed with an group law, which is uniquely determined by the formulae in Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Formula.lean and follows from an equivalence with the nonsingular points W⟮F⟯ in affine coordinates.

This file defines the group law on nonsingular Jacobian points.

Main definitions

• WeierstrassCurve.Jacobian.neg: the negation of a point representative.
• WeierstrassCurve.Jacobian.negMap: the negation of a point class.
• WeierstrassCurve.Jacobian.add: the addition of two point representatives.
• WeierstrassCurve.Jacobian.addMap: the addition of two point classes.
• WeierstrassCurve.Jacobian.Point: a nonsingular Jacobian point.
• WeierstrassCurve.Jacobian.Point.neg: the negation of a nonsingular Jacobian point.
• WeierstrassCurve.Jacobian.Point.add: the addition of two nonsingular Jacobian points.
• WeierstrassCurve.Jacobian.Point.toAffineAddEquiv: the equivalence between the type of nonsingular Jacobian points with the type of nonsingular points W⟮F⟯ in affine coordinates.

Main statements

• WeierstrassCurve.Jacobian.nonsingular_neg: negation preserves the nonsingular condition.
• WeierstrassCurve.Jacobian.nonsingular_add: addition preserves the nonsingular condition.
• WeierstrassCurve.Jacobian.Point.instAddCommGroup: the type of nonsingular Jacobian points forms an abelian group under addition.

Implementation notes

Note that W(X, Y, Z) and its partial derivatives are independent of the point representative, and the nonsingularity condition already implies (x, y, z) ≠ (0, 0, 0), so a nonsingular Jacobian point on W can be given by [x : y : z] and the nonsingular condition on any representative.

A nonsingular Jacobian point representative can be converted to a nonsingular point in affine coordinates using WeiestrassCurve.Jacobian.Point.toAffine, which lifts to a map on nonsingular Jacobian points using WeiestrassCurve.Jacobian.Point.toAffineLift. Conversely, a nonsingular point in affine coordinates can be converted to a nonsingular Jacobian point using WeierstrassCurve.Jacobian.Point.fromAffine or WeierstrassCurve.Affine.Point.toJacobian.

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

References

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

Tags

elliptic curve, Jacobian, point, group law

Negation on Jacobian point representatives

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

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

Equations

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

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

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

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

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

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

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

theorem WeierstrassCurve.Jacobian.neg_of_Z_eq_zero' {R : Type r} [CommRing R] {W' : Jacobian R} {P : Fin 3 → R} (hPz : P 2 = 0) : W'.neg P = ![P 0, -P 1, 0]

theorem WeierstrassCurve.Jacobian.neg_of_Z_eq_zero {F : Type u} [Field F] {W : Jacobian F} {P : Fin 3 → F} (hP : W.Nonsingular P) (hPz : P 2 = 0) : W.neg P = -(P 1 / P 0) • ![1, 1, 0]

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

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

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

theorem WeierstrassCurve.Jacobian.addX_neg {R : Type r} [CommRing R] {W' : Jacobian R} {P : Fin 3 → R} (hP : W'.Equation P) : W'.addX P (W'.neg P) = W'.dblZ P ^ 2

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

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

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

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

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

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

Equations

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

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

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

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

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

Addition on Jacobian point representatives

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

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

Equations

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem WeierstrassCurve.Jacobian.add_of_Y_ne {F : Type u} [Field F] {W : Jacobian F} {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) (hy : P 1 * Q 2 ^ 3 ≠ Q 1 * P 2 ^ 3) : W.add P Q = addU P Q • ![1, 1, 0]

theorem WeierstrassCurve.Jacobian.add_of_Y_ne' {F : Type u} [Field F] {W : Jacobian F} {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) (hy : P 1 * Q 2 ^ 3 ≠ W.negY Q * P 2 ^ 3) : W.add P Q = W.dblZ P • ![W.toAffine.addX (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)), W.toAffine.addY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)), 1]

theorem WeierstrassCurve.Jacobian.add_of_X_ne {F : Type u} [Field F] {W : Jacobian F} {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 ≠ Q 0 * P 2 ^ 2) : W.add P Q = addZ P Q • ![W.toAffine.addX (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)), W.toAffine.addY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)), 1]

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

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

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

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

Equations

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

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

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

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

theorem WeierstrassCurve.Jacobian.addMap_of_Y_eq {F : Type u} [Field F] {W : Jacobian F} {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Equation Q) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2) (hy' : P 1 * Q 2 ^ 3 = W.negY Q * P 2 ^ 3) : W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![1, 1, 0]⟧

theorem WeierstrassCurve.Jacobian.addMap_of_Z_ne_zero {F : Type u} [Field F] {W : Jacobian F} {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hxy : ¬(P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 ∧ P 1 * Q 2 ^ 3 = W.negY Q * P 2 ^ 3)) : W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![W.toAffine.addX (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)), W.toAffine.addY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)), 1]⟧

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

Nonsingular Jacobian points

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

A nonsingular Jacobian point on a Weierstrass curve W.

• point : PointClass R

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

• nonsingular : W'.NonsingularLift self.point

  The nonsingular condition underlying a nonsingular Jacobian point on W.

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

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

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

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

Equations

• WeierstrassCurve.Jacobian.Point.instZeroOfNontrivial = { zero := { point := ⟦![1, 1, 0]⟧, nonsingular := ⋯ } }

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

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

theorem WeierstrassCurve.Jacobian.Point.mk_ne_zero {R : Type r} [CommRing R] {W' : Jacobian R} [Nontrivial R] {X Y : R} (h : W'.NonsingularLift ⟦![X, Y, 1]⟧) : { point := ⟦![X, Y, 1]⟧, nonsingular := h } ≠ 0

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

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

Equations

• WeierstrassCurve.Jacobian.Point.fromAffine WeierstrassCurve.Affine.Point.zero = 0
• WeierstrassCurve.Jacobian.Point.fromAffine (WeierstrassCurve.Affine.Point.some h) = { point := ⟦![x_1, y, 1]⟧, nonsingular := ⋯ }

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

theorem WeierstrassCurve.Jacobian.Point.fromAffine_some {R : Type r} [CommRing R] {W' : Jacobian R} [Nontrivial R] {X Y : R} (h : W'.toAffine.Nonsingular X Y) : fromAffine (Affine.Point.some h) = { point := ⟦![X, Y, 1]⟧, nonsingular := ⋯ }

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

@[deprecated WeierstrassCurve.Jacobian.Point.fromAffine_some_ne_zero (since := "2025-03-01")]

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

Alias of WeierstrassCurve.Jacobian.Point.fromAffine_some_ne_zero.

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

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

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

Equations

• P.neg = { point := W.negMap P.point, nonsingular := ⋯ }

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

Equations

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

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

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

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

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

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

Equations

• P.add Q = { point := W.addMap P.point Q.point, nonsingular := ⋯ }

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

Equations

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

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

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

Equivalence between Jacobian and affine coordinates

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

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

Equations

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

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

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

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

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

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

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

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

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

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

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

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

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

Equations

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

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

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

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

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

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

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

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

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

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

Equations

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

@[simp]

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

@[simp]

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

noncomputable instance WeierstrassCurve.Jacobian.Point.instAddCommGroup {F : Type u} [Field F] {W : Jacobian F} : AddCommGroup W.Point

Equations

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

Maps and base changes

@[simp]

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

@[simp]

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

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

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

@[reducible, inline]

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

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

Equations

• P.toJacobian = WeierstrassCurve.Jacobian.Point.fromAffine P