# mathlib3documentation

algebraic_geometry.elliptic_curve.point

# Nonsingular rational points on Weierstrass curves #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

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

## Main statements #

• weierstrass_curve.point.add_comm_group: 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

## Tags #

elliptic curve, rational point, group law

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

noncomputable def weierstrass_curve.neg_polynomial {R : Type u} [comm_ring R] (W : weierstrass_curve R) :

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

Equations
@[simp]
def weierstrass_curve.neg_Y {R : Type u} [comm_ring R] (W : weierstrass_curve R) (x₁ 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$.

Equations
theorem weierstrass_curve.neg_Y_neg_Y {R : Type u} [comm_ring R] (W : weierstrass_curve R) (x₁ y₁ : R) :
W.neg_Y x₁ (W.neg_Y x₁ y₁) = y₁
theorem weierstrass_curve.base_change_neg_Y {R : Type u} [comm_ring R] (W : weierstrass_curve R) (A : Type v) [comm_ring A] [ A] (x₁ y₁ : R) :
(W.base_change A).neg_Y ( A) x₁) ( A) y₁) = A) (W.neg_Y x₁ y₁)
theorem weierstrass_curve.base_change_neg_Y_of_base_change {R : Type u} [comm_ring R] (W : weierstrass_curve R) (A : Type v) [comm_ring A] [ A] (B : Type w) [comm_ring B] [ B] [ B] [ B] (x₁ y₁ : A) :
(W.base_change B).neg_Y ( B) x₁) ( B) y₁) = B) ((W.base_change A).neg_Y x₁ y₁)
@[simp]
theorem weierstrass_curve.eval_neg_polynomial {R : Type u} [comm_ring R] (W : weierstrass_curve R) (x₁ y₁ : R) :
= W.neg_Y x₁ y₁
noncomputable def weierstrass_curve.line_polynomial {R : Type u} [comm_ring R] (x₁ y₁ 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$.

Equations
theorem weierstrass_curve.XY_ideal_eq₁ {R : Type u} [comm_ring R] (W : weierstrass_curve R) (x₁ y₁ L : R) :
noncomputable def weierstrass_curve.add_polynomial {R : Type u} [comm_ring R] (W : weierstrass_curve R) (x₁ y₁ 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$.

Equations
theorem weierstrass_curve.C_add_polynomial {R : Type u} [comm_ring R] (W : weierstrass_curve R) (x₁ y₁ L : R) :
theorem weierstrass_curve.add_polynomial_eq {R : Type u} [comm_ring R] (W : weierstrass_curve R) (x₁ y₁ L : R) :
W.add_polynomial x₁ y₁ L = -{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₆)}.to_poly
@[simp]
def weierstrass_curve.add_X {R : Type u} [comm_ring R] (W : weierstrass_curve R) (x₁ x₂ 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$.

Equations
theorem weierstrass_curve.base_change_add_X {R : Type u} [comm_ring R] (W : weierstrass_curve R) (A : Type v) [comm_ring A] [ A] (x₁ x₂ L : R) :
(W.base_change A).add_X ( A) x₁) ( A) x₂) ( A) L) = A) (W.add_X x₁ x₂ L)
theorem weierstrass_curve.base_change_add_X_of_base_change {R : Type u} [comm_ring R] (W : weierstrass_curve R) (A : Type v) [comm_ring A] [ A] (B : Type w) [comm_ring B] [ B] [ B] [ B] (x₁ x₂ L : A) :
(W.base_change B).add_X ( B) x₁) ( B) x₂) ( B) L) = B) ((W.base_change A).add_X x₁ x₂ L)
@[simp]
def weierstrass_curve.add_Y' {R : Type u} [comm_ring R] (W : weierstrass_curve R) (x₁ x₂ y₁ 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$.

Equations
theorem weierstrass_curve.base_change_add_Y' {R : Type u} [comm_ring R] (W : weierstrass_curve R) (A : Type v) [comm_ring A] [ A] (x₁ x₂ y₁ L : R) :
(W.base_change A).add_Y' ( A) x₁) ( A) x₂) ( A) y₁) ( A) L) = A) (W.add_Y' x₁ x₂ y₁ L)
theorem weierstrass_curve.base_change_add_Y'_of_base_change {R : Type u} [comm_ring R] (W : weierstrass_curve R) (A : Type v) [comm_ring A] [ A] (B : Type w) [comm_ring B] [ B] [ B] [ B] (x₁ x₂ y₁ L : A) :
(W.base_change B).add_Y' ( B) x₁) ( B) x₂) ( B) y₁) ( B) L) = B) ((W.base_change A).add_Y' x₁ x₂ y₁ L)
@[simp]
def weierstrass_curve.add_Y {R : Type u} [comm_ring R] (W : weierstrass_curve R) (x₁ x₂ y₁ 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$.

Equations
theorem weierstrass_curve.base_change_add_Y {R : Type u} [comm_ring R] (W : weierstrass_curve R) (A : Type v) [comm_ring A] [ A] (x₁ x₂ y₁ L : R) :
(W.base_change A).add_Y ( A) x₁) ( A) x₂) ( A) y₁) ( A) L) = A) (W.add_Y x₁ x₂ y₁ L)
theorem weierstrass_curve.base_change_add_Y_of_base_change {R : Type u} [comm_ring R] (W : weierstrass_curve R) (A : Type v) [comm_ring A] [ A] (B : Type w) [comm_ring B] [ B] [ B] [ B] (x₁ x₂ y₁ L : A) :
(W.base_change B).add_Y ( B) x₁) ( B) x₂) ( B) y₁) ( B) L) = B) ((W.base_change A).add_Y x₁ x₂ y₁ L)
theorem weierstrass_curve.XY_ideal_add_eq {R : Type u} [comm_ring R] (W : weierstrass_curve R) (x₁ x₂ y₁ L : R) :
(W.add_X x₁ x₂ L) (polynomial.C (W.add_Y x₁ x₂ y₁ L)) = ideal.span (W.neg_polynomial - polynomial.C L))} (W.add_X x₁ x₂ L)
theorem weierstrass_curve.equation_add_iff {R : Type u} [comm_ring R] (W : weierstrass_curve R) (x₁ x₂ y₁ L : R) :
theorem weierstrass_curve.nonsingular_add_of_eval_derivative_ne_zero {R : Type u} [comm_ring R] (W : weierstrass_curve R) (x₁ x₂ y₁ L : R) (hx' : W.equation (W.add_X x₁ x₂ L) (W.add_Y' x₁ x₂ y₁ L)) (hx : polynomial.eval (W.add_X x₁ x₂ L) (polynomial.derivative (W.add_polynomial x₁ y₁ L)) 0) :

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

inductive weierstrass_curve.point {R : Type u} [comm_ring R] (W : weierstrass_curve R) :

A nonsingular rational point on a Weierstrass curve W over R. This is either the point at infinity weierstrass_curve.point.zero or an affine point weierstrass_curve.point.some $(x, y)$ satisfying the equation $y^2 + a_1xy + a_3y = x^3 + a_2x^2 + a_4x + a_6$ of W. For an algebraic extension S of R, the type of nonsingular S-rational points on W is denoted W⟮S⟯.

Instances for weierstrass_curve.point
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem weierstrass_curve.equation_neg_iff {R : Type u} [comm_ring R] {W : weierstrass_curve R} {x₁ y₁ : R} :
W.equation x₁ (W.neg_Y x₁ y₁) W.equation x₁ y₁
theorem weierstrass_curve.equation_neg_of {R : Type u} [comm_ring R] {W : weierstrass_curve R} {x₁ y₁ : R} (h : W.equation x₁ (W.neg_Y x₁ y₁)) :
W.equation x₁ y₁
theorem weierstrass_curve.equation_neg {R : Type u} [comm_ring R] {W : weierstrass_curve R} {x₁ y₁ : R} (h : W.equation x₁ y₁) :
W.equation x₁ (W.neg_Y x₁ y₁)

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

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

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

The negation of a nonsingular rational point.

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

Equations
@[protected, instance]
Equations
@[simp]
theorem weierstrass_curve.point.neg_def {R : Type u} [comm_ring R] {W : weierstrass_curve R} (P : W.point) :
P.neg = -P
@[simp]
@[simp]
theorem weierstrass_curve.point.neg_some {R : Type u} [comm_ring R] {W : weierstrass_curve R} {x₁ y₁ : R} (h : W.nonsingular x₁ y₁) :
@[protected, instance]
Equations

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

noncomputable def weierstrass_curve.slope {F : Type u} [field F] (W : weierstrass_curve F) (x₁ x₂ y₁ 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$.

Equations
@[simp]
theorem weierstrass_curve.slope_of_Y_eq {F : Type u} [field F] {W : weierstrass_curve F} {x₁ x₂ y₁ y₂ : F} (hx : x₁ = x₂) (hy : y₁ = W.neg_Y x₂ y₂) :
W.slope x₁ x₂ y₁ y₂ = 0
@[simp]
theorem weierstrass_curve.slope_of_Y_ne {F : Type u} [field F] {W : weierstrass_curve F} {x₁ x₂ y₁ y₂ : F} (hx : x₁ = x₂) (hy : y₁ W.neg_Y x₂ y₂) :
W.slope x₁ x₂ y₁ y₂ = (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.neg_Y x₁ y₁)
@[simp]
theorem weierstrass_curve.slope_of_X_ne {F : Type u} [field F] {W : weierstrass_curve F} {x₁ x₂ y₁ y₂ : F} (hx : x₁ x₂) :
W.slope x₁ x₂ y₁ y₂ = (y₁ - y₂) / (x₁ - x₂)
theorem weierstrass_curve.slope_of_Y_ne_eq_eval {F : Type u} [field F] {W : weierstrass_curve F} {x₁ x₂ y₁ y₂ : F} (hx : x₁ = x₂) (hy : y₁ W.neg_Y x₂ y₂) :
W.slope x₁ x₂ y₁ y₂ = - W.polynomial_X) / W.polynomial_Y)
theorem weierstrass_curve.base_change_slope {F : Type u} [field F] {W : weierstrass_curve F} (K : Type v) [field K] [ K] {x₁ x₂ y₁ y₂ : F} :
(W.base_change K).slope ( K) x₁) ( K) x₂) ( K) y₁) ( K) y₂) = K) (W.slope x₁ x₂ y₁ y₂)
theorem weierstrass_curve.base_change_slope_of_base_change {R : Type u} [comm_ring R] (W : weierstrass_curve R) (F : Type v) [field F] [ F] (K : Type w) [field K] [ K] [ K] [ K] (x₁ x₂ y₁ y₂ : F) :
(W.base_change K).slope ( K) x₁) ( K) x₂) ( K) y₁) ( K) y₂) = K) ((W.base_change F).slope x₁ x₂ y₁ y₂)
theorem weierstrass_curve.Y_eq_of_X_eq {F : Type u} [field F] {W : weierstrass_curve F} {x₁ x₂ y₁ y₂ : F} (h₁' : W.equation x₁ y₁) (h₂' : W.equation x₂ y₂) (hx : x₁ = x₂) :
y₁ = y₂ y₁ = W.neg_Y x₂ y₂
theorem weierstrass_curve.Y_eq_of_Y_ne {F : Type u} [field F] {W : weierstrass_curve F} {x₁ x₂ y₁ y₂ : F} (h₁' : W.equation x₁ y₁) (h₂' : W.equation x₂ y₂) (hx : x₁ = x₂) (hy : y₁ W.neg_Y x₂ y₂) :
y₁ = y₂
theorem weierstrass_curve.XY_ideal_eq₂ {F : Type u} [field F] {W : weierstrass_curve F} {x₁ x₂ y₁ y₂ : F} (h₁' : W.equation x₁ y₁) (h₂' : W.equation x₂ y₂) (hxy : x₁ = x₂ y₁ W.neg_Y x₂ y₂) :
= (W.slope x₁ x₂ y₁ y₂))
theorem weierstrass_curve.add_polynomial_slope {F : Type u} [field F] {W : weierstrass_curve F} {x₁ x₂ y₁ y₂ : F} (h₁' : W.equation x₁ y₁) (h₂' : W.equation x₂ y₂) (hxy : x₁ = x₂ y₁ W.neg_Y x₂ y₂) :
W.add_polynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂) = - * * (polynomial.X - polynomial.C (W.add_X x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))
theorem weierstrass_curve.coordinate_ring.C_add_polynomial_slope {F : Type u} [field F] {W : weierstrass_curve F} {x₁ x₂ y₁ y₂ : F} (h₁' : W.equation x₁ y₁) (h₂' : W.equation x₂ y₂) (hxy : x₁ = x₂ y₁ W.neg_Y x₂ y₂) :
(polynomial.C (W.add_polynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) = - * (W.add_X x₁ x₂ (W.slope x₁ x₂ y₁ y₂)))
theorem weierstrass_curve.derivative_add_polynomial_slope {F : Type u} [field F] {W : weierstrass_curve F} {x₁ x₂ y₁ y₂ : F} (h₁' : W.equation x₁ y₁) (h₂' : W.equation x₂ y₂) (hxy : x₁ = x₂ y₁ W.neg_Y x₂ y₂) :
polynomial.derivative (W.add_polynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) = - * + * (polynomial.X - polynomial.C (W.add_X x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) + * (polynomial.X - polynomial.C (W.add_X x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))

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

theorem weierstrass_curve.equation_add' {F : Type u} [field F] {W : weierstrass_curve F} {x₁ x₂ y₁ y₂ : F} (h₁' : W.equation x₁ y₁) (h₂' : W.equation x₂ y₂) (hxy : x₁ = x₂ y₁ W.neg_Y x₂ y₂) :
W.equation (W.add_X x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.add_Y' x₁ x₂ y₁ (W.slope 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 weierstrass_curve.equation_add {F : Type u} [field F] {W : weierstrass_curve F} {x₁ x₂ y₁ y₂ : F} (h₁' : W.equation x₁ y₁) (h₂' : W.equation x₂ y₂) (hxy : x₁ = x₂ y₁ W.neg_Y x₂ y₂) :
W.equation (W.add_X x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.add_Y x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))

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

theorem weierstrass_curve.nonsingular_add' {F : Type u} [field F] {W : weierstrass_curve F} {x₁ x₂ y₁ y₂ : F} (h₁ : W.nonsingular x₁ y₁) (h₂ : W.nonsingular x₂ y₂) (hxy : x₁ = x₂ y₁ W.neg_Y x₂ y₂) :
W.nonsingular (W.add_X x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.add_Y' x₁ x₂ y₁ (W.slope 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 weierstrass_curve.nonsingular_add {F : Type u} [field F] {W : weierstrass_curve F} {x₁ x₂ y₁ y₂ : F} (h₁ : W.nonsingular x₁ y₁) (h₂ : W.nonsingular x₂ y₂) (hxy : x₁ = x₂ y₁ W.neg_Y x₂ y₂) :
W.nonsingular (W.add_X x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.add_Y x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))

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

noncomputable def weierstrass_curve.point.add {F : Type u} [field F] {W : weierstrass_curve F} :

The addition of two nonsingular rational points.

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

Equations
• = dite (x₁ = x₂) (λ (hx : x₁ = x₂), dite (y₁ = W.neg_Y x₂ y₂) (λ (hy : y₁ = W.neg_Y x₂ y₂), 0) (λ (hy : ¬y₁ = W.neg_Y x₂ y₂), (λ (hx : ¬x₁ = x₂),
@[protected, instance]
noncomputable def weierstrass_curve.point.has_add {F : Type u} [field F] {W : weierstrass_curve F} :
Equations
@[simp]
theorem weierstrass_curve.point.add_def {F : Type u} [field F] {W : weierstrass_curve F} (P Q : W.point) :
P.add Q = P + Q
@[protected, instance]
noncomputable def weierstrass_curve.point.add_zero_class {F : Type u} [field F] {W : weierstrass_curve F} :
Equations
@[simp]
theorem weierstrass_curve.point.some_add_some_of_Y_eq {F : Type u} [field F] {W : weierstrass_curve F} {x₁ x₂ y₁ y₂ : F} {h₁ : W.nonsingular x₁ y₁} {h₂ : W.nonsingular x₂ y₂} (hx : x₁ = x₂) (hy : y₁ = W.neg_Y x₂ y₂) :
@[simp]
theorem weierstrass_curve.point.some_add_self_of_Y_eq {F : Type u} [field F] {W : weierstrass_curve F} {x₁ y₁ : F} {h₁ : W.nonsingular x₁ y₁} (hy : y₁ = W.neg_Y x₁ y₁) :
@[simp]
theorem weierstrass_curve.point.some_add_some_of_Y_ne {F : Type u} [field F] {W : weierstrass_curve F} {x₁ x₂ y₁ y₂ : F} {h₁ : W.nonsingular x₁ y₁} {h₂ : W.nonsingular x₂ y₂} (hx : x₁ = x₂) (hy : y₁ W.neg_Y x₂ y₂) :
theorem weierstrass_curve.point.some_add_some_of_Y_ne' {F : Type u} [field F] {W : weierstrass_curve F} {x₁ x₂ y₁ y₂ : F} {h₁ : W.nonsingular x₁ y₁} {h₂ : W.nonsingular x₂ y₂} (hx : x₁ = x₂) (hy : y₁ W.neg_Y x₂ y₂) :
@[simp]
theorem weierstrass_curve.point.some_add_self_of_Y_ne {F : Type u} [field F] {W : weierstrass_curve F} {x₁ y₁ : F} {h₁ : W.nonsingular x₁ y₁} (hy : y₁ W.neg_Y x₁ y₁) :
theorem weierstrass_curve.point.some_add_self_of_Y_ne' {F : Type u} [field F] {W : weierstrass_curve F} {x₁ y₁ : F} {h₁ : W.nonsingular x₁ y₁} (hy : y₁ W.neg_Y x₁ y₁) :
@[simp]
theorem weierstrass_curve.point.some_add_some_of_X_ne {F : Type u} [field F] {W : weierstrass_curve F} {x₁ x₂ y₁ y₂ : F} {h₁ : W.nonsingular x₁ y₁} {h₂ : W.nonsingular x₂ y₂} (hx : x₁ x₂) :
theorem weierstrass_curve.point.some_add_some_of_X_ne' {F : Type u} [field F] {W : weierstrass_curve F} {x₁ x₂ y₁ y₂ : F} {h₁ : W.nonsingular x₁ y₁} {h₂ : W.nonsingular x₂ y₂} (hx : x₁ x₂) :

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

theorem weierstrass_curve.XY_ideal_neg_mul {F : Type u} [field F] {W : weierstrass_curve F} {x₁ y₁ : F} (h₁ : W.nonsingular x₁ y₁) :
theorem weierstrass_curve.XY_ideal_mul_XY_ideal {F : Type u} [field F] {W : weierstrass_curve F} {x₁ x₂ y₁ y₂ : F} (h₁' : W.equation x₁ y₁) (h₂' : W.equation x₂ y₂) (hxy : x₁ = x₂ y₁ W.neg_Y x₂ y₂) :
(W.add_X x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) * = (W.slope x₁ x₂ y₁ y₂)) * (W.add_X x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (polynomial.C (W.add_Y x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)))
@[simp]
noncomputable def weierstrass_curve.XY_ideal' {F : Type u} [field F] {W : weierstrass_curve F} {x₁ y₁ : F} (h₁ : W.nonsingular x₁ y₁) :

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

Equations
theorem weierstrass_curve.XY_ideal'_eq {F : Type u} [field F] {W : weierstrass_curve F} {x₁ y₁ : F} (h₁ : W.nonsingular x₁ y₁) :
theorem weierstrass_curve.mk_XY_ideal'_mul_mk_XY_ideal'_of_Y_eq {F : Type u} [field F] {W : weierstrass_curve F} {x₁ y₁ : F} (h₁ : W.nonsingular x₁ y₁) :
theorem weierstrass_curve.mk_XY_ideal'_mul_mk_XY_ideal' {F : Type u} [field F] {W : weierstrass_curve F} {x₁ x₂ y₁ y₂ : F} (h₁ : W.nonsingular x₁ y₁) (h₂ : W.nonsingular x₂ y₂) (hxy : x₁ = x₂ y₁ W.neg_Y x₂ y₂) :
@[simp]
noncomputable def weierstrass_curve.point.to_class_fun {F : Type u} [field F] {W : weierstrass_curve F} :

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]$.

Equations
noncomputable def weierstrass_curve.point.to_class {F : Type u} [field F] {W : weierstrass_curve F} :

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]$.

Equations
@[simp]
theorem weierstrass_curve.point.to_class_apply {F : Type u} [field F] {W : weierstrass_curve F} (ᾰ : W.point) :
theorem weierstrass_curve.point.to_class_some {F : Type u} [field F] {W : weierstrass_curve F} {x₁ y₁ : F} (h₁ : W.nonsingular x₁ y₁) :
@[simp]
theorem weierstrass_curve.point.add_eq_zero {F : Type u} [field F] {W : weierstrass_curve F} (P Q : W.point) :
P + Q = 0 P = -Q
@[simp]
theorem weierstrass_curve.point.add_left_neg {F : Type u} [field F] {W : weierstrass_curve F} (P : W.point) :
-P + P = 0
@[simp]
theorem weierstrass_curve.point.neg_add_eq_zero {F : Type u} [field F] {W : weierstrass_curve F} (P Q : W.point) :
-P + Q = 0 P = Q
theorem weierstrass_curve.point.add_comm {F : Type u} [field F] {W : weierstrass_curve F} (P Q : W.point) :
P + Q = Q + P
theorem weierstrass_curve.point.add_assoc {F : Type u} [field F] {W : weierstrass_curve F} (P Q R : W.point) :
P + Q + R = P + (Q + R)
@[protected, instance]
noncomputable def weierstrass_curve.point.add_comm_group {F : Type u} [field F] {W : weierstrass_curve F} :
Equations

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

def weierstrass_curve.point.of_base_change_fun {R : Type u} [comm_ring R] (W : weierstrass_curve R) (F : Type v) [field F] [ F] (K : Type w) [field K] [ K] [ K] [ K] :

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

Equations
def weierstrass_curve.point.of_base_change {R : Type u} [comm_ring R] (W : weierstrass_curve R) (F : Type v) [field F] [ F] (K : Type w) [field K] [ K] [ K] [ K] :

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

Equations
@[simp]
theorem weierstrass_curve.point.of_base_change_apply {R : Type u} [comm_ring R] (W : weierstrass_curve R) (F : Type v) [field F] [ F] (K : Type w) [field K] [ K] [ K] [ K] (ᾰ : (W.base_change F).point) :
theorem weierstrass_curve.point.of_base_change_injective {R : Type u} [comm_ring R] (W : weierstrass_curve R) (F : Type v) [field F] [ F] (K : Type w) [field K] [ K] [ K] [ K] :

### Rational points on an elliptic curve #

def elliptic_curve.point.mk {R : Type} [nontrivial R] [comm_ring R] (E : elliptic_curve R) {x y : R} (h : y) :

An affine point on an elliptic curve E over R.

Equations