# Documentation

Mathlib.AlgebraicGeometry.EllipticCurve.Point

# Nonsingular rational points on Weierstrass curves #

This file defines the type of nonsingular rational points on a Weierstrass curve over a field and proves that it forms an abelian group under a geometric secant-and-tangent process.

## Mathematical background #

Let W be a Weierstrass curve over a field F. A rational point on W is simply a point $[X:Y:Z]$ defined over F in the projective plane satisfying the homogeneous cubic equation $Y^2Z + a_1XYZ + a_3YZ^2 = X^3 + a_2X^2Z + a_4XZ^2 + a_6Z^3$. Any such point either lies in the affine chart $Z \ne 0$ and satisfies the Weierstrass equation obtained by replacing $X/Z$ with $X$ and $Y/Z$ with $Y$, or is the unique point at infinity $0 := [0:1:0]$ when $Z = 0$. With this new description, a nonsingular rational point on W is either $0$ or an affine point $(x, y)$ where the partial derivatives $W_X(X, Y)$ and $W_Y(X, Y)$ do not vanish simultaneously. For a field extension K of F, a K-rational point is simply a rational point on W base changed to K.

The set of nonsingular rational points forms an abelian group under a secant-and-tangent process.

• The identity rational point is 0.
• Given a nonsingular rational point P, its negation -P is defined to be the unique third point of intersection between W and the line through 0 and P. Explicitly, if P is $(x, y)$, then -P is $(x, -y - a_1x - a_3)$.
• Given two points P and Q, their addition P + Q is defined to be the negation of the unique third point of intersection between W and the line L through P and Q. Explicitly, let P be $(x_1, y_1)$ and let Q be $(x_2, y_2)$.
• If $x_1 = x_2$ and $y_1 = -y_2 - a_1x_2 - a_3$, then L is vertical and P + Q is 0.
• If $x_1 = x_2$ and $y_1 \ne -y_2 - a_1x_2 - a_3$, then L is the tangent of W at P = Q, and has slope $\ell := (3x_1^2 + 2a_2x_1 + a_4 - a_1y_1) / (2y_1 + a_1x_1 + a_3)$.
• Otherwise $x_1 \ne x_2$, then L is the secant of W through P and Q, and has slope $\ell := (y_1 - y_2) / (x_1 - x_2)$. In the latter two cases, the $X$-coordinate of P + Q is then the unique third solution of the equation obtained by substituting the line $Y = \ell(X - x_1) + y_1$ into the Weierstrass equation, and can be written down explicitly as $x := \ell^2 + a_1\ell - a_2 - x_1 - x_2$ by inspecting the $X^2$ terms. The $Y$-coordinate of P + Q, after applying the final negation that maps $Y$ to $-Y - a_1X - a_3$, is precisely $y := -(\ell(x - x_1) + y_1) - a_1x - a_3$. The group law on this set is then uniquely determined by these constructions.

## Main definitions #

• WeierstrassCurve.Point: the type of nonsingular rational points on a Weierstrass curve W.
• WeierstrassCurve.Point.add: the addition of two nonsingular rational points on W.

## Main statements #

• WeierstrassCurve.Point.instAddCommGroupPoint: the type of nonsingular rational points on W forms an abelian group under addition.

## Notations #

• W⟮K⟯: the group of nonsingular rational points on W base changed to K.

## References #

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

## Tags #

elliptic curve, rational point, group law

### Polynomials associated to nonsingular rational points on a Weierstrass curve #

noncomputable def WeierstrassCurve.negPolynomial {R : Type u} [] (W : ) :

The polynomial $-Y - a_1X - a_3$ associated to negation.

Instances For
def WeierstrassCurve.negY {R : Type u} [] (W : ) (x₁ : R) (y₁ : R) :
R

The $Y$-coordinate of the negation of an affine point in W.

This depends on W, and has argument order: $x_1$, $y_1$.

Instances For
theorem WeierstrassCurve.negY_negY {R : Type u} [] (W : ) (x₁ : R) (y₁ : R) :
WeierstrassCurve.negY W x₁ () = y₁
theorem WeierstrassCurve.baseChange_negY {R : Type u} [] (W : ) (A : Type v) [] [Algebra R A] (x₁ : R) (y₁ : R) :
WeierstrassCurve.negY () (↑() x₁) (↑() y₁) = ↑() ()
theorem WeierstrassCurve.baseChange_negY_of_baseChange {R : Type u} [] (W : ) (A : Type v) [] [Algebra R A] (B : Type w) [] [Algebra R B] [Algebra A B] [] (x₁ : A) (y₁ : A) :
WeierstrassCurve.negY () (↑() x₁) (↑() y₁) = ↑() ()
theorem WeierstrassCurve.eval_negPolynomial {R : Type u} [] (W : ) (x₁ : R) (y₁ : R) :
Polynomial.eval x₁ (Polynomial.eval (Polynomial.C y₁) ()) =
noncomputable def WeierstrassCurve.linePolynomial {R : Type u} [] (x₁ : R) (y₁ : R) (L : R) :

The polynomial $L(X - x_1) + y_1$ associated to the line $Y = L(X - x_1) + y_1$, with a slope of $L$ that passes through an affine point $(x_1, y_1)$.

This does not depend on W, and has argument order: $x_1$, $y_1$, $L$.

Instances For
theorem WeierstrassCurve.XYIdeal_eq₁ {R : Type u} [] (W : ) (x₁ : R) (y₁ : R) (L : R) :
WeierstrassCurve.CoordinateRing.XYIdeal W x₁ (Polynomial.C y₁) =
noncomputable def WeierstrassCurve.addPolynomial {R : Type u} [] (W : ) (x₁ : R) (y₁ : R) (L : R) :

The polynomial obtained by substituting the line $Y = L*(X - x_1) + y_1$, with a slope of $L$ that passes through an affine point $(x_1, y_1)$, into the polynomial $W(X, Y)$ associated to W. If such a line intersects W at another point $(x_2, y_2)$, then the roots of this polynomial are precisely $x_1$, $x_2$, and the $X$-coordinate of the addition of $(x_1, y_1)$ and $(x_2, y_2)$.

This depends on W, and has argument order: $x_1$, $y_1$, $L$.

Instances For
theorem WeierstrassCurve.C_addPolynomial {R : Type u} [] (W : ) (x₁ : R) (y₁ : R) (L : R) :
Polynomial.C () = (Polynomial.X - Polynomial.C ()) * ( - Polynomial.C ()) +
theorem WeierstrassCurve.CoordinateRing.C_addPolynomial {R : Type u} [] (W : ) (x₁ : R) (y₁ : R) (L : R) :
↑() (Polynomial.C ()) = ↑() ((Polynomial.X - Polynomial.C ()) * ( - Polynomial.C ()))
theorem WeierstrassCurve.addPolynomial_eq {R : Type u} [] (W : ) (x₁ : R) (y₁ : R) (L : R) :
= -Cubic.toPoly { a := 1, b := -L ^ 2 - W.a₁ * L + W.a₂, c := 2 * x₁ * L ^ 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * L + (-W.a₁ * y₁ + W.a₄), d := -x₁ ^ 2 * L ^ 2 + (2 * x₁ * y₁ + W.a₃ * x₁) * L - (y₁ ^ 2 + W.a₃ * y₁ - W.a₆) }
def WeierstrassCurve.addX {R : Type u} [] (W : ) (x₁ : R) (x₂ : R) (L : R) :
R

The $X$-coordinate of the addition of two affine points $(x_1, y_1)$ and $(x_2, y_2)$ in W, where the line through them is not vertical and has a slope of $L$.

This depends on W, and has argument order: $x_1$, $x_2$, $L$.

Instances For
theorem WeierstrassCurve.baseChange_addX {R : Type u} [] (W : ) (A : Type v) [] [Algebra R A] (x₁ : R) (x₂ : R) (L : R) :
WeierstrassCurve.addX () (↑() x₁) (↑() x₂) (↑() L) = ↑() (WeierstrassCurve.addX W x₁ x₂ L)
theorem WeierstrassCurve.baseChange_addX_of_baseChange {R : Type u} [] (W : ) (A : Type v) [] [Algebra R A] (B : Type w) [] [Algebra R B] [Algebra A B] [] (x₁ : A) (x₂ : A) (L : A) :
WeierstrassCurve.addX () (↑() x₁) (↑() x₂) (↑() L) = ↑() ()
def WeierstrassCurve.addY' {R : Type u} [] (W : ) (x₁ : R) (x₂ : R) (y₁ : R) (L : R) :
R

The $Y$-coordinate, before applying the final negation, of the addition of two affine points $(x_1, y_1)$ and $(x_2, y_2)$, where the line through them is not vertical and has a slope of $L$.

This depends on W, and has argument order: $x_1$, $x_2$, $y_1$, $L$.

Instances For
theorem WeierstrassCurve.baseChange_addY' {R : Type u} [] (W : ) (A : Type v) [] [Algebra R A] (x₁ : R) (x₂ : R) (y₁ : R) (L : R) :
WeierstrassCurve.addY' () (↑() x₁) (↑() x₂) (↑() y₁) (↑() L) = ↑() (WeierstrassCurve.addY' W x₁ x₂ y₁ L)
theorem WeierstrassCurve.baseChange_addY'_of_baseChange {R : Type u} [] (W : ) (A : Type v) [] [Algebra R A] (B : Type w) [] [Algebra R B] [Algebra A B] [] (x₁ : A) (x₂ : A) (y₁ : A) (L : A) :
WeierstrassCurve.addY' () (↑() x₁) (↑() x₂) (↑() y₁) (↑() L) = ↑() (WeierstrassCurve.addY' () x₁ x₂ y₁ L)
def WeierstrassCurve.addY {R : Type u} [] (W : ) (x₁ : R) (x₂ : R) (y₁ : R) (L : R) :
R

The $Y$-coordinate of the addition of two affine points $(x_1, y_1)$ and $(x_2, y_2)$ in W, where the line through them is not vertical and has a slope of $L$.

This depends on W, and has argument order: $x_1$, $x_2$, $y_1$, $L$.

Instances For
theorem WeierstrassCurve.baseChange_addY {R : Type u} [] (W : ) (A : Type v) [] [Algebra R A] (x₁ : R) (x₂ : R) (y₁ : R) (L : R) :
WeierstrassCurve.addY () (↑() x₁) (↑() x₂) (↑() y₁) (↑() L) = ↑() (WeierstrassCurve.addY W x₁ x₂ y₁ L)
theorem WeierstrassCurve.baseChange_addY_of_baseChange {R : Type u} [] (W : ) (A : Type v) [] [Algebra R A] (B : Type w) [] [Algebra R B] [Algebra A B] [] (x₁ : A) (x₂ : A) (y₁ : A) (L : A) :
WeierstrassCurve.addY () (↑() x₁) (↑() x₂) (↑() y₁) (↑() L) = ↑() (WeierstrassCurve.addY () x₁ x₂ y₁ L)
theorem WeierstrassCurve.XYIdeal_add_eq {R : Type u} [] (W : ) (x₁ : R) (x₂ : R) (y₁ : R) (L : R) :
WeierstrassCurve.CoordinateRing.XYIdeal W (WeierstrassCurve.addX W x₁ x₂ L) (Polynomial.C (WeierstrassCurve.addY W x₁ x₂ y₁ L)) = Ideal.span {↑() ( - Polynomial.C ())}
theorem WeierstrassCurve.equation_add_iff {R : Type u} [] (W : ) (x₁ : R) (x₂ : R) (y₁ : R) (L : R) :
theorem WeierstrassCurve.nonsingular_add_of_eval_derivative_ne_zero {R : Type u} [] (W : ) (x₁ : R) (x₂ : R) (y₁ : R) (L : R) (hx' : WeierstrassCurve.equation W (WeierstrassCurve.addX W x₁ x₂ L) (WeierstrassCurve.addY' W x₁ x₂ y₁ L)) (hx : Polynomial.eval (WeierstrassCurve.addX W x₁ x₂ L) (Polynomial.derivative ()) 0) :

### The type of nonsingular rational points on a Weierstrass curve #

inductive WeierstrassCurve.Point {R : Type u} [] (W : ) :
• zero: {R : Type u} → [inst : ] → {W : } →
• some: {R : Type u} → [inst : ] → {W : } → {x y : R} →

A nonsingular rational point on a Weierstrass curve W over R. This is either the point at infinity WeierstrassCurve.Point.zero or an affine point WeierstrassCurve.Point.some $(x, y)$ satisfying the equation $y^2 + a_1xy + a_3y = x^3 + a_2x^2 + a_4x + a_6$ of W.

Instances For

For an algebraic extension S of R, The type of nonsingular S-rational points on W.

Instances For
theorem WeierstrassCurve.Point.zero_def {R : Type u} [] (W : ) :
WeierstrassCurve.Point.zero = 0
theorem WeierstrassCurve.equation_neg_iff {R : Type u} [] {W : } {x₁ : R} {y₁ : R} :
theorem WeierstrassCurve.equation_neg_of {R : Type u} [] {W : } {x₁ : R} {y₁ : R} (h : WeierstrassCurve.equation W x₁ ()) :
theorem WeierstrassCurve.equation_neg {R : Type u} [] {W : } {x₁ : R} {y₁ : R} (h : ) :

The negation of an affine point in W lies in W.

theorem WeierstrassCurve.nonsingular_neg_iff {R : Type u} [] {W : } {x₁ : R} {y₁ : R} :
theorem WeierstrassCurve.nonsingular_neg_of {R : Type u} [] {W : } {x₁ : R} {y₁ : R} (h : WeierstrassCurve.nonsingular W x₁ ()) :
theorem WeierstrassCurve.nonsingular_neg {R : Type u} [] {W : } {x₁ : R} {y₁ : R} (h : ) :

The negation of a nonsingular affine point in W is nonsingular.

def WeierstrassCurve.Point.neg {R : Type u} [] {W : } :

The negation of a nonsingular rational point.

Given a nonsingular rational point P, use -P instead of neg P.

Instances For
instance WeierstrassCurve.Point.instNegPoint {R : Type u} [] {W : } :
theorem WeierstrassCurve.Point.neg_def {R : Type u} [] {W : } (P : ) :
@[simp]
theorem WeierstrassCurve.Point.neg_zero {R : Type u} [] {W : } :
-0 = 0
@[simp]
theorem WeierstrassCurve.Point.neg_some {R : Type u} [] {W : } {x₁ : R} {y₁ : R} (h : ) :

### Slopes of lines through nonsingular rational points on a Weierstrass curve #

noncomputable def WeierstrassCurve.slope {F : Type u} [] (W : ) (x₁ : F) (x₂ : F) (y₁ : F) (y₂ : F) :
F

The slope of the line through two affine points $(x_1, y_1)$ and $(x_2, y_2)$ in W. If $x_1 \ne x_2$, then this line is the secant of W through $(x_1, y_1)$ and $(x_2, y_2)$, and has slope $(y_1 - y_2) / (x_1 - x_2)$. Otherwise, if $y_1 \ne -y_1 - a_1x_1 - a_3$, then this line is the tangent of W at $(x_1, y_1) = (x_2, y_2)$, and has slope $(3x_1^2 + 2a_2x_1 + a_4 - a_1y_1) / (2y_1 + a_1x_1 + a_3)$. Otherwise, this line is vertical, and has undefined slope, in which case this function returns the value 0.

This depends on W, and has argument order: $x_1$, $x_2$, $y_1$, $y_2$.

Instances For
@[simp]
theorem WeierstrassCurve.slope_of_Y_eq {F : Type u} [] {W : } {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (hx : x₁ = x₂) (hy : y₁ = ) :
WeierstrassCurve.slope W x₁ x₂ y₁ y₂ = 0
@[simp]
theorem WeierstrassCurve.slope_of_Y_ne {F : Type u} [] {W : } {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (hx : x₁ = x₂) (hy : y₁ ) :
WeierstrassCurve.slope W x₁ x₂ y₁ y₂ = (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - )
@[simp]
theorem WeierstrassCurve.slope_of_X_ne {F : Type u} [] {W : } {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (hx : x₁ x₂) :
WeierstrassCurve.slope W x₁ x₂ y₁ y₂ = (y₁ - y₂) / (x₁ - x₂)
theorem WeierstrassCurve.slope_of_Y_ne_eq_eval {F : Type u} [] {W : } {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (hx : x₁ = x₂) (hy : y₁ ) :
WeierstrassCurve.slope W x₁ x₂ y₁ y₂ = -Polynomial.eval x₁ (Polynomial.eval (Polynomial.C y₁) ()) / Polynomial.eval x₁ (Polynomial.eval (Polynomial.C y₁) ())
theorem WeierstrassCurve.baseChange_slope {F : Type u} [] {W : } (K : Type v) [] [Algebra F K] {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} :
WeierstrassCurve.slope () (↑() x₁) (↑() x₂) (↑() y₁) (↑() y₂) = ↑() (WeierstrassCurve.slope W x₁ x₂ y₁ y₂)
theorem WeierstrassCurve.baseChange_slope_of_baseChange {R : Type u} [] (W : ) (F : Type v) [] [Algebra R F] (K : Type w) [] [Algebra R K] [Algebra F K] [] (x₁ : F) (x₂ : F) (y₁ : F) (y₂ : F) :
WeierstrassCurve.slope () (↑() x₁) (↑() x₂) (↑() y₁) (↑() y₂) = ↑() (WeierstrassCurve.slope () x₁ x₂ y₁ y₂)
theorem WeierstrassCurve.Y_eq_of_X_eq {F : Type u} [] {W : } {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁' : ) (h₂' : ) (hx : x₁ = x₂) :
y₁ = y₂ y₁ =
theorem WeierstrassCurve.Y_eq_of_Y_ne {F : Type u} [] {W : } {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁' : ) (h₂' : ) (hx : x₁ = x₂) (hy : y₁ ) :
y₁ = y₂
theorem WeierstrassCurve.XYIdeal_eq₂ {F : Type u} [] {W : } {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁' : ) (h₂' : ) (hxy : x₁ = x₂y₁ ) :
theorem WeierstrassCurve.addPolynomial_slope {F : Type u} [] {W : } {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁' : ) (h₂' : ) (hxy : x₁ = x₂y₁ ) :
WeierstrassCurve.addPolynomial W x₁ y₁ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂) = -((Polynomial.X - Polynomial.C x₁) * (Polynomial.X - Polynomial.C x₂) * (Polynomial.X - Polynomial.C (WeierstrassCurve.addX W x₁ x₂ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂))))
theorem WeierstrassCurve.CoordinateRing.C_addPolynomial_slope {F : Type u} [] {W : } {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁' : ) (h₂' : ) (hxy : x₁ = x₂y₁ ) :
↑() (Polynomial.C (WeierstrassCurve.addPolynomial W x₁ y₁ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂))) = -( * WeierstrassCurve.CoordinateRing.XClass W (WeierstrassCurve.addX W x₁ x₂ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂)))
theorem WeierstrassCurve.derivative_addPolynomial_slope {F : Type u} [] {W : } {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁' : ) (h₂' : ) (hxy : x₁ = x₂y₁ ) :
Polynomial.derivative (WeierstrassCurve.addPolynomial W x₁ y₁ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂)) = -((Polynomial.X - Polynomial.C x₁) * (Polynomial.X - Polynomial.C x₂) + (Polynomial.X - Polynomial.C x₁) * (Polynomial.X - Polynomial.C (WeierstrassCurve.addX W x₁ x₂ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂))) + (Polynomial.X - Polynomial.C x₂) * (Polynomial.X - Polynomial.C (WeierstrassCurve.addX W x₁ x₂ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂))))

### The addition law on nonsingular rational points on a Weierstrass curve #

theorem WeierstrassCurve.equation_add' {F : Type u} [] {W : } {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁' : ) (h₂' : ) (hxy : x₁ = x₂y₁ ) :
WeierstrassCurve.equation W (WeierstrassCurve.addX W x₁ x₂ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂)) (WeierstrassCurve.addY' W x₁ x₂ y₁ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂))

The addition of two affine points in W on a sloped line, before applying the final negation that maps $Y$ to $-Y - a_1X - a_3$, lies in W.

theorem WeierstrassCurve.equation_add {F : Type u} [] {W : } {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁' : ) (h₂' : ) (hxy : x₁ = x₂y₁ ) :
WeierstrassCurve.equation W (WeierstrassCurve.addX W x₁ x₂ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂)) (WeierstrassCurve.addY W x₁ x₂ y₁ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂))

The addition of two affine points in W on a sloped line lies in W.

theorem WeierstrassCurve.nonsingular_add' {F : Type u} [] {W : } {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁ : ) (h₂ : ) (hxy : x₁ = x₂y₁ ) :
WeierstrassCurve.nonsingular W (WeierstrassCurve.addX W x₁ x₂ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂)) (WeierstrassCurve.addY' W x₁ x₂ y₁ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂))

The addition of two nonsingular affine points in W on a sloped line, before applying the final negation that maps $Y$ to $-Y - a_1X - a_3$, is nonsingular.

theorem WeierstrassCurve.nonsingular_add {F : Type u} [] {W : } {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁ : ) (h₂ : ) (hxy : x₁ = x₂y₁ ) :
WeierstrassCurve.nonsingular W (WeierstrassCurve.addX W x₁ x₂ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂)) (WeierstrassCurve.addY W x₁ x₂ y₁ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂))

The addition of two nonsingular affine points in W on a sloped line is nonsingular.

noncomputable def WeierstrassCurve.Point.add {F : Type u} [] {W : } :

The addition of two nonsingular rational points.

Given two nonsingular rational points P and Q, use P + Q instead of add P Q.

Instances For
noncomputable instance WeierstrassCurve.Point.instAddPoint {F : Type u} [] {W : } :
theorem WeierstrassCurve.Point.add_def {F : Type u} [] {W : } (P : ) (Q : ) :
= P + Q
noncomputable instance WeierstrassCurve.Point.instAddZeroClassPoint {F : Type u} [] {W : } :
@[simp]
theorem WeierstrassCurve.Point.some_add_some_of_Y_eq {F : Type u} [] {W : } {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} {h₁ : } {h₂ : } (hx : x₁ = x₂) (hy : y₁ = ) :
@[simp]
theorem WeierstrassCurve.Point.some_add_self_of_Y_eq {F : Type u} [] {W : } {x₁ : F} {y₁ : F} {h₁ : } (hy : y₁ = ) :
@[simp]
theorem WeierstrassCurve.Point.some_add_some_of_Y_ne {F : Type u} [] {W : } {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} {h₁ : } {h₂ : } (hx : x₁ = x₂) (hy : y₁ ) :
= WeierstrassCurve.Point.some (_ : WeierstrassCurve.nonsingular W (WeierstrassCurve.addX W x₁ x₂ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂)) (WeierstrassCurve.addY W x₁ x₂ y₁ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂)))
theorem WeierstrassCurve.Point.some_add_some_of_Y_ne' {F : Type u} [] {W : } {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} {h₁ : } {h₂ : } (hx : x₁ = x₂) (hy : y₁ ) :
= -WeierstrassCurve.Point.some (_ : WeierstrassCurve.nonsingular W (WeierstrassCurve.addX W x₁ x₂ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂)) (WeierstrassCurve.addY' W x₁ x₂ y₁ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂)))
@[simp]
theorem WeierstrassCurve.Point.some_add_self_of_Y_ne {F : Type u} [] {W : } {x₁ : F} {y₁ : F} {h₁ : } (hy : y₁ ) :
= WeierstrassCurve.Point.some (_ : WeierstrassCurve.nonsingular W (WeierstrassCurve.addX W x₁ x₁ (WeierstrassCurve.slope W x₁ x₁ y₁ y₁)) (WeierstrassCurve.addY W x₁ x₁ y₁ (WeierstrassCurve.slope W x₁ x₁ y₁ y₁)))
theorem WeierstrassCurve.Point.some_add_self_of_Y_ne' {F : Type u} [] {W : } {x₁ : F} {y₁ : F} {h₁ : } (hy : y₁ ) :
= -WeierstrassCurve.Point.some (_ : WeierstrassCurve.nonsingular W (WeierstrassCurve.addX W x₁ x₁ (WeierstrassCurve.slope W x₁ x₁ y₁ y₁)) (WeierstrassCurve.addY' W x₁ x₁ y₁ (WeierstrassCurve.slope W x₁ x₁ y₁ y₁)))
@[simp]
theorem WeierstrassCurve.Point.some_add_some_of_X_ne {F : Type u} [] {W : } {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} {h₁ : } {h₂ : } (hx : x₁ x₂) :
= WeierstrassCurve.Point.some (_ : WeierstrassCurve.nonsingular W (WeierstrassCurve.addX W x₁ x₂ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂)) (WeierstrassCurve.addY W x₁ x₂ y₁ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂)))
theorem WeierstrassCurve.Point.some_add_some_of_X_ne' {F : Type u} [] {W : } {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} {h₁ : } {h₂ : } (hx : x₁ x₂) :
= -WeierstrassCurve.Point.some (_ : WeierstrassCurve.nonsingular W (WeierstrassCurve.addX W x₁ x₂ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂)) (WeierstrassCurve.addY' W x₁ x₂ y₁ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂)))

### The axioms for nonsingular rational points on a Weierstrass curve #

theorem WeierstrassCurve.XYIdeal_neg_mul {F : Type u} [] {W : } {x₁ : F} {y₁ : F} (h₁ : ) :
WeierstrassCurve.CoordinateRing.XYIdeal W x₁ (Polynomial.C ()) * WeierstrassCurve.CoordinateRing.XYIdeal W x₁ (Polynomial.C y₁) =
theorem WeierstrassCurve.XYIdeal_mul_XYIdeal {F : Type u} [] {W : } {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁' : ) (h₂' : ) (hxy : x₁ = x₂y₁ ) :
WeierstrassCurve.CoordinateRing.XIdeal W (WeierstrassCurve.addX W x₁ x₂ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂)) * (WeierstrassCurve.CoordinateRing.XYIdeal W x₁ (Polynomial.C y₁) * WeierstrassCurve.CoordinateRing.XYIdeal W x₂ (Polynomial.C y₂)) = WeierstrassCurve.CoordinateRing.YIdeal W (WeierstrassCurve.linePolynomial x₁ y₁ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂)) * WeierstrassCurve.CoordinateRing.XYIdeal W (WeierstrassCurve.addX W x₁ x₂ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂)) (Polynomial.C (WeierstrassCurve.addY W x₁ x₂ y₁ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂)))
noncomputable def WeierstrassCurve.XYIdeal' {F : Type u} [] {W : } {x₁ : F} {y₁ : F} (h₁ : ) :

The non-zero fractional ideal $\langle X - x, Y - y \rangle$ of $F(W)$ for some $x, y \in F$.

Instances For
theorem WeierstrassCurve.XYIdeal'_eq {F : Type u} [] {W : } {x₁ : F} {y₁ : F} (h₁ : ) :
= ↑(WeierstrassCurve.CoordinateRing.XYIdeal W x₁ (Polynomial.C y₁))
theorem WeierstrassCurve.mk_XYIdeal'_mul_mk_XYIdeal'_of_Y_eq {F : Type u} [] {W : } {x₁ : F} {y₁ : F} (h₁ : ) :
ClassGroup.mk (WeierstrassCurve.XYIdeal' (_ : WeierstrassCurve.nonsingular W x₁ ())) * ClassGroup.mk () = 1
theorem WeierstrassCurve.mk_XYIdeal'_mul_mk_XYIdeal' {F : Type u} [] {W : } {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁ : ) (h₂ : ) (hxy : x₁ = x₂y₁ ) :
ClassGroup.mk () * ClassGroup.mk () = ClassGroup.mk (WeierstrassCurve.XYIdeal' (_ : WeierstrassCurve.nonsingular W (WeierstrassCurve.addX W x₁ x₂ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂)) (WeierstrassCurve.addY W x₁ x₂ y₁ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂))))
noncomputable def WeierstrassCurve.Point.toClassFun {F : Type u} [] {W : } :

The set function mapping an affine point $(x, y)$ of W to the class of the non-zero fractional ideal $\langle X - x, Y - y \rangle$ of $F(W)$ in the class group of $F[W]$.

Instances For
@[simp]
theorem WeierstrassCurve.Point.toClass_apply {F : Type u} [] {W : } :
∀ (a : ), WeierstrassCurve.Point.toClass a =
noncomputable def WeierstrassCurve.Point.toClass {F : Type u} [] {W : } :

The group homomorphism mapping an affine point $(x, y)$ of W to the class of the non-zero fractional ideal $\langle X - x, Y - y \rangle$ of $F(W)$ in the class group of $F[W]$.

Instances For
theorem WeierstrassCurve.Point.toClass_zero {F : Type u} [] {W : } :
WeierstrassCurve.Point.toClass 0 = 0
theorem WeierstrassCurve.Point.toClass_some {F : Type u} [] {W : } {x₁ : F} {y₁ : F} (h₁ : ) :
WeierstrassCurve.Point.toClass () = ClassGroup.mk ()
theorem WeierstrassCurve.Point.add_eq_zero {F : Type u} [] {W : } (P : ) (Q : ) :
P + Q = 0 P = -Q
theorem WeierstrassCurve.Point.add_left_neg {F : Type u} [] {W : } (P : ) :
-P + P = 0
theorem WeierstrassCurve.Point.neg_add_eq_zero {F : Type u} [] {W : } (P : ) (Q : ) :
-P + Q = 0 P = Q
theorem WeierstrassCurve.Point.toClass_eq_zero {F : Type u} [] {W : } (P : ) :
WeierstrassCurve.Point.toClass P = 0 P = 0
theorem WeierstrassCurve.Point.toClass_injective {F : Type u} [] {W : } :
Function.Injective WeierstrassCurve.Point.toClass
theorem WeierstrassCurve.Point.add_comm {F : Type u} [] {W : } (P : ) (Q : ) :
P + Q = Q + P
theorem WeierstrassCurve.Point.add_assoc {F : Type u} [] {W : } (P : ) (Q : ) (R : ) :
P + Q + R = P + (Q + R)
noncomputable instance WeierstrassCurve.Point.instAddCommGroupPoint {F : Type u} [] {W : } :

### Nonsingular rational points on a base changed Weierstrass curve #

def WeierstrassCurve.Point.ofBaseChangeFun {R : Type u} [] (W : ) (F : Type v) [] [Algebra R F] (K : Type w) [] [Algebra R K] [Algebra F K] [] :

The function from W⟮F⟯ to W⟮K⟯ induced by a base change from F to K.

Instances For
@[simp]
theorem WeierstrassCurve.Point.ofBaseChange_apply {R : Type u} [] (W : ) (F : Type v) [] [Algebra R F] (K : Type w) [] [Algebra R K] [Algebra F K] [] :
∀ (a : ), ↑() a =
def WeierstrassCurve.Point.ofBaseChange {R : Type u} [] (W : ) (F : Type v) [] [Algebra R F] (K : Type w) [] [Algebra R K] [Algebra F K] [] :

The group homomorphism from W⟮F⟯ to W⟮K⟯ induced by a base change from F to K.

Instances For
theorem WeierstrassCurve.Point.ofBaseChange_injective {R : Type u} [] (W : ) (F : Type v) [] [Algebra R F] (K : Type w) [] [Algebra R K] [Algebra F K] [] :

### Rational points on an elliptic curve #

def EllipticCurve.Point.mk {R : Type} [] [] (E : ) {x : R} {y : R} (h : WeierstrassCurve.equation E.toWeierstrassCurve x y) :
WeierstrassCurve.Point E.toWeierstrassCurve

An affine point on an elliptic curve E over R.

Instances For