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-Pis defined to be the unique third point of intersection betweenWand the line through0andP. Explicitly, ifPis $(x, y)$, then-Pis $(x, -y - a_1x - a_3)$. - Given two points
PandQ, their additionP + Qis defined to be the negation of the unique third point of intersection betweenWand the lineLthroughPandQ. Explicitly, letPbe $(x_1, y_1)$ and letQbe $(x_2, y_2)$.- If $x_1 = x_2$ and $y_1 = -y_2 - a_1x_2 - a_3$, then
Lis vertical andP + Qis0. - If $x_1 = x_2$ and $y_1 \ne -y_2 - a_1x_2 - a_3$, then
Lis the tangent ofWatP = 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
Lis the secant ofWthroughPandQ, and has slope $\ell := (y_1 - y_2) / (x_1 - x_2)$. In the latter two cases, the $X$-coordinate ofP + Qis 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 ofP + 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.
- If $x_1 = x_2$ and $y_1 = -y_2 - a_1x_2 - a_3$, then
Main definitions #
weierstrass_curve.point: the type of nonsingular rational points on a Weierstrass curveW.weierstrass_curve.point.add: the addition of two nonsingular rational points onW.
Main statements #
weierstrass_curve.point.add_comm_group: the type of nonsingular rational points onWforms an abelian group under addition.
Notations #
W⟮K⟯: the group of nonsingular rational points onWbase changed toK.
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) :
polynomial (polynomial R)
The polynomial $-Y - a_1X - a_3$ associated to negation.
Equations
theorem
weierstrass_curve.neg_Y_neg_Y
{R : Type u}
[comm_ring R]
(W : weierstrass_curve R)
(x₁ y₁ : R) :
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]
theorem
weierstrass_curve.eval_neg_polynomial
{R : Type u}
[comm_ring R]
(W : weierstrass_curve R)
(x₁ y₁ : R) :
polynomial.eval x₁ (polynomial.eval (⇑polynomial.C y₁) W.neg_polynomial) = W.neg_Y x₁ y₁
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
- weierstrass_curve.line_polynomial x₁ y₁ L = ⇑polynomial.C L * (polynomial.X - ⇑polynomial.C x₁) + ⇑polynomial.C y₁
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
- W.add_polynomial x₁ y₁ L = polynomial.eval (weierstrass_curve.line_polynomial x₁ y₁ L) W.polynomial
theorem
weierstrass_curve.C_add_polynomial
{R : Type u}
[comm_ring R]
(W : weierstrass_curve R)
(x₁ y₁ L : R) :
⇑polynomial.C (W.add_polynomial x₁ y₁ L) = (polynomial.X - ⇑polynomial.C (weierstrass_curve.line_polynomial x₁ y₁ L)) * (W.neg_polynomial - ⇑polynomial.C (weierstrass_curve.line_polynomial x₁ y₁ L)) + W.polynomial
theorem
weierstrass_curve.coordinate_ring.C_add_polynomial
{R : Type u}
[comm_ring R]
(W : weierstrass_curve R)
(x₁ y₁ L : R) :
⇑(adjoin_root.mk W.polynomial) (⇑polynomial.C (W.add_polynomial x₁ y₁ L)) = ⇑(adjoin_root.mk W.polynomial) ((polynomial.X - ⇑polynomial.C (weierstrass_curve.line_polynomial x₁ y₁ L)) * (W.neg_polynomial - ⇑polynomial.C (weierstrass_curve.line_polynomial x₁ y₁ L)))
theorem
weierstrass_curve.add_polynomial_eq
{R : Type u}
[comm_ring R]
(W : weierstrass_curve R)
(x₁ y₁ L : R) :
@[simp]
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$.
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$.
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$.
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.XY_ideal_add_eq
{R : Type u}
[comm_ring R]
(W : weierstrass_curve R)
(x₁ x₂ y₁ L : R) :
weierstrass_curve.coordinate_ring.XY_ideal W (W.add_X x₁ x₂ L) (⇑polynomial.C (W.add_Y x₁ x₂ y₁ L)) = ideal.span {⇑(adjoin_root.mk W.polynomial) (W.neg_polynomial - ⇑polynomial.C (weierstrass_curve.line_polynomial x₁ y₁ L))} ⊔ weierstrass_curve.coordinate_ring.X_ideal W (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) :
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 #
- zero : Π {R : Type u} [_inst_1 : comm_ring R] {W : weierstrass_curve R}, W.point
- some : Π {R : Type u} [_inst_1 : comm_ring R] {W : weierstrass_curve R} {x y : R}, W.nonsingular x y → W.point
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
@[simp]
theorem
weierstrass_curve.equation_neg_iff
{R : Type u}
[comm_ring R]
{W : weierstrass_curve R}
{x₁ y₁ : R} :
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₁) :
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) :
@[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]
def
weierstrass_curve.point.has_involutive_neg
{R : Type u}
[comm_ring R]
{W : weierstrass_curve R} :
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$.
@[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₂) :
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₂ = -polynomial.eval x₁ (polynomial.eval (⇑polynomial.C y₁) W.polynomial_X) / polynomial.eval x₁ (polynomial.eval (⇑polynomial.C y₁) W.polynomial_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.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₂) :
weierstrass_curve.coordinate_ring.XY_ideal W x₂ (⇑polynomial.C y₂) = weierstrass_curve.coordinate_ring.XY_ideal W x₂ (weierstrass_curve.line_polynomial 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 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₂) :
⇑(adjoin_root.mk W.polynomial) (⇑polynomial.C (W.add_polynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) = -(weierstrass_curve.coordinate_ring.X_class W x₁ * weierstrass_curve.coordinate_ring.X_class W x₂ * weierstrass_curve.coordinate_ring.X_class W (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 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₂) :
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₂) :
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.
The addition of two nonsingular rational points.
Given two nonsingular rational points P and Q, use P + Q instead of add P Q.
Equations
- (weierstrass_curve.point.some h₁).add (weierstrass_curve.point.some h₂) = 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₂), weierstrass_curve.point.some _)) (λ (hx : ¬x₁ = x₂), weierstrass_curve.point.some _)
- (weierstrass_curve.point.some h).add 0 = weierstrass_curve.point.some h
- 0.add (weierstrass_curve.point.some h) = weierstrass_curve.point.some h
- 0.add weierstrass_curve.point.zero = weierstrass_curve.point.zero
@[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) :
@[protected, instance]
noncomputable
def
weierstrass_curve.point.add_zero_class
{F : Type u}
[field F]
{W : weierstrass_curve F} :
Equations
- weierstrass_curve.point.add_zero_class = {zero := 0, add := has_add.add weierstrass_curve.point.has_add, zero_add := _, add_zero := _}
@[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₂) :
weierstrass_curve.coordinate_ring.X_ideal W (W.add_X x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) * (weierstrass_curve.coordinate_ring.XY_ideal W x₁ (⇑polynomial.C y₁) * weierstrass_curve.coordinate_ring.XY_ideal W x₂ (⇑polynomial.C y₂)) = weierstrass_curve.coordinate_ring.Y_ideal W (weierstrass_curve.line_polynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) * weierstrass_curve.coordinate_ring.XY_ideal W (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
- weierstrass_curve.XY_ideal' h₁ = units.mk_of_mul_eq_one ↑(weierstrass_curve.coordinate_ring.XY_ideal W x₁ (⇑polynomial.C y₁)) (↑(weierstrass_curve.coordinate_ring.XY_ideal W x₁ (⇑polynomial.C (W.neg_Y x₁ y₁))) * (↑(weierstrass_curve.coordinate_ring.X_ideal W x₁))⁻¹) _
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} :
W.point → additive (class_group W.coordinate_ring)
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) :
@[simp]
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_left_neg
{F : Type u}
[field F]
{W : weierstrass_curve F}
(P : W.point) :
theorem
weierstrass_curve.point.to_class_eq_zero
{F : Type u}
[field F]
{W : weierstrass_curve F}
(P : W.point) :
⇑weierstrass_curve.point.to_class P = 0 ↔ P = 0
theorem
weierstrass_curve.point.to_class_injective
{F : Type u}
[field F]
{W : weierstrass_curve F} :
theorem
weierstrass_curve.point.add_comm
{F : Type u}
[field F]
{W : weierstrass_curve F}
(P Q : W.point) :
@[protected, instance]
noncomputable
def
weierstrass_curve.point.add_comm_group
{F : Type u}
[field F]
{W : weierstrass_curve F} :
Equations
- weierstrass_curve.point.add_comm_group = {add := weierstrass_curve.point.add W, add_assoc := _, zero := weierstrass_curve.point.zero W, zero_add := _, add_zero := _, nsmul := add_group.nsmul._default weierstrass_curve.point.zero weierstrass_curve.point.add weierstrass_curve.point.add_comm_group._proof_3 weierstrass_curve.point.add_comm_group._proof_4, nsmul_zero' := _, nsmul_succ' := _, neg := weierstrass_curve.point.neg W, sub := add_group.sub._default weierstrass_curve.point.add weierstrass_curve.point.add_assoc weierstrass_curve.point.zero weierstrass_curve.point.add_comm_group._proof_7 weierstrass_curve.point.add_comm_group._proof_8 (add_group.nsmul._default weierstrass_curve.point.zero weierstrass_curve.point.add weierstrass_curve.point.add_comm_group._proof_3 weierstrass_curve.point.add_comm_group._proof_4) weierstrass_curve.point.add_comm_group._proof_9 weierstrass_curve.point.add_comm_group._proof_10 weierstrass_curve.point.neg, sub_eq_add_neg := _, zsmul := add_group.zsmul._default weierstrass_curve.point.add weierstrass_curve.point.add_assoc weierstrass_curve.point.zero weierstrass_curve.point.add_comm_group._proof_12 weierstrass_curve.point.add_comm_group._proof_13 (add_group.nsmul._default weierstrass_curve.point.zero weierstrass_curve.point.add weierstrass_curve.point.add_comm_group._proof_3 weierstrass_curve.point.add_comm_group._proof_4) weierstrass_curve.point.add_comm_group._proof_14 weierstrass_curve.point.add_comm_group._proof_15 weierstrass_curve.point.neg, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
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]
[algebra R F]
(K : Type w)
[field K]
[algebra R K]
[algebra F K]
[is_scalar_tower R F K] :
(W.base_change F).point → (W.base_change K).point
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] :
(W.base_change F).point →+ (W.base_change K).point
The group homomorphism from W⟮F⟯ to W⟮K⟯ induced by a base change from F to K.
Equations
- weierstrass_curve.point.of_base_change W F K = {to_fun := weierstrass_curve.point.of_base_change_fun W F K _inst_7, map_zero' := _, map_add' := _}
@[simp]
theorem
weierstrass_curve.point.of_base_change_apply
{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]
(ᾰ : (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]
[algebra R F]
(K : Type w)
[field K]
[algebra R K]
[algebra F K]
[is_scalar_tower R F 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 : E.to_weierstrass_curve.equation x y) :
An affine point on an elliptic curve E over R.