Affine coordinates for Weierstrass curves

This file defines the type of points on a Weierstrass curve as an inductive, consisting of the point at infinity and affine points satisfying a Weierstrass equation with a nonsingular condition. This file also defines the negation and addition operations of the group law for this type, and proves that they respect the Weierstrass equation and the nonsingular condition. The fact that they form an abelian group is proven in Mathlib.AlgebraicGeometry.EllipticCurve.Group.

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.Affine.equation: the Weierstrass equation of an affine Weierstrass curve.
• WeierstrassCurve.Affine.nonsingular: the nonsingular condition on an affine Weierstrass curve.
• WeierstrassCurve.Affine.Point: a nonsingular rational point on an affine Weierstrass curve.
• WeierstrassCurve.Affine.Point.neg: the negation operation on an affine Weierstrass curve.
• WeierstrassCurve.Affine.Point.add: the addition operation on an affine Weierstrass curve.

Main statements

• WeierstrassCurve.Affine.equation_neg: negation preserves the Weierstrass equation.
• WeierstrassCurve.Affine.equation_add: addition preserves the Weierstrass equation.
• WeierstrassCurve.Affine.nonsingular_neg: negation preserves the nonsingular condition.
• WeierstrassCurve.Affine.nonsingular_add: addition preserves the nonsingular condition.
• WeierstrassCurve.Affine.nonsingular_of_Δ_ne_zero: an affine Weierstrass curve is nonsingular at every point if its discriminant is non-zero.
• EllipticCurve.Affine.nonsingular: an affine elliptic curve is nonsingular at every point.

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, affine coordinates

def PolynomialPolynomial.termY : Lean.ParserDescr

The notation Y for X in the PolynomialPolynomial scope.

Equations

• PolynomialPolynomial.termY = Lean.ParserDescr.node `PolynomialPolynomial.termY 1024 (Lean.ParserDescr.symbol "Y")

def PolynomialPolynomial.«term_[X][Y]» : Lean.TrailingParserDescr

The notation R[X][Y] for R[X][X] in the PolynomialPolynomial scope.

Equations

• PolynomialPolynomial.«term_[X][Y]» = Lean.ParserDescr.trailingNode `PolynomialPolynomial.term_[X][Y] 1022 0 (Lean.ParserDescr.symbol "[X][Y]")

Weierstrass curves

@[inline, reducible]

abbrev WeierstrassCurve.Affine (R : Type u) : Type u

An abbreviation for a Weierstrass curve in affine coordinates.

Equations

• WeierstrassCurve.Affine R = WeierstrassCurve R

@[inline, reducible]

abbrev WeierstrassCurve.toAffine {R : Type u} (W : WeierstrassCurve R) : WeierstrassCurve.Affine R

The coercion to a Weierstrass curve in affine coordinates.

Equations

• W.toAffine = W

Weierstrass equations

noncomputable def WeierstrassCurve.Affine.polynomial {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) : Polynomial (Polynomial R)

The polynomial $W(X, Y) := Y^2 + a_1XY + a_3Y - (X^3 + a_2X^2 + a_4X + a_6)$ associated to a Weierstrass curve W over R. For ease of polynomial manipulation, this is represented as a term of type R[X][X], where the inner variable represents $X$ and the outer variable represents $Y$. For clarity, the alternative notations Y and R[X][Y] are provided in the PolynomialPolynomial scope to represent the outer variable and the bivariate polynomial ring R[X][X] respectively.

Equations

• One or more equations did not get rendered due to their size.

theorem WeierstrassCurve.Affine.polynomial_eq {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) : W.polynomial = Cubic.toPoly { a := 0, b := 1, c := Cubic.toPoly { a := 0, b := 0, c := W.a₁, d := W.a₃ }, d := Cubic.toPoly { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ } }

theorem WeierstrassCurve.Affine.polynomial_ne_zero {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) [Nontrivial R] : W.polynomial ≠ 0

@[simp]

theorem WeierstrassCurve.Affine.degree_polynomial {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) [Nontrivial R] : Polynomial.degree W.polynomial = 2

@[simp]

theorem WeierstrassCurve.Affine.natDegree_polynomial {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) [Nontrivial R] : Polynomial.natDegree W.polynomial = 2

theorem WeierstrassCurve.Affine.monic_polynomial {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) : Polynomial.Monic W.polynomial

theorem WeierstrassCurve.Affine.irreducible_polynomial {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) [IsDomain R] : Irreducible W.polynomial

theorem WeierstrassCurve.Affine.eval_polynomial {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) : Polynomial.eval x (Polynomial.eval (Polynomial.C y) W.polynomial) = y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆)

@[simp]

theorem WeierstrassCurve.Affine.eval_polynomial_zero {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) : Polynomial.eval 0 (Polynomial.eval 0 W.polynomial) = -W.a₆

def WeierstrassCurve.Affine.equation {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) : Prop

The proposition that an affine point $(x, y)$ lies in W. In other words, $W(x, y) = 0$.

Equations

• W.equation x y = (Polynomial.eval x (Polynomial.eval (Polynomial.C y) W.polynomial) = 0)

theorem WeierstrassCurve.Affine.equation_iff' {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) : W.equation x y ↔ y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆) = 0

theorem WeierstrassCurve.Affine.equation_iff {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) : W.equation x y ↔ y ^ 2 + W.a₁ * x * y + W.a₃ * y = x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆

@[simp]

theorem WeierstrassCurve.Affine.equation_zero {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) : W.equation 0 0 ↔ W.a₆ = 0

theorem WeierstrassCurve.Affine.equation_iff_variableChange {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) : W.equation x y ↔ (W.variableChange { u := 1, r := x, s := 0, t := y }).toAffine.equation 0 0

Nonsingular Weierstrass equations

noncomputable def WeierstrassCurve.Affine.polynomialX {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) : Polynomial (Polynomial R)

The partial derivative $W_X(X, Y)$ of $W(X, Y)$ with respect to $X$.

TODO: define this in terms of Polynomial.derivative.

Equations

• W.polynomialX = Polynomial.C (Polynomial.C W.a₁) * Polynomial.X - Polynomial.C (Polynomial.C 3 * Polynomial.X ^ 2 + Polynomial.C (2 * W.a₂) * Polynomial.X + Polynomial.C W.a₄)

theorem WeierstrassCurve.Affine.eval_polynomialX {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) : Polynomial.eval x (Polynomial.eval (Polynomial.C y) W.polynomialX) = W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)

@[simp]

theorem WeierstrassCurve.Affine.eval_polynomialX_zero {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) : Polynomial.eval 0 (Polynomial.eval 0 W.polynomialX) = -W.a₄

noncomputable def WeierstrassCurve.Affine.polynomialY {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) : Polynomial (Polynomial R)

The partial derivative $W_Y(X, Y)$ of $W(X, Y)$ with respect to $Y$.

TODO: define this in terms of Polynomial.derivative.

Equations

• W.polynomialY = Polynomial.C (Polynomial.C 2) * Polynomial.X + Polynomial.C (Polynomial.C W.a₁ * Polynomial.X + Polynomial.C W.a₃)

theorem WeierstrassCurve.Affine.eval_polynomialY {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) : Polynomial.eval x (Polynomial.eval (Polynomial.C y) W.polynomialY) = 2 * y + W.a₁ * x + W.a₃

@[simp]

theorem WeierstrassCurve.Affine.eval_polynomialY_zero {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) : Polynomial.eval 0 (Polynomial.eval 0 W.polynomialY) = W.a₃

def WeierstrassCurve.Affine.nonsingular {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) : Prop

The proposition that an affine point $(x, y)$ in W is nonsingular. In other words, either $W_X(x, y) \ne 0$ or $W_Y(x, y) \ne 0$.

Equations

• W.nonsingular x y = (W.equation x y ∧ (Polynomial.eval x (Polynomial.eval (Polynomial.C y) W.polynomialX) ≠ 0 ∨ Polynomial.eval x (Polynomial.eval (Polynomial.C y) W.polynomialY) ≠ 0))

theorem WeierstrassCurve.Affine.nonsingular_iff' {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) : W.nonsingular x y ↔ W.equation x y ∧ (W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0)

theorem WeierstrassCurve.Affine.nonsingular_iff {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) : W.nonsingular x y ↔ W.equation x y ∧ (W.a₁ * y ≠ 3 * x ^ 2 + 2 * W.a₂ * x + W.a₄ ∨ y ≠ -y - W.a₁ * x - W.a₃)

@[simp]

theorem WeierstrassCurve.Affine.nonsingular_zero {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) : W.nonsingular 0 0 ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)

theorem WeierstrassCurve.Affine.nonsingular_iff_variableChange {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) : W.nonsingular x y ↔ (W.variableChange { u := 1, r := x, s := 0, t := y }).toAffine.nonsingular 0 0

theorem WeierstrassCurve.Affine.nonsingular_zero_of_Δ_ne_zero {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (h : W.equation 0 0) (hΔ : W.Δ ≠ 0) : W.nonsingular 0 0

theorem WeierstrassCurve.Affine.nonsingular_of_Δ_ne_zero {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) {x : R} {y : R} (h : W.equation x y) (hΔ : W.Δ ≠ 0) : W.nonsingular x y

A Weierstrass curve is nonsingular at every point if its discriminant is non-zero.

Group operation polynomials over a ring

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

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

Equations

• W.negPolynomial = -Polynomial.X - Polynomial.C (Polynomial.C W.a₁ * Polynomial.X + Polynomial.C W.a₃)

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

Equations

• W.negY x y = -y - W.a₁ * x - W.a₃

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

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

noncomputable def WeierstrassCurve.Affine.linePolynomial {R : Type u} [CommRing R] (x : R) (y : R) (L : R) : Polynomial R

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

This does not depend on W, and has argument order: $x$, $y$, $L$.

Equations

• x.linePolynomial y L = Polynomial.C L * (Polynomial.X - Polynomial.C x) + Polynomial.C y

noncomputable def WeierstrassCurve.Affine.addPolynomial {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) (L : R) : Polynomial R

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

This depends on W, and has argument order: $x$, $y$, $L$.

Equations

• W.addPolynomial x y L = Polynomial.eval (x.linePolynomial y L) W.polynomial

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

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

Equations

• W.addX x₁ x₂ L = L ^ 2 + W.a₁ * L - W.a₂ - x₁ - x₂

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

Equations

• W.addY' x₁ x₂ y₁ L = L * (W.addX x₁ x₂ L - x₁) + y₁

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

Equations

• W.addY x₁ x₂ y₁ L = W.negY (W.addX x₁ x₂ L) (W.addY' x₁ x₂ y₁ L)

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

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

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

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

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

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

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

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

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

theorem WeierstrassCurve.Affine.nonsingular_add_of_eval_derivative_ne_zero {R : Type u} [CommRing R] {W : WeierstrassCurve.Affine R} {x₁ : R} {x₂ : R} {y₁ : R} {L : R} (hx' : W.equation (W.addX x₁ x₂ L) (W.addY' x₁ x₂ y₁ L)) (hx : Polynomial.eval (W.addX x₁ x₂ L) (Polynomial.derivative (W.addPolynomial x₁ y₁ L)) ≠ 0) : W.nonsingular (W.addX x₁ x₂ L) (W.addY' x₁ x₂ y₁ L)

Group operation polynomials over a field

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

Equations

• W.slope x₁ x₂ y₁ y₂ = if x₁ = x₂ then if y₁ = W.negY x₂ y₂ then 0 else (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁) else (y₁ - y₂) / (x₁ - x₂)

@[simp]

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

@[simp]

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

@[simp]

theorem WeierstrassCurve.Affine.slope_of_Xne {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (hx : x₁ ≠ x₂) : W.slope x₁ x₂ y₁ y₂ = (y₁ - y₂) / (x₁ - x₂)

theorem WeierstrassCurve.Affine.slope_of_Yne_eq_eval {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (hx : x₁ = x₂) (hy : y₁ ≠ W.negY x₂ y₂) : W.slope x₁ x₂ y₁ y₂ = -Polynomial.eval x₁ (Polynomial.eval (Polynomial.C y₁) W.polynomialX) / Polynomial.eval x₁ (Polynomial.eval (Polynomial.C y₁) W.polynomialY)

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

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

theorem WeierstrassCurve.Affine.addPolynomial_slope {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁ : W.equation x₁ y₁) (h₂ : W.equation x₂ y₂) (hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂) : W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂) = -((Polynomial.X - Polynomial.C x₁) * (Polynomial.X - Polynomial.C x₂) * (Polynomial.X - Polynomial.C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))

theorem WeierstrassCurve.Affine.equation_add' {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁ : W.equation x₁ y₁) (h₂ : W.equation x₂ y₂) (hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂) : W.equation (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY' 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 WeierstrassCurve.Affine.equation_add {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁ : W.equation x₁ y₁) (h₂ : W.equation x₂ y₂) (hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂) : W.equation (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY 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 WeierstrassCurve.Affine.derivative_addPolynomial_slope {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁ : W.equation x₁ y₁) (h₂ : W.equation x₂ y₂) (hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂) : Polynomial.derivative (W.addPolynomial 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.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) + (Polynomial.X - Polynomial.C x₂) * (Polynomial.X - Polynomial.C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))

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

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

Group operations

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

A nonsingular rational point on a Weierstrass curve W in affine coordinates. This is either the unique point at infinity WeierstrassCurve.Affine.Point.zero or the nonsingular affine points WeierstrassCurve.Affine.Point.some $(x, y)$ satisfying the Weierstrass equation of W.

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

def WeierstrassCurve.«term_⟮_⟯».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• WeierstrassCurve.Affine.Point.instInhabitedPoint = { default := WeierstrassCurve.Affine.Point.zero }

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

Equations

• WeierstrassCurve.Affine.Point.instZeroPoint = { zero := WeierstrassCurve.Affine.Point.zero }

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

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

The negation of a nonsingular rational point on W.

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

Equations

• x.neg = match x with | WeierstrassCurve.Affine.Point.zero => 0 | WeierstrassCurve.Affine.Point.some h => WeierstrassCurve.Affine.Point.some ⋯

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

Equations

• WeierstrassCurve.Affine.Point.instNegPoint = { neg := WeierstrassCurve.Affine.Point.neg }

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

@[simp]

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

@[simp]

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

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

Equations

• WeierstrassCurve.Affine.Point.instInvolutiveNegPoint = InvolutiveNeg.mk ⋯

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

The addition of two nonsingular rational points on W.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• WeierstrassCurve.Affine.Point.instAddPoint = { add := WeierstrassCurve.Affine.Point.add }

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

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

Equations

• WeierstrassCurve.Affine.Point.instAddZeroClassPoint = AddZeroClass.mk ⋯ ⋯

@[simp]

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

@[simp]

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

@[simp]

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

theorem WeierstrassCurve.Affine.Point.some_add_some_of_Yne' {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} {h₁ : W.nonsingular x₁ y₁} {h₂ : W.nonsingular x₂ y₂} (hx : x₁ = x₂) (hy : y₁ ≠ W.negY x₂ y₂) : WeierstrassCurve.Affine.Point.some h₁ + WeierstrassCurve.Affine.Point.some h₂ = -WeierstrassCurve.Affine.Point.some ⋯

@[simp]

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

theorem WeierstrassCurve.Affine.Point.some_add_self_of_Yne' {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {y₁ : F} {h₁ : W.nonsingular x₁ y₁} (hy : y₁ ≠ W.negY x₁ y₁) : WeierstrassCurve.Affine.Point.some h₁ + WeierstrassCurve.Affine.Point.some h₁ = -WeierstrassCurve.Affine.Point.some ⋯

@[simp]

theorem WeierstrassCurve.Affine.Point.some_add_some_of_Xne {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} {h₁ : W.nonsingular x₁ y₁} {h₂ : W.nonsingular x₂ y₂} (hx : x₁ ≠ x₂) : WeierstrassCurve.Affine.Point.some h₁ + WeierstrassCurve.Affine.Point.some h₂ = WeierstrassCurve.Affine.Point.some ⋯

theorem WeierstrassCurve.Affine.Point.some_add_some_of_Xne' {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} {h₁ : W.nonsingular x₁ y₁} {h₂ : W.nonsingular x₂ y₂} (hx : x₁ ≠ x₂) : WeierstrassCurve.Affine.Point.some h₁ + WeierstrassCurve.Affine.Point.some h₂ = -WeierstrassCurve.Affine.Point.some ⋯

Maps and base changes

theorem WeierstrassCurve.Affine.map_equation {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) {A : Type v} [CommRing A] {φ : R →+* A} (hφ : Function.Injective ⇑φ) (x : R) (y : R) : (W.map φ).toAffine.equation (φ x) (φ y) ↔ W.equation x y

theorem WeierstrassCurve.Affine.map_nonsingular {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) {A : Type v} [CommRing A] {φ : R →+* A} (hφ : Function.Injective ⇑φ) (x : R) (y : R) : (W.map φ).toAffine.nonsingular (φ x) (φ y) ↔ W.nonsingular x y

theorem WeierstrassCurve.Affine.map_negY {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) {A : Type v} [CommRing A] (φ : R →+* A) (x : R) (y : R) : (W.map φ).toAffine.negY (φ x) (φ y) = φ (W.negY x y)

theorem WeierstrassCurve.Affine.map_addX {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) {A : Type v} [CommRing A] (φ : R →+* A) (x₁ : R) (x₂ : R) (L : R) : (W.map φ).toAffine.addX (φ x₁) (φ x₂) (φ L) = φ (W.addX x₁ x₂ L)

theorem WeierstrassCurve.Affine.map_addY' {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) {A : Type v} [CommRing A] (φ : R →+* A) (x₁ : R) (x₂ : R) (y₁ : R) (L : R) : (W.map φ).toAffine.addY' (φ x₁) (φ x₂) (φ y₁) (φ L) = φ (W.addY' x₁ x₂ y₁ L)

theorem WeierstrassCurve.Affine.map_addY {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) {A : Type v} [CommRing A] (φ : R →+* A) (x₁ : R) (x₂ : R) (y₁ : R) (L : R) : (W.map φ).toAffine.addY (φ x₁) (φ x₂) (φ y₁) (φ L) = φ (W.toAffine.addY x₁ x₂ y₁ L)

theorem WeierstrassCurve.Affine.map_slope {F : Type u} [Field F] (W : WeierstrassCurve.Affine F) {K : Type v} [Field K] (φ : F →+* K) (x₁ : F) (x₂ : F) (y₁ : F) (y₂ : F) : (W.map φ).toAffine.slope (φ x₁) (φ x₂) (φ y₁) (φ y₂) = φ (W.slope x₁ x₂ y₁ y₂)

theorem WeierstrassCurve.Affine.baseChange_equation {R : Type r} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] {ψ : A →ₐ[S] B} (hψ : Function.Injective ⇑ψ) (x : A) (y : A) : (W.baseChange B).toAffine.equation (ψ x) (ψ y) ↔ (W.baseChange A).toAffine.equation x y

theorem WeierstrassCurve.Affine.baseChange_nonsingular {R : Type r} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] {ψ : A →ₐ[S] B} (hψ : Function.Injective ⇑ψ) (x : A) (y : A) : (W.baseChange B).toAffine.nonsingular (ψ x) (ψ y) ↔ (W.baseChange A).toAffine.nonsingular x y

theorem WeierstrassCurve.Affine.baseChange_negY {R : Type r} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (ψ : A →ₐ[S] B) (x : A) (y : A) : (W.baseChange B).toAffine.negY (ψ x) (ψ y) = ψ ((W.baseChange A).toAffine.negY x y)

theorem WeierstrassCurve.Affine.baseChange_addX {R : Type r} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (ψ : A →ₐ[S] B) (x₁ : A) (x₂ : A) (L : A) : (W.baseChange B).toAffine.addX (ψ x₁) (ψ x₂) (ψ L) = ψ ((W.baseChange A).toAffine.addX x₁ x₂ L)

theorem WeierstrassCurve.Affine.baseChange_addY' {R : Type r} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (ψ : A →ₐ[S] B) (x₁ : A) (x₂ : A) (y₁ : A) (L : A) : (W.baseChange B).toAffine.addY' (ψ x₁) (ψ x₂) (ψ y₁) (ψ L) = ψ ((W.baseChange A).toAffine.addY' x₁ x₂ y₁ L)

theorem WeierstrassCurve.Affine.baseChange_addY {R : Type r} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (ψ : A →ₐ[S] B) (x₁ : A) (x₂ : A) (y₁ : A) (L : A) : (W.baseChange B).toAffine.addY (ψ x₁) (ψ x₂) (ψ y₁) (ψ L) = ψ ((W.baseChange A).toAffine.addY x₁ x₂ y₁ L)

theorem WeierstrassCurve.Affine.baseChange_slope {R : Type r} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [CommRing S] [Algebra R S] {F : Type u} [Field F] [Algebra R F] [Algebra S F] [IsScalarTower R S F] {K : Type v} [Field K] [Algebra R K] [Algebra S K] [IsScalarTower R S K] (ψ : F →ₐ[S] K) (x₁ : F) (x₂ : F) (y₁ : F) (y₂ : F) : (W.baseChange K).toAffine.slope (ψ x₁) (ψ x₂) (ψ y₁) (ψ y₂) = ψ ((W.baseChange F).toAffine.slope x₁ x₂ y₁ y₂)

def WeierstrassCurve.Affine.Point.mapFun {R : Type r} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [CommRing S] [Algebra R S] {F : Type u} [Field F] [Algebra R F] [Algebra S F] [IsScalarTower R S F] {K : Type v} [Field K] [Algebra R K] [Algebra S K] [IsScalarTower R S K] (ψ : F →ₐ[S] K) : (W.baseChange F).Point → (W.baseChange K).Point

The function from W⟮F⟯ to W⟮K⟯ induced by an algebra homomorphism ψ : F →ₐ[S] K, where W is defined over a subring of a ring S, and F and K are field extensions of S.

Equations

• WeierstrassCurve.Affine.Point.mapFun W ψ x = match x with | WeierstrassCurve.Affine.Point.zero => 0 | WeierstrassCurve.Affine.Point.some h => WeierstrassCurve.Affine.Point.some ⋯

def WeierstrassCurve.Affine.Point.map {R : Type r} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [CommRing S] [Algebra R S] {F : Type u} [Field F] [Algebra R F] [Algebra S F] [IsScalarTower R S F] {K : Type v} [Field K] [Algebra R K] [Algebra S K] [IsScalarTower R S K] (ψ : F →ₐ[S] K) : (W.baseChange F).Point →+ (W.baseChange K).Point

The group homomorphism from W⟮F⟯ to W⟮K⟯ induced by an algebra homomorphism ψ : F →ₐ[S] K, where W is defined over a subring of a ring S, and F and K are field extensions of S.

Equations

• WeierstrassCurve.Affine.Point.map W ψ = { toZeroHom := { toFun := WeierstrassCurve.Affine.Point.mapFun W ψ, map_zero' := ⋯ }, map_add' := ⋯ }

theorem WeierstrassCurve.Affine.Point.map_zero {R : Type r} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [CommRing S] [Algebra R S] {F : Type u} [Field F] [Algebra R F] [Algebra S F] [IsScalarTower R S F] {K : Type v} [Field K] [Algebra R K] [Algebra S K] [IsScalarTower R S K] (ψ : F →ₐ[S] K) : (WeierstrassCurve.Affine.Point.map W ψ) 0 = 0

theorem WeierstrassCurve.Affine.Point.map_some {R : Type r} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [CommRing S] [Algebra R S] {F : Type u} [Field F] [Algebra R F] [Algebra S F] [IsScalarTower R S F] {K : Type v} [Field K] [Algebra R K] [Algebra S K] [IsScalarTower R S K] (ψ : F →ₐ[S] K) {x : F} {y : F} (h : (W.baseChange F).toAffine.nonsingular x y) : (WeierstrassCurve.Affine.Point.map W ψ) (WeierstrassCurve.Affine.Point.some h) = WeierstrassCurve.Affine.Point.some ⋯

theorem WeierstrassCurve.Affine.Point.map_id {R : Type r} [CommRing R] (W : WeierstrassCurve.Affine R) {F : Type u} [Field F] [Algebra R F] (P : (W.baseChange F).Point) : (WeierstrassCurve.Affine.Point.map W (Algebra.ofId F F)) P = P

theorem WeierstrassCurve.Affine.Point.map_map {R : Type r} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [CommRing S] [Algebra R S] {F : Type u} [Field F] [Algebra R F] [Algebra S F] [IsScalarTower R S F] {K : Type v} [Field K] [Algebra R K] [Algebra S K] [IsScalarTower R S K] (ψ : F →ₐ[S] K) {L : Type w} [Field L] [Algebra R L] [Algebra S L] [IsScalarTower R S L] (χ : K →ₐ[S] L) (P : (W.baseChange F).Point) : (WeierstrassCurve.Affine.Point.map W χ) ((WeierstrassCurve.Affine.Point.map W ψ) P) = (WeierstrassCurve.Affine.Point.map W (AlgHom.comp χ ψ)) P

theorem WeierstrassCurve.Affine.Point.map_injective {R : Type r} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [CommRing S] [Algebra R S] {F : Type u} [Field F] [Algebra R F] [Algebra S F] [IsScalarTower R S F] {K : Type v} [Field K] [Algebra R K] [Algebra S K] [IsScalarTower R S K] (ψ : F →ₐ[S] K) : Function.Injective ⇑(WeierstrassCurve.Affine.Point.map W ψ)

@[inline, reducible]

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

The group homomorphism from W⟮F⟯ to W⟮K⟯ induced by the base change from F to K, where W is defined over a subring of a ring S, and F and K are field extensions of S.

Equations

• WeierstrassCurve.Affine.Point.baseChange W F K = WeierstrassCurve.Affine.Point.map W (Algebra.ofId F K)

theorem WeierstrassCurve.Affine.Point.map_baseChange {R : Type r} [CommRing R] (W : WeierstrassCurve.Affine R) {F : Type u} [Field F] [Algebra R F] {K : Type v} [Field K] [Algebra R K] {L : Type w} [Field L] [Algebra R L] [Algebra F K] [IsScalarTower R F K] [Algebra F L] [IsScalarTower R F L] (χ : K →ₐ[F] L) (P : (W.baseChange F).Point) : (WeierstrassCurve.Affine.Point.map W χ) ((WeierstrassCurve.Affine.Point.baseChange W F K) P) = (WeierstrassCurve.Affine.Point.baseChange W F L) P

Elliptic curves

@[inline, reducible]

abbrev EllipticCurve.toAffine {R : Type u} [CommRing R] (E : EllipticCurve R) : WeierstrassCurve.Affine R

The coercion from an elliptic curve to a Weierstrass curve in affine coordinates.

Equations

• E.toAffine = E.toAffine

theorem EllipticCurve.Affine.nonsingular {R : Type u} [CommRing R] (E : EllipticCurve R) [Nontrivial R] {x : R} {y : R} (h : E.toAffine.equation x y) : E.toAffine.nonsingular x y