Nonsingular points and the group law in projective coordinates

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

This file defines the group law on nonsingular projective points.

Main definitions

• 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.nonsingular_neg: negation preserves the nonsingular condition.
• WeierstrassCurve.Projective.nonsingular_add: addition preserves the nonsingular condition.
• WeierstrassCurve.Projective.Point.instAddCommGroup: the type of nonsingular projective 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 projective point on W can be given by [x : y : z] and the nonsingular condition on any representative.

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.

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

References

J Silverman, The Arithmetic of Elliptic Curves

Tags

elliptic curve, projective, point, group law

Negation on projective 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 projective 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 projective 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.instZeroOfNontrivial {R : Type r} [CommRing R] {W' : Projective R} [Nontrivial R] : Zero W'.Point

Equations

• WeierstrassCurve.Projective.Point.instZeroOfNontrivial = { 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]⟧

theorem WeierstrassCurve.Projective.Point.mk_ne_zero {R : Type r} [CommRing R] {W' : Projective R} [Nontrivial R] {X Y : R} (h : W'.NonsingularLift ⟦![X, Y, 1]⟧) : mk h ≠ 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_some_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

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

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

Alias of WeierstrassCurve.Projective.Point.fromAffine_some_ne_zero.

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.instNeg {F : Type u} [Field F] {W : Projective F} : Neg W.Point

Equations

• WeierstrassCurve.Projective.Point.instNeg = { 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.instAdd {F : Type u} [Field F] {W : Projective F} : Add W.Point

Equations

• WeierstrassCurve.Projective.Point.instAdd = { 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 between projective and 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_symm_apply {F : Type u} [Field F] (W : Projective F) (a✝ : (Projective.toAffine W).Point) : (toAffineAddEquiv W).symm a✝ = fromAffine a✝

@[simp]

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

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

Equations

• WeierstrassCurve.Projective.Point.instAddCommGroup = AddCommGroup.mk ⋯

Maps and base changes

@[simp]

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

@[simp]

theorem WeierstrassCurve.Projective.map_add {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) : (map W f).toProjective.add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W.add P Q

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

theorem WeierstrassCurve.Projective.baseChange_add {R : Type r} {S : Type s} {F : Type u} {K : Type v} [CommRing R] [CommRing S] [Field F] [Field K] {W' : Projective R} [Algebra R S] [Algebra R F] [Algebra S F] [IsScalarTower R S F] [Algebra R K] [Algebra S K] [IsScalarTower R S K] (f : F →ₐ[S] K) {P 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 r} [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