mathlib3 documentation

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.

Main definitions #

Main statements #

Notations #

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 #

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] [algebra R A] (x₁ y₁ : R) :
(W.base_change A).neg_Y ((algebra_map R A) x₁) ((algebra_map R A) y₁) = (algebra_map R 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] [algebra R A] (B : Type w) [comm_ring B] [algebra R B] [algebra A B] [is_scalar_tower R A B] (x₁ y₁ : A) :
(W.base_change B).neg_Y ((algebra_map A B) x₁) ((algebra_map A B) y₁) = (algebra_map A B) ((W.base_change A).neg_Y x₁ y₁)
@[simp]
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
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.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] [algebra R A] (x₁ x₂ L : R) :
(W.base_change A).add_X ((algebra_map R A) x₁) ((algebra_map R A) x₂) ((algebra_map R A) L) = (algebra_map R 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] [algebra R A] (B : Type w) [comm_ring B] [algebra R B] [algebra A B] [is_scalar_tower R A B] (x₁ x₂ L : A) :
(W.base_change B).add_X ((algebra_map A B) x₁) ((algebra_map A B) x₂) ((algebra_map A B) L) = (algebra_map A 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] [algebra R A] (x₁ x₂ y₁ L : R) :
(W.base_change A).add_Y' ((algebra_map R A) x₁) ((algebra_map R A) x₂) ((algebra_map R A) y₁) ((algebra_map R A) L) = (algebra_map R 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] [algebra R A] (B : Type w) [comm_ring B] [algebra R B] [algebra A B] [is_scalar_tower R A B] (x₁ x₂ y₁ L : A) :
(W.base_change B).add_Y' ((algebra_map A B) x₁) ((algebra_map A B) x₂) ((algebra_map A B) y₁) ((algebra_map A B) L) = (algebra_map A 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] [algebra R A] (x₁ x₂ y₁ L : R) :
(W.base_change A).add_Y ((algebra_map R A) x₁) ((algebra_map R A) x₂) ((algebra_map R A) y₁) ((algebra_map R A) L) = (algebra_map R 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] [algebra R A] (B : Type w) [comm_ring B] [algebra R B] [algebra A B] [is_scalar_tower R A B] (x₁ x₂ y₁ L : A) :
(W.base_change B).add_Y ((algebra_map A B) x₁) ((algebra_map A B) x₂) ((algebra_map A B) y₁) ((algebra_map A B) L) = (algebra_map A B) ((W.base_change A).add_Y x₁ x₂ y₁ L)
theorem weierstrass_curve.equation_add_iff {R : Type u} [comm_ring R] (W : weierstrass_curve R) (x₁ x₂ y₁ L : R) :
W.equation (W.add_X x₁ x₂ L) (W.add_Y' x₁ x₂ y₁ L) polynomial.eval (W.add_X x₁ x₂ L) (W.add_polynomial x₁ y₁ L) = 0
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) :
W.nonsingular (W.add_X x₁ x₂ L) (W.add_Y' x₁ x₂ y₁ L)

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
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
@[simp]
theorem weierstrass_curve.point.neg_def {R : Type u} [comm_ring R] {W : weierstrass_curve R} (P : W.point) :
P.neg = -P
@[simp]

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₂) :
theorem weierstrass_curve.base_change_slope {F : Type u} [field F] {W : weierstrass_curve F} (K : Type v) [field K] [algebra F K] {x₁ x₂ y₁ y₂ : F} :
(W.base_change K).slope ((algebra_map F K) x₁) ((algebra_map F K) x₂) ((algebra_map F K) y₁) ((algebra_map F K) y₂) = (algebra_map F 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] [algebra R F] (K : Type w) [field K] [algebra R K] [algebra F K] [is_scalar_tower R F K] (x₁ x₂ y₁ y₂ : F) :
(W.base_change K).slope ((algebra_map F K) x₁) ((algebra_map F K) x₂) ((algebra_map F K) y₁) ((algebra_map F K) y₂) = (algebra_map F 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₂) :
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 x₁) * (polynomial.X - polynomial.C x₂) * (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₂) :
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 x₁) * (polynomial.X - polynomial.C x₂) + (polynomial.X - polynomial.C x₁) * (polynomial.X - polynomial.C (W.add_X x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) + (polynomial.X - polynomial.C x₂) * (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
@[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
@[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]
@[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_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₂) :
@[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.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]

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

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

Nonsingular rational points on a base changed Weierstrass curve #

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] [algebra R F] (K : Type w) [field K] [algebra R K] [algebra F K] [is_scalar_tower R F K] :

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

Equations

Rational points on an elliptic curve #

An affine point on an elliptic curve E over R.

Equations