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} [CommRing R] (W : WeierstrassCurve R) : Polynomial (Polynomial R)

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

def WeierstrassCurve.negY {R : Type u} [CommRing R] (W : WeierstrassCurve R) (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$.

theorem WeierstrassCurve.negY_negY {R : Type u} [CommRing R] (W : WeierstrassCurve R) (x₁ : R) (y₁ : R) : WeierstrassCurve.negY W x₁ (WeierstrassCurve.negY W x₁ y₁) = y₁

theorem WeierstrassCurve.baseChange_negY {R : Type u} [CommRing R] (W : WeierstrassCurve R) (A : Type v) [CommRing A] [Algebra R A] (x₁ : R) (y₁ : R) : WeierstrassCurve.negY (WeierstrassCurve.baseChange W A) (↑(algebraMap R A) x₁) (↑(algebraMap R A) y₁) = ↑(algebraMap R A) (WeierstrassCurve.negY W x₁ y₁)

theorem WeierstrassCurve.baseChange_negY_of_baseChange {R : Type u} [CommRing R] (W : WeierstrassCurve R) (A : Type v) [CommRing A] [Algebra R A] (B : Type w) [CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] (x₁ : A) (y₁ : A) : WeierstrassCurve.negY (WeierstrassCurve.baseChange W B) (↑(algebraMap A B) x₁) (↑(algebraMap A B) y₁) = ↑(algebraMap A B) (WeierstrassCurve.negY (WeierstrassCurve.baseChange W A) x₁ y₁)

theorem WeierstrassCurve.eval_negPolynomial {R : Type u} [CommRing R] (W : WeierstrassCurve R) (x₁ : R) (y₁ : R) : Polynomial.eval x₁ (Polynomial.eval (↑Polynomial.C y₁) (WeierstrassCurve.negPolynomial W)) = WeierstrassCurve.negY W x₁ y₁

noncomputable def WeierstrassCurve.linePolynomial {R : Type u} [CommRing R] (x₁ : R) (y₁ : R) (L : R) : Polynomial 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$.

theorem WeierstrassCurve.XYIdeal_eq₁ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (x₁ : R) (y₁ : R) (L : R) : WeierstrassCurve.CoordinateRing.XYIdeal W x₁ (↑Polynomial.C y₁) = WeierstrassCurve.CoordinateRing.XYIdeal W x₁ (WeierstrassCurve.linePolynomial x₁ y₁ L)

noncomputable def WeierstrassCurve.addPolynomial {R : Type u} [CommRing R] (W : WeierstrassCurve R) (x₁ : R) (y₁ : R) (L : R) : Polynomial 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$.

theorem WeierstrassCurve.C_addPolynomial {R : Type u} [CommRing R] (W : WeierstrassCurve R) (x₁ : R) (y₁ : R) (L : R) : ↑Polynomial.C (WeierstrassCurve.addPolynomial W x₁ y₁ L) = (Polynomial.X - ↑Polynomial.C (WeierstrassCurve.linePolynomial x₁ y₁ L)) * (WeierstrassCurve.negPolynomial W - ↑Polynomial.C (WeierstrassCurve.linePolynomial x₁ y₁ L)) + WeierstrassCurve.polynomial W

theorem WeierstrassCurve.CoordinateRing.C_addPolynomial {R : Type u} [CommRing R] (W : WeierstrassCurve R) (x₁ : R) (y₁ : R) (L : R) : ↑(WeierstrassCurve.CoordinateRing.mk W) (↑Polynomial.C (WeierstrassCurve.addPolynomial W x₁ y₁ L)) = ↑(WeierstrassCurve.CoordinateRing.mk W) ((Polynomial.X - ↑Polynomial.C (WeierstrassCurve.linePolynomial x₁ y₁ L)) * (WeierstrassCurve.negPolynomial W - ↑Polynomial.C (WeierstrassCurve.linePolynomial x₁ y₁ L)))

theorem WeierstrassCurve.addPolynomial_eq {R : Type u} [CommRing R] (W : WeierstrassCurve R) (x₁ : R) (y₁ : R) (L : R) : WeierstrassCurve.addPolynomial W x₁ y₁ L = -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} [CommRing R] (W : WeierstrassCurve R) (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$.

theorem WeierstrassCurve.baseChange_addX {R : Type u} [CommRing R] (W : WeierstrassCurve R) (A : Type v) [CommRing A] [Algebra R A] (x₁ : R) (x₂ : R) (L : R) : WeierstrassCurve.addX (WeierstrassCurve.baseChange W A) (↑(algebraMap R A) x₁) (↑(algebraMap R A) x₂) (↑(algebraMap R A) L) = ↑(algebraMap R A) (WeierstrassCurve.addX W x₁ x₂ L)

theorem WeierstrassCurve.baseChange_addX_of_baseChange {R : Type u} [CommRing R] (W : WeierstrassCurve R) (A : Type v) [CommRing A] [Algebra R A] (B : Type w) [CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] (x₁ : A) (x₂ : A) (L : A) : WeierstrassCurve.addX (WeierstrassCurve.baseChange W B) (↑(algebraMap A B) x₁) (↑(algebraMap A B) x₂) (↑(algebraMap A B) L) = ↑(algebraMap A B) (WeierstrassCurve.addX (WeierstrassCurve.baseChange W A) x₁ x₂ L)

def WeierstrassCurve.addY' {R : Type u} [CommRing R] (W : WeierstrassCurve R) (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$.

theorem WeierstrassCurve.baseChange_addY' {R : Type u} [CommRing R] (W : WeierstrassCurve R) (A : Type v) [CommRing A] [Algebra R A] (x₁ : R) (x₂ : R) (y₁ : R) (L : R) : WeierstrassCurve.addY' (WeierstrassCurve.baseChange W A) (↑(algebraMap R A) x₁) (↑(algebraMap R A) x₂) (↑(algebraMap R A) y₁) (↑(algebraMap R A) L) = ↑(algebraMap R A) (WeierstrassCurve.addY' W x₁ x₂ y₁ L)

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

def WeierstrassCurve.addY {R : Type u} [CommRing R] (W : WeierstrassCurve R) (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$.

theorem WeierstrassCurve.baseChange_addY {R : Type u} [CommRing R] (W : WeierstrassCurve R) (A : Type v) [CommRing A] [Algebra R A] (x₁ : R) (x₂ : R) (y₁ : R) (L : R) : WeierstrassCurve.addY (WeierstrassCurve.baseChange W A) (↑(algebraMap R A) x₁) (↑(algebraMap R A) x₂) (↑(algebraMap R A) y₁) (↑(algebraMap R A) L) = ↑(algebraMap R A) (WeierstrassCurve.addY W x₁ x₂ y₁ L)

theorem WeierstrassCurve.baseChange_addY_of_baseChange {R : Type u} [CommRing R] (W : WeierstrassCurve R) (A : Type v) [CommRing A] [Algebra R A] (B : Type w) [CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] (x₁ : A) (x₂ : A) (y₁ : A) (L : A) : WeierstrassCurve.addY (WeierstrassCurve.baseChange W B) (↑(algebraMap A B) x₁) (↑(algebraMap A B) x₂) (↑(algebraMap A B) y₁) (↑(algebraMap A B) L) = ↑(algebraMap A B) (WeierstrassCurve.addY (WeierstrassCurve.baseChange W A) x₁ x₂ y₁ L)

theorem WeierstrassCurve.XYIdeal_add_eq {R : Type u} [CommRing R] (W : WeierstrassCurve R) (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 {↑(WeierstrassCurve.CoordinateRing.mk W) (WeierstrassCurve.negPolynomial W - ↑Polynomial.C (WeierstrassCurve.linePolynomial x₁ y₁ L))} ⊔ WeierstrassCurve.CoordinateRing.XIdeal W (WeierstrassCurve.addX W x₁ x₂ L)

theorem WeierstrassCurve.equation_add_iff {R : Type u} [CommRing R] (W : WeierstrassCurve R) (x₁ : R) (x₂ : R) (y₁ : R) (L : R) : WeierstrassCurve.equation W (WeierstrassCurve.addX W x₁ x₂ L) (WeierstrassCurve.addY' W x₁ x₂ y₁ L) ↔ Polynomial.eval (WeierstrassCurve.addX W x₁ x₂ L) (WeierstrassCurve.addPolynomial W x₁ y₁ L) = 0

theorem WeierstrassCurve.nonsingular_add_of_eval_derivative_ne_zero {R : Type u} [CommRing R] (W : WeierstrassCurve R) (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 (WeierstrassCurve.addPolynomial W x₁ y₁ L)) ≠ 0) : WeierstrassCurve.nonsingular W (WeierstrassCurve.addX W x₁ x₂ L) (WeierstrassCurve.addY' W x₁ x₂ y₁ L)

The type of nonsingular rational points on a Weierstrass curve

inductive WeierstrassCurve.Point {R : Type u} [CommRing R] (W : WeierstrassCurve R) : Type u

• zero: {R : Type u} → [inst : CommRing R] → {W : WeierstrassCurve R} → WeierstrassCurve.Point W
• some: {R : Type u} → [inst : CommRing R] → {W : WeierstrassCurve R} → {x y : R} → WeierstrassCurve.nonsingular W x y → WeierstrassCurve.Point W

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.

def WeierstrassCurve.«term_⟮_⟯» : Lean.TrailingParserDescr

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

instance WeierstrassCurve.Point.instInhabitedPoint {R : Type u} [CommRing R] (W : WeierstrassCurve R) : Inhabited (WeierstrassCurve.Point W)

instance WeierstrassCurve.Point.instZeroPoint {R : Type u} [CommRing R] (W : WeierstrassCurve R) : Zero (WeierstrassCurve.Point W)

theorem WeierstrassCurve.Point.zero_def {R : Type u} [CommRing R] (W : WeierstrassCurve R) : WeierstrassCurve.Point.zero = 0

theorem WeierstrassCurve.equation_neg_iff {R : Type u} [CommRing R] {W : WeierstrassCurve R} {x₁ : R} {y₁ : R} : WeierstrassCurve.equation W x₁ (WeierstrassCurve.negY W x₁ y₁) ↔ WeierstrassCurve.equation W x₁ y₁

theorem WeierstrassCurve.equation_neg_of {R : Type u} [CommRing R] {W : WeierstrassCurve R} {x₁ : R} {y₁ : R} (h : WeierstrassCurve.equation W x₁ (WeierstrassCurve.negY W x₁ y₁)) : WeierstrassCurve.equation W x₁ y₁

theorem WeierstrassCurve.equation_neg {R : Type u} [CommRing R] {W : WeierstrassCurve R} {x₁ : R} {y₁ : R} (h : WeierstrassCurve.equation W x₁ y₁) : WeierstrassCurve.equation W x₁ (WeierstrassCurve.negY W x₁ y₁)

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

theorem WeierstrassCurve.nonsingular_neg_iff {R : Type u} [CommRing R] {W : WeierstrassCurve R} {x₁ : R} {y₁ : R} : WeierstrassCurve.nonsingular W x₁ (WeierstrassCurve.negY W x₁ y₁) ↔ WeierstrassCurve.nonsingular W x₁ y₁

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

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

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

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

The negation of a nonsingular rational point.

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

instance WeierstrassCurve.Point.instNegPoint {R : Type u} [CommRing R] {W : WeierstrassCurve R} : Neg (WeierstrassCurve.Point W)

theorem WeierstrassCurve.Point.neg_def {R : Type u} [CommRing R] {W : WeierstrassCurve R} (P : WeierstrassCurve.Point W) : WeierstrassCurve.Point.neg P = -P

@[simp]

theorem WeierstrassCurve.Point.neg_zero {R : Type u} [CommRing R] {W : WeierstrassCurve R} : -0 = 0

@[simp]

theorem WeierstrassCurve.Point.neg_some {R : Type u} [CommRing R] {W : WeierstrassCurve R} {x₁ : R} {y₁ : R} (h : WeierstrassCurve.nonsingular W x₁ y₁) : -WeierstrassCurve.Point.some h = WeierstrassCurve.Point.some (_ : WeierstrassCurve.nonsingular W x₁ (WeierstrassCurve.negY W x₁ y₁))

instance WeierstrassCurve.Point.instInvolutiveNegPoint {R : Type u} [CommRing R] {W : WeierstrassCurve R} : InvolutiveNeg (WeierstrassCurve.Point W)

Slopes of lines through nonsingular rational points on a Weierstrass curve

noncomputable def WeierstrassCurve.slope {F : Type u} [Field F] (W : WeierstrassCurve F) (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$.

@[simp]

theorem WeierstrassCurve.slope_of_Y_eq {F : Type u} [Field F] {W : WeierstrassCurve F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (hx : x₁ = x₂) (hy : y₁ = WeierstrassCurve.negY W x₂ y₂) : WeierstrassCurve.slope W x₁ x₂ y₁ y₂ = 0

@[simp]

theorem WeierstrassCurve.slope_of_Y_ne {F : Type u} [Field F] {W : WeierstrassCurve F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (hx : x₁ = x₂) (hy : y₁ ≠ WeierstrassCurve.negY W x₂ y₂) : WeierstrassCurve.slope W x₁ x₂ y₁ y₂ = (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - WeierstrassCurve.negY W x₁ y₁)

@[simp]

theorem WeierstrassCurve.slope_of_X_ne {F : Type u} [Field F] {W : WeierstrassCurve F} {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} [Field F] {W : WeierstrassCurve F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (hx : x₁ = x₂) (hy : y₁ ≠ WeierstrassCurve.negY W x₂ y₂) : WeierstrassCurve.slope W x₁ x₂ y₁ y₂ = -Polynomial.eval x₁ (Polynomial.eval (↑Polynomial.C y₁) (WeierstrassCurve.polynomialX W)) / Polynomial.eval x₁ (Polynomial.eval (↑Polynomial.C y₁) (WeierstrassCurve.polynomialY W))

theorem WeierstrassCurve.baseChange_slope {F : Type u} [Field F] {W : WeierstrassCurve F} (K : Type v) [Field K] [Algebra F K] {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} : WeierstrassCurve.slope (WeierstrassCurve.baseChange W K) (↑(algebraMap F K) x₁) (↑(algebraMap F K) x₂) (↑(algebraMap F K) y₁) (↑(algebraMap F K) y₂) = ↑(algebraMap F K) (WeierstrassCurve.slope W x₁ x₂ y₁ y₂)

theorem WeierstrassCurve.baseChange_slope_of_baseChange {R : Type u} [CommRing R] (W : WeierstrassCurve R) (F : Type v) [Field F] [Algebra R F] (K : Type w) [Field K] [Algebra R K] [Algebra F K] [IsScalarTower R F K] (x₁ : F) (x₂ : F) (y₁ : F) (y₂ : F) : WeierstrassCurve.slope (WeierstrassCurve.baseChange W K) (↑(algebraMap F K) x₁) (↑(algebraMap F K) x₂) (↑(algebraMap F K) y₁) (↑(algebraMap F K) y₂) = ↑(algebraMap F K) (WeierstrassCurve.slope (WeierstrassCurve.baseChange W F) x₁ x₂ y₁ y₂)

theorem WeierstrassCurve.Y_eq_of_X_eq {F : Type u} [Field F] {W : WeierstrassCurve F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁' : WeierstrassCurve.equation W x₁ y₁) (h₂' : WeierstrassCurve.equation W x₂ y₂) (hx : x₁ = x₂) : y₁ = y₂ ∨ y₁ = WeierstrassCurve.negY W x₂ y₂

theorem WeierstrassCurve.Y_eq_of_Y_ne {F : Type u} [Field F] {W : WeierstrassCurve F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁' : WeierstrassCurve.equation W x₁ y₁) (h₂' : WeierstrassCurve.equation W x₂ y₂) (hx : x₁ = x₂) (hy : y₁ ≠ WeierstrassCurve.negY W x₂ y₂) : y₁ = y₂

theorem WeierstrassCurve.XYIdeal_eq₂ {F : Type u} [Field F] {W : WeierstrassCurve F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁' : WeierstrassCurve.equation W x₁ y₁) (h₂' : WeierstrassCurve.equation W x₂ y₂) (hxy : x₁ = x₂ → y₁ ≠ WeierstrassCurve.negY W x₂ y₂) : WeierstrassCurve.CoordinateRing.XYIdeal W x₂ (↑Polynomial.C y₂) = WeierstrassCurve.CoordinateRing.XYIdeal W x₂ (WeierstrassCurve.linePolynomial x₁ y₁ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂))

theorem WeierstrassCurve.addPolynomial_slope {F : Type u} [Field F] {W : WeierstrassCurve F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁' : WeierstrassCurve.equation W x₁ y₁) (h₂' : WeierstrassCurve.equation W x₂ y₂) (hxy : x₁ = x₂ → y₁ ≠ WeierstrassCurve.negY W 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} [Field F] {W : WeierstrassCurve F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁' : WeierstrassCurve.equation W x₁ y₁) (h₂' : WeierstrassCurve.equation W x₂ y₂) (hxy : x₁ = x₂ → y₁ ≠ WeierstrassCurve.negY W x₂ y₂) : ↑(WeierstrassCurve.CoordinateRing.mk W) (↑Polynomial.C (WeierstrassCurve.addPolynomial W x₁ y₁ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂))) = -(WeierstrassCurve.CoordinateRing.XClass W x₁ * WeierstrassCurve.CoordinateRing.XClass W x₂ * WeierstrassCurve.CoordinateRing.XClass W (WeierstrassCurve.addX W x₁ x₂ (WeierstrassCurve.slope W x₁ x₂ y₁ y₂)))

theorem WeierstrassCurve.derivative_addPolynomial_slope {F : Type u} [Field F] {W : WeierstrassCurve F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁' : WeierstrassCurve.equation W x₁ y₁) (h₂' : WeierstrassCurve.equation W x₂ y₂) (hxy : x₁ = x₂ → y₁ ≠ WeierstrassCurve.negY W 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} [Field F] {W : WeierstrassCurve F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁' : WeierstrassCurve.equation W x₁ y₁) (h₂' : WeierstrassCurve.equation W x₂ y₂) (hxy : x₁ = x₂ → y₁ ≠ WeierstrassCurve.negY W 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} [Field F] {W : WeierstrassCurve F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁' : WeierstrassCurve.equation W x₁ y₁) (h₂' : WeierstrassCurve.equation W x₂ y₂) (hxy : x₁ = x₂ → y₁ ≠ WeierstrassCurve.negY W 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} [Field F] {W : WeierstrassCurve F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁ : WeierstrassCurve.nonsingular W x₁ y₁) (h₂ : WeierstrassCurve.nonsingular W x₂ y₂) (hxy : x₁ = x₂ → y₁ ≠ WeierstrassCurve.negY W 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} [Field F] {W : WeierstrassCurve F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁ : WeierstrassCurve.nonsingular W x₁ y₁) (h₂ : WeierstrassCurve.nonsingular W x₂ y₂) (hxy : x₁ = x₂ → y₁ ≠ WeierstrassCurve.negY W 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} [Field F] {W : WeierstrassCurve F} : WeierstrassCurve.Point W → WeierstrassCurve.Point W → WeierstrassCurve.Point W

The addition of two nonsingular rational points.

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

noncomputable instance WeierstrassCurve.Point.instAddPoint {F : Type u} [Field F] {W : WeierstrassCurve F} : Add (WeierstrassCurve.Point W)

theorem WeierstrassCurve.Point.add_def {F : Type u} [Field F] {W : WeierstrassCurve F} (P : WeierstrassCurve.Point W) (Q : WeierstrassCurve.Point W) : WeierstrassCurve.Point.add P Q = P + Q

noncomputable instance WeierstrassCurve.Point.instAddZeroClassPoint {F : Type u} [Field F] {W : WeierstrassCurve F} : AddZeroClass (WeierstrassCurve.Point W)

@[simp]

theorem WeierstrassCurve.Point.some_add_some_of_Y_eq {F : Type u} [Field F] {W : WeierstrassCurve F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} {h₁ : WeierstrassCurve.nonsingular W x₁ y₁} {h₂ : WeierstrassCurve.nonsingular W x₂ y₂} (hx : x₁ = x₂) (hy : y₁ = WeierstrassCurve.negY W x₂ y₂) : WeierstrassCurve.Point.some h₁ + WeierstrassCurve.Point.some h₂ = 0

@[simp]

theorem WeierstrassCurve.Point.some_add_self_of_Y_eq {F : Type u} [Field F] {W : WeierstrassCurve F} {x₁ : F} {y₁ : F} {h₁ : WeierstrassCurve.nonsingular W x₁ y₁} (hy : y₁ = WeierstrassCurve.negY W x₁ y₁) : WeierstrassCurve.Point.some h₁ + WeierstrassCurve.Point.some h₁ = 0

@[simp]

theorem WeierstrassCurve.Point.some_add_some_of_Y_ne {F : Type u} [Field F] {W : WeierstrassCurve F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} {h₁ : WeierstrassCurve.nonsingular W x₁ y₁} {h₂ : WeierstrassCurve.nonsingular W x₂ y₂} (hx : x₁ = x₂) (hy : y₁ ≠ WeierstrassCurve.negY W x₂ y₂) : WeierstrassCurve.Point.some h₁ + WeierstrassCurve.Point.some h₂ = 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} [Field F] {W : WeierstrassCurve F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} {h₁ : WeierstrassCurve.nonsingular W x₁ y₁} {h₂ : WeierstrassCurve.nonsingular W x₂ y₂} (hx : x₁ = x₂) (hy : y₁ ≠ WeierstrassCurve.negY W x₂ y₂) : WeierstrassCurve.Point.some h₁ + WeierstrassCurve.Point.some h₂ = -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} [Field F] {W : WeierstrassCurve F} {x₁ : F} {y₁ : F} {h₁ : WeierstrassCurve.nonsingular W x₁ y₁} (hy : y₁ ≠ WeierstrassCurve.negY W x₁ y₁) : WeierstrassCurve.Point.some h₁ + WeierstrassCurve.Point.some h₁ = 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} [Field F] {W : WeierstrassCurve F} {x₁ : F} {y₁ : F} {h₁ : WeierstrassCurve.nonsingular W x₁ y₁} (hy : y₁ ≠ WeierstrassCurve.negY W x₁ y₁) : WeierstrassCurve.Point.some h₁ + WeierstrassCurve.Point.some h₁ = -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} [Field F] {W : WeierstrassCurve F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} {h₁ : WeierstrassCurve.nonsingular W x₁ y₁} {h₂ : WeierstrassCurve.nonsingular W x₂ y₂} (hx : x₁ ≠ x₂) : WeierstrassCurve.Point.some h₁ + WeierstrassCurve.Point.some h₂ = 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} [Field F] {W : WeierstrassCurve F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} {h₁ : WeierstrassCurve.nonsingular W x₁ y₁} {h₂ : WeierstrassCurve.nonsingular W x₂ y₂} (hx : x₁ ≠ x₂) : WeierstrassCurve.Point.some h₁ + WeierstrassCurve.Point.some h₂ = -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} [Field F] {W : WeierstrassCurve F} {x₁ : F} {y₁ : F} (h₁ : WeierstrassCurve.nonsingular W x₁ y₁) : WeierstrassCurve.CoordinateRing.XYIdeal W x₁ (↑Polynomial.C (WeierstrassCurve.negY W x₁ y₁)) * WeierstrassCurve.CoordinateRing.XYIdeal W x₁ (↑Polynomial.C y₁) = WeierstrassCurve.CoordinateRing.XIdeal W x₁

theorem WeierstrassCurve.XYIdeal_mul_XYIdeal {F : Type u} [Field F] {W : WeierstrassCurve F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁' : WeierstrassCurve.equation W x₁ y₁) (h₂' : WeierstrassCurve.equation W x₂ y₂) (hxy : x₁ = x₂ → y₁ ≠ WeierstrassCurve.negY W 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} [Field F] {W : WeierstrassCurve F} {x₁ : F} {y₁ : F} (h₁ : WeierstrassCurve.nonsingular W x₁ y₁) : (FractionalIdeal (nonZeroDivisors (WeierstrassCurve.CoordinateRing W)) (WeierstrassCurve.FunctionField W))ˣ

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

theorem WeierstrassCurve.XYIdeal'_eq {F : Type u} [Field F] {W : WeierstrassCurve F} {x₁ : F} {y₁ : F} (h₁ : WeierstrassCurve.nonsingular W x₁ y₁) : ↑(WeierstrassCurve.XYIdeal' h₁) = ↑(WeierstrassCurve.CoordinateRing.XYIdeal W x₁ (↑Polynomial.C y₁))

theorem WeierstrassCurve.mk_XYIdeal'_mul_mk_XYIdeal'_of_Y_eq {F : Type u} [Field F] {W : WeierstrassCurve F} {x₁ : F} {y₁ : F} (h₁ : WeierstrassCurve.nonsingular W x₁ y₁) : ↑ClassGroup.mk (WeierstrassCurve.XYIdeal' (_ : WeierstrassCurve.nonsingular W x₁ (WeierstrassCurve.negY W x₁ y₁))) * ↑ClassGroup.mk (WeierstrassCurve.XYIdeal' h₁) = 1

theorem WeierstrassCurve.mk_XYIdeal'_mul_mk_XYIdeal' {F : Type u} [Field F] {W : WeierstrassCurve F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁ : WeierstrassCurve.nonsingular W x₁ y₁) (h₂ : WeierstrassCurve.nonsingular W x₂ y₂) (hxy : x₁ = x₂ → y₁ ≠ WeierstrassCurve.negY W x₂ y₂) : ↑ClassGroup.mk (WeierstrassCurve.XYIdeal' h₁) * ↑ClassGroup.mk (WeierstrassCurve.XYIdeal' h₂) = ↑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} [Field F] {W : WeierstrassCurve F} : WeierstrassCurve.Point W → Additive (ClassGroup (WeierstrassCurve.CoordinateRing 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]$.

@[simp]

theorem WeierstrassCurve.Point.toClass_apply {F : Type u} [Field F] {W : WeierstrassCurve F} : ∀ (a : WeierstrassCurve.Point W), ↑WeierstrassCurve.Point.toClass a = WeierstrassCurve.Point.toClassFun a

noncomputable def WeierstrassCurve.Point.toClass {F : Type u} [Field F] {W : WeierstrassCurve F} : WeierstrassCurve.Point W →+ Additive (ClassGroup (WeierstrassCurve.CoordinateRing 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]$.

theorem WeierstrassCurve.Point.toClass_zero {F : Type u} [Field F] {W : WeierstrassCurve F} : ↑WeierstrassCurve.Point.toClass 0 = 0

theorem WeierstrassCurve.Point.toClass_some {F : Type u} [Field F] {W : WeierstrassCurve F} {x₁ : F} {y₁ : F} (h₁ : WeierstrassCurve.nonsingular W x₁ y₁) : ↑WeierstrassCurve.Point.toClass (WeierstrassCurve.Point.some h₁) = ↑ClassGroup.mk (WeierstrassCurve.XYIdeal' h₁)

theorem WeierstrassCurve.Point.add_eq_zero {F : Type u} [Field F] {W : WeierstrassCurve F} (P : WeierstrassCurve.Point W) (Q : WeierstrassCurve.Point W) : P + Q = 0 ↔ P = -Q

theorem WeierstrassCurve.Point.add_left_neg {F : Type u} [Field F] {W : WeierstrassCurve F} (P : WeierstrassCurve.Point W) : -P + P = 0

theorem WeierstrassCurve.Point.neg_add_eq_zero {F : Type u} [Field F] {W : WeierstrassCurve F} (P : WeierstrassCurve.Point W) (Q : WeierstrassCurve.Point W) : -P + Q = 0 ↔ P = Q

theorem WeierstrassCurve.Point.toClass_eq_zero {F : Type u} [Field F] {W : WeierstrassCurve F} (P : WeierstrassCurve.Point W) : ↑WeierstrassCurve.Point.toClass P = 0 ↔ P = 0

theorem WeierstrassCurve.Point.toClass_injective {F : Type u} [Field F] {W : WeierstrassCurve F} : Function.Injective ↑WeierstrassCurve.Point.toClass

theorem WeierstrassCurve.Point.add_comm {F : Type u} [Field F] {W : WeierstrassCurve F} (P : WeierstrassCurve.Point W) (Q : WeierstrassCurve.Point W) : P + Q = Q + P

theorem WeierstrassCurve.Point.add_assoc {F : Type u} [Field F] {W : WeierstrassCurve F} (P : WeierstrassCurve.Point W) (Q : WeierstrassCurve.Point W) (R : WeierstrassCurve.Point W) : P + Q + R = P + (Q + R)

noncomputable instance WeierstrassCurve.Point.instAddCommGroupPoint {F : Type u} [Field F] {W : WeierstrassCurve F} : AddCommGroup (WeierstrassCurve.Point W)

Nonsingular rational points on a base changed Weierstrass curve

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

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

@[simp]

theorem WeierstrassCurve.Point.ofBaseChange_apply {R : Type u} [CommRing R] (W : WeierstrassCurve R) (F : Type v) [Field F] [Algebra R F] (K : Type w) [Field K] [Algebra R K] [Algebra F K] [IsScalarTower R F K] : ∀ (a : WeierstrassCurve.Point (WeierstrassCurve.baseChange W F)), ↑(WeierstrassCurve.Point.ofBaseChange W F K) a = WeierstrassCurve.Point.ofBaseChangeFun W F K a

def WeierstrassCurve.Point.ofBaseChange {R : Type u} [CommRing R] (W : WeierstrassCurve R) (F : Type v) [Field F] [Algebra R F] (K : Type w) [Field K] [Algebra R K] [Algebra F K] [IsScalarTower R F K] : WeierstrassCurve.Point (WeierstrassCurve.baseChange W F) →+ WeierstrassCurve.Point (WeierstrassCurve.baseChange W K)

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

theorem WeierstrassCurve.Point.ofBaseChange_injective {R : Type u} [CommRing R] (W : WeierstrassCurve R) (F : Type v) [Field F] [Algebra R F] (K : Type w) [Field K] [Algebra R K] [Algebra F K] [IsScalarTower R F K] : Function.Injective ↑(WeierstrassCurve.Point.ofBaseChange W F K)

Rational points on an elliptic curve

def EllipticCurve.Point.mk {R : Type} [Nontrivial R] [CommRing R] (E : EllipticCurve R) {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.