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.lean.

Mathematical background

Let W be a Weierstrass curve over a field F with coefficients aᵢ. An affine point on W is a tuple (x, y) of elements in R satisfying the Weierstrass equation W(X, Y) = 0 in affine coordinates, where W(X, Y) := Y² + a₁XY + a₃Y - (X³ + a₂X² + a₄X + a₆). It is nonsingular if its partial derivatives W_X(x, y) and W_Y(x, y) do not vanish simultaneously.

The nonsingular affine points on W can be given negation and addition operations defined by a secant-and-tangent process.

• Given a nonsingular affine point P, its negation -P is defined to be the unique third nonsingular point of intersection between W and the vertical line through P. Explicitly, if P is (x, y), then -P is (x, -y - a₁x - a₃).

• Given two nonsingular affine points P and Q, their addition P + Q is defined to be the negation of the unique third nonsingular point of intersection between W and the line L through P and Q. Explicitly, let P be (x₁, y₁) and let Q be (x₂, y₂).

  • If x₁ = x₂ and y₁ = -y₂ - a₁x₂ - a₃, then L is vertical.
  • If x₁ = x₂ and y₁ ≠ -y₂ - a₁x₂ - a₃, then L is the tangent of W at P = Q, and has slope ℓ := (3x₁² + 2a₂x₁ + a₄ - a₁y₁) / (2y₁ + a₁x₁ + a₃).
  • Otherwise x₁ ≠ x₂, then L is the secant of W through P and Q, and has slope ℓ := (y₁ - y₂) / (x₁ - x₂).

  In the last two cases, the X-coordinate of P + Q is then the unique third solution of the equation obtained by substituting the line Y = ℓ(X - x₁) + y₁ into the Weierstrass equation, and can be written down explicitly as x := ℓ² + a₁ℓ - a₂ - x₁ - x₂ by inspecting the coefficients of X². The Y-coordinate of P + Q, after applying the final negation that maps Y to -Y - a₁X - a₃, is precisely y := -(ℓ(x - x₁) + y₁) - a₁x - a₃.

The type of nonsingular points W⟮F⟯ in affine coordinates is an inductive, consisting of the unique point at infinity 𝓞 and nonsingular affine points (x, y). Then W⟮F⟯ can be endowed with a group law, with 𝓞 as the identity nonsingular point, which is uniquely determined by these formulae.

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.
• WeierstrassCurve.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

Weierstrass curves

@[reducible, inline]

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

An abbreviation for a Weierstrass curve in affine coordinates.

Equations

• WeierstrassCurve.Affine R = WeierstrassCurve R

@[reducible, inline]

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

The conversion from a Weierstrass curve to affine coordinates.

Equations

• W.toAffine = W

Weierstrass equations

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

The polynomial W(X, Y) := Y² + a₁XY + a₃Y - (X³ + a₂X² + a₄X + a₆) associated to a Weierstrass curve W over a ring R in affine coordinates.

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 Polynomial.Bivariate 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 r} [CommRing R] {W' : Affine R} : W'.polynomial = { a := 0, b := 1, c := { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly, d := { a := -1, b := -W'.a₂, c := -W'.a₄, d := -W'.a₆ }.toPoly }.toPoly

theorem WeierstrassCurve.Affine.polynomial_ne_zero {R : Type r} [CommRing R] {W' : Affine R} [Nontrivial R] : W'.polynomial ≠ 0

@[simp]

theorem WeierstrassCurve.Affine.degree_polynomial {R : Type r} [CommRing R] {W' : Affine R} [Nontrivial R] : W'.polynomial.degree = 2

@[simp]

theorem WeierstrassCurve.Affine.natDegree_polynomial {R : Type r} [CommRing R] {W' : Affine R} [Nontrivial R] : W'.polynomial.natDegree = 2

theorem WeierstrassCurve.Affine.monic_polynomial {R : Type r} [CommRing R] {W' : Affine R} : W'.polynomial.Monic

theorem WeierstrassCurve.Affine.irreducible_polynomial {R : Type r} [CommRing R] {W' : Affine R} [IsDomain R] : Irreducible W'.polynomial

theorem WeierstrassCurve.Affine.evalEval_polynomial {R : Type r} [CommRing R] {W' : Affine R} (x y : R) : Polynomial.evalEval x 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.evalEval_polynomial_zero {R : Type r} [CommRing R] {W' : Affine R} : Polynomial.evalEval 0 0 W'.polynomial = -W'.a₆

def WeierstrassCurve.Affine.Equation {R : Type r} [CommRing R] (W' : Affine R) (x y : R) : Prop

The proposition that an affine point (x, y) lies in a Weierstrass curve W.

In other words, it satisfies the Weierstrass equation W(X, Y) = 0.

Equations

• W'.Equation x y = (Polynomial.evalEval x y W'.polynomial = 0)

theorem WeierstrassCurve.Affine.equation_iff' {R : Type r} [CommRing R] {W' : Affine R} (x 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 r} [CommRing R] {W' : Affine R} (x 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 r} [CommRing R] {W' : Affine R} : W'.Equation 0 0 ↔ W'.a₆ = 0

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

Nonsingular Weierstrass equations

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

The partial derivative W_X(X, Y) with respect to X of the polynomial W(X, Y) associated to a Weierstrass curve W in affine coordinates.

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.evalEval_polynomialX {R : Type r} [CommRing R] {W' : Affine R} (x y : R) : Polynomial.evalEval x y W'.polynomialX = W'.a₁ * y - (3 * x ^ 2 + 2 * W'.a₂ * x + W'.a₄)

@[simp]

theorem WeierstrassCurve.Affine.evalEval_polynomialX_zero {R : Type r} [CommRing R] {W' : Affine R} : Polynomial.evalEval 0 0 W'.polynomialX = -W'.a₄

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

The partial derivative W_Y(X, Y) with respect to Y of the polynomial W(X, Y) associated to a Weierstrass curve W in affine coordinates.

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.evalEval_polynomialY {R : Type r} [CommRing R] {W' : Affine R} (x y : R) : Polynomial.evalEval x y W'.polynomialY = 2 * y + W'.a₁ * x + W'.a₃

@[simp]

theorem WeierstrassCurve.Affine.evalEval_polynomialY_zero {R : Type r} [CommRing R] {W' : Affine R} : Polynomial.evalEval 0 0 W'.polynomialY = W'.a₃

def WeierstrassCurve.Affine.Nonsingular {R : Type r} [CommRing R] (W' : Affine R) (x y : R) : Prop

The proposition that an affine point (x, y) on a Weierstrass curve W is nonsingular.

In other words, either W_X(x, y) ≠ 0 or W_Y(x, y) ≠ 0.

Note that this definition is only mathematically accurate for fields.

Equations

• W'.Nonsingular x y = (W'.Equation x y ∧ (Polynomial.evalEval x y W'.polynomialX ≠ 0 ∨ Polynomial.evalEval x y W'.polynomialY ≠ 0))

theorem WeierstrassCurve.Affine.nonsingular_iff' {R : Type r} [CommRing R] {W' : Affine R} (x 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 r} [CommRing R] {W' : Affine R} (x 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 r} [CommRing R] {W' : Affine R} : W'.Nonsingular 0 0 ↔ W'.a₆ = 0 ∧ (W'.a₃ ≠ 0 ∨ W'.a₄ ≠ 0)

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

theorem WeierstrassCurve.Affine.nonsingular_zero_of_Δ_ne_zero {R : Type r} [CommRing R] {W' : Affine R} (h : W'.Equation 0 0) (hΔ : Δ W' ≠ 0) : W'.Nonsingular 0 0

theorem WeierstrassCurve.Affine.nonsingular_of_Δ_ne_zero {R : Type r} [CommRing R] {W' : Affine R} {x 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 r} [CommRing R] (W' : Affine R) : Polynomial (Polynomial R)

The negation polynomial -Y - a₁X - a₃ associated to the negation of a nonsingular affine point on a Weierstrass curve.

Equations

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

theorem WeierstrassCurve.Affine.Y_sub_polynomialY {R : Type r} [CommRing R] {W' : Affine R} : Polynomial.X - W'.polynomialY = W'.negPolynomial

theorem WeierstrassCurve.Affine.Y_sub_negPolynomial {R : Type r} [CommRing R] {W' : Affine R} : Polynomial.X - W'.negPolynomial = W'.polynomialY

def WeierstrassCurve.Affine.negY {R : Type r} [CommRing R] (W' : Affine R) (x y : R) : R

The Y-coordinate of -(x, y) for a nonsingular affine point (x, y) on a Weierstrass curve 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 r} [CommRing R] {W' : Affine R} (x y : R) : W'.negY x (W'.negY x y) = y

theorem WeierstrassCurve.Affine.eval_negPolynomial {R : Type r} [CommRing R] {W' : Affine R} (x y : R) : Polynomial.evalEval x y W'.negPolynomial = W'.negY x y

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

The line polynomial ℓ(X - x) + y associated to the line Y = ℓ(X - x) + y that passes through a nonsingular affine point (x, y) on a Weierstrass curve W with a slope of ℓ.

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

Equations

• WeierstrassCurve.Affine.linePolynomial x y ℓ = Polynomial.C ℓ * (Polynomial.X - Polynomial.C x) + Polynomial.C y

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

The addition polynomial obtained by substituting the line Y = ℓ(X - x) + y into the polynomial W(X, Y) associated to a Weierstrass curve W. If such a line intersects W at another nonsingular affine point (x', y') on W, 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, ℓ.

Equations

• W'.addPolynomial x y ℓ = Polynomial.eval (WeierstrassCurve.Affine.linePolynomial x y ℓ) W'.polynomial

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

theorem WeierstrassCurve.Affine.addPolynomial_eq {R : Type r} [CommRing R] {W' : Affine R} (x y ℓ : R) : W'.addPolynomial x y ℓ = -{ a := 1, b := -ℓ ^ 2 - W'.a₁ * ℓ + W'.a₂, c := 2 * x * ℓ ^ 2 + (W'.a₁ * x - 2 * y - W'.a₃) * ℓ + (-W'.a₁ * y + W'.a₄), d := -x ^ 2 * ℓ ^ 2 + (2 * x * y + W'.a₃ * x) * ℓ - (y ^ 2 + W'.a₃ * y - W'.a₆) }.toPoly

def WeierstrassCurve.Affine.addX {R : Type r} [CommRing R] (W' : Affine R) (x₁ x₂ ℓ : R) : R

The X-coordinate of (x₁, y₁) + (x₂, y₂) for two nonsingular affine points (x₁, y₁) and (x₂, y₂) on a Weierstrass curve W, where the line through them has a slope of ℓ.

This depends on W, and has argument order: x₁, x₂, ℓ.

Equations

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

def WeierstrassCurve.Affine.negAddY {R : Type r} [CommRing R] (W' : Affine R) (x₁ x₂ y₁ ℓ : R) : R

The Y-coordinate of -((x₁, y₁) + (x₂, y₂)) for two nonsingular affine points (x₁, y₁) and (x₂, y₂) on a Weierstrass curve W, where the line through them has a slope of ℓ.

This depends on W, and has argument order: x₁, x₂, y₁, ℓ.

Equations

• W'.negAddY x₁ x₂ y₁ ℓ = ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁

def WeierstrassCurve.Affine.addY {R : Type r} [CommRing R] (W' : Affine R) (x₁ x₂ y₁ ℓ : R) : R

The Y-coordinate of (x₁, y₁) + (x₂, y₂) for two nonsingular affine points (x₁, y₁) and (x₂, y₂) on a Weierstrass curve W, where the line through them has a slope of ℓ.

This depends on W, and has argument order: x₁, x₂, y₁, ℓ.

Equations

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

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

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

theorem WeierstrassCurve.Affine.equation_add_iff {R : Type r} [CommRing R] {W' : Affine R} (x₁ x₂ y₁ ℓ : R) : W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ) ↔ Polynomial.eval (W'.addX x₁ x₂ ℓ) (W'.addPolynomial x₁ y₁ ℓ) = 0

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

theorem WeierstrassCurve.Affine.equation_neg {R : Type r} [CommRing R] {W' : Affine R} {x 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 r} [CommRing R] {W' : Affine R} {x y : R} (h : W'.Nonsingular x (W'.negY x y)) : W'.Nonsingular x y

theorem WeierstrassCurve.Affine.nonsingular_neg {R : Type r} [CommRing R] {W' : Affine R} {x 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_negAdd_of_eval_derivative_ne_zero {R : Type r} [CommRing R] {W' : Affine R} {x₁ x₂ y₁ ℓ : R} (hx' : W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)) (hx : Polynomial.eval (W'.addX x₁ x₂ ℓ) (Polynomial.derivative (W'.addPolynomial x₁ y₁ ℓ)) ≠ 0) : W'.Nonsingular (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)

Group operation polynomials over a field

noncomputable def WeierstrassCurve.Affine.slope {F : Type u} [Field F] (W : Affine F) (x₁ x₂ y₁ y₂ : F) : F

The slope of the line through two nonsingular affine points (x₁, y₁) and (x₂, y₂) on a Weierstrass curve W.

If x₁ ≠ x₂, then this line is the secant of W through (x₁, y₁) and (x₂, y₂), and has slope (y₁ - y₂) / (x₁ - x₂). Otherwise, if y₁ ≠ -y₁ - a₁x₁ - a₃, then this line is the tangent of W at (x₁, y₁) = (x₂, y₂), and has slope (3x₁² + 2a₂x₁ + a₄ - a₁y₁) / (2y₁ + a₁x₁ + a₃). Otherwise, this line is vertical, in which case this returns the value 0.

This depends on W, and has argument order: x₁, x₂, y₁, y₂.

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_Y_eq {F : Type u} [Field F] {W : Affine F} {x₁ x₂ y₁ y₂ : F} (hx : x₁ = x₂) (hy : y₁ = W.negY x₂ y₂) : W.slope x₁ x₂ y₁ y₂ = 0

@[simp]

theorem WeierstrassCurve.Affine.slope_of_Y_ne {F : Type u} [Field F] {W : Affine F} {x₁ x₂ y₁ 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_X_ne {F : Type u} [Field F] {W : Affine F} {x₁ x₂ y₁ y₂ : F} (hx : x₁ ≠ x₂) : W.slope x₁ x₂ y₁ y₂ = (y₁ - y₂) / (x₁ - x₂)

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

theorem WeierstrassCurve.Affine.Y_eq_of_X_eq {F : Type u} [Field F] {W : Affine F} {x₁ x₂ y₁ 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.Y_eq_of_Y_ne {F : Type u} [Field F] {W : Affine F} {x₁ x₂ y₁ 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 : Affine F} {x₁ x₂ y₁ 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_negAdd {F : Type u} [Field F] {W : Affine F} {x₁ x₂ y₁ 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.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))

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

theorem WeierstrassCurve.Affine.equation_add {F : Type u} [Field F] {W : Affine F} {x₁ x₂ y₁ 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.C_addPolynomial_slope {F : Type u} [Field F] {W : Affine F} {x₁ x₂ y₁ y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂) (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) : Polynomial.C (W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) = -(Polynomial.C (Polynomial.X - Polynomial.C x₁) * Polynomial.C (Polynomial.X - Polynomial.C x₂) * Polynomial.C (Polynomial.X - Polynomial.C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))

theorem WeierstrassCurve.Affine.derivative_addPolynomial_slope {F : Type u} [Field F] {W : Affine F} {x₁ x₂ y₁ 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_negAdd {F : Type u} [Field F] {W : Affine F} {x₁ x₂ y₁ 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.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))

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

theorem WeierstrassCurve.Affine.nonsingular_add {F : Type u} [Field F] {W : Affine F} {x₁ x₂ y₁ 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.

theorem WeierstrassCurve.Affine.addX_eq_addX_negY_sub {F : Type u} [Field F] {W : Affine F} {x₁ x₂ : F} (y₁ y₂ : F) (hx : x₁ ≠ x₂) : W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = W.addX x₁ x₂ (W.slope x₁ x₂ y₁ (W.negY x₂ y₂)) - (y₁ - W.negY x₁ y₁) * (y₂ - W.negY x₂ y₂) / (x₂ - x₁) ^ 2

The formula x(P₁ + P₂) = x(P₁ - P₂) - ψ(P₁)ψ(P₂) / (x(P₂) - x(P₁))², where ψ(x,y) = 2y + a₁x + a₃.

theorem WeierstrassCurve.Affine.cyclic_sum_Y_mul_X_sub_X {F : Type u} [Field F] {W : Affine F} {x₁ x₂ : F} (y₁ y₂ : F) (hx : x₁ ≠ x₂) : let x₃ := W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂); y₁ * (x₂ - x₃) + y₂ * (x₃ - x₁) + W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) * (x₁ - x₂) = 0

The formula y(P₁)(x(P₂) - x(P₃)) + y(P₂)(x(P₃) - x(P₁)) + y(P₃)(x(P₁) - x(P₂)) = 0, assuming that P₁ + P₂ + P₃ = O.

theorem WeierstrassCurve.Affine.addY_sub_negY_addY {F : Type u} [Field F] {W : Affine F} {x₁ x₂ : F} (y₁ y₂ : F) (hx : x₁ ≠ x₂) : let x₃ := W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂); let y₃ := W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂); y₃ - W.negY x₃ y₃ = ((y₂ - W.negY x₂ y₂) * (x₁ - x₃) - (y₁ - W.negY x₁ y₁) * (x₂ - x₃)) / (x₂ - x₁)

The formula ψ(P₁ + P₂) = (ψ(P₂)(x(P₁) - x(P₃)) - ψ(P₁)(x(P₂) - x(P₃))) / (x(P₂) - x(P₁)), where ψ(x,y) = 2y + a₁x + a₃.

Nonsingular points

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

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

• zero {R : Type r} [CommRing R] {W' : Affine R} : W'.Point
• some {R : Type r} [CommRing R] {W' : Affine R} {x y : R} (h : W'.Nonsingular x y) : W'.Point

def WeierstrassCurve.Affine.«term_⟮_⟯».«delab_app.WeierstrassCurve.Affine.Point» : 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.Affine.«term_⟮_⟯» : Lean.TrailingParserDescr

For an algebraic extension S of a ring R, the type of nonsingular S-points on a Weierstrass curve W over R in affine coordinates.

Equations

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

Group operations

instance WeierstrassCurve.Affine.Point.instInhabited {R : Type r} [CommRing R] {W' : Affine R} : Inhabited W'.Point

Equations

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

instance WeierstrassCurve.Affine.Point.instZero {R : Type r} [CommRing R] {W' : Affine R} : Zero W'.Point

Equations

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

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

theorem WeierstrassCurve.Affine.Point.some_ne_zero {R : Type r} [CommRing R] {W' : Affine R} {x y : R} (h : W'.Nonsingular x y) : some h ≠ 0

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

The negation of a nonsingular point on a Weierstrass curve in affine coordinates.

Given a nonsingular point P in affine coordinates, use -P instead of neg P.

Equations

• WeierstrassCurve.Affine.Point.zero.neg = 0
• (WeierstrassCurve.Affine.Point.some h).neg = WeierstrassCurve.Affine.Point.some ⋯

instance WeierstrassCurve.Affine.Point.instNeg {R : Type r} [CommRing R] {W' : Affine R} : Neg W'.Point

Equations

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

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

@[simp]

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

@[simp]

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

instance WeierstrassCurve.Affine.Point.instInvolutiveNeg {R : Type r} [CommRing R] {W' : Affine R} : InvolutiveNeg W'.Point

Equations

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

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

The addition of two nonsingular points on a Weierstrass curve in affine coordinates.

Given two nonsingular points P and Q in affine coordinates, use P + Q instead of add P Q.

Equations

• WeierstrassCurve.Affine.Point.zero.add x✝ = x✝
• x✝.add WeierstrassCurve.Affine.Point.zero = x✝
• (WeierstrassCurve.Affine.Point.some h₁).add (WeierstrassCurve.Affine.Point.some h₂) = if hxy : x₁ = x₂ ∧ y₁ = W.negY x₂ y₂ then 0 else WeierstrassCurve.Affine.Point.some ⋯

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

Equations

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

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

Equations

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

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

theorem WeierstrassCurve.Affine.Point.add_some {F : Type u} [Field F] {W : Affine F} {x₁ x₂ y₁ y₂ : F} (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) {h₁ : W.Nonsingular x₁ y₁} {h₂ : W.Nonsingular x₂ y₂} : some h₁ + some h₂ = some ⋯

@[deprecated WeierstrassCurve.Affine.Point.add_some (since := "2025-02-28")]

theorem WeierstrassCurve.Affine.Point.add_of_imp {F : Type u} [Field F] {W : Affine F} {x₁ x₂ y₁ y₂ : F} (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) {h₁ : W.Nonsingular x₁ y₁} {h₂ : W.Nonsingular x₂ y₂} : some h₁ + some h₂ = some ⋯

Alias of WeierstrassCurve.Affine.Point.add_some.

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

Maps across ring homomorphisms

theorem WeierstrassCurve.Affine.map_polynomial {R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : Affine R} (f : R →+* S) : (map W' f).toAffine.polynomial = Polynomial.map (Polynomial.mapRingHom f) W'.polynomial

theorem WeierstrassCurve.Affine.evalEval_baseChange_polynomial_X_Y {R : Type r} [CommRing R] {W' : Affine R} : Polynomial.evalEval (Polynomial.C Polynomial.X) Polynomial.X (baseChange W' (Polynomial (Polynomial R))).toAffine.polynomial = W'.polynomial

theorem WeierstrassCurve.Affine.Equation.map {R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : Affine R} (f : R →+* S) {x y : R} (h : W'.Equation x y) : (WeierstrassCurve.map W' f).toAffine.Equation (f x) (f y)

theorem WeierstrassCurve.Affine.map_equation {R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : Affine R} {f : R →+* S} (x y : R) (hf : Function.Injective ⇑f) : (map W' f).toAffine.Equation (f x) (f y) ↔ W'.Equation x y

theorem WeierstrassCurve.Affine.map_polynomialX {R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : Affine R} (f : R →+* S) : (map W' f).toAffine.polynomialX = Polynomial.map (Polynomial.mapRingHom f) W'.polynomialX

theorem WeierstrassCurve.Affine.map_polynomialY {R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : Affine R} (f : R →+* S) : (map W' f).toAffine.polynomialY = Polynomial.map (Polynomial.mapRingHom f) W'.polynomialY

theorem WeierstrassCurve.Affine.map_nonsingular {R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : Affine R} {f : R →+* S} (x y : R) (hf : Function.Injective ⇑f) : (map W' f).toAffine.Nonsingular (f x) (f y) ↔ W'.Nonsingular x y

theorem WeierstrassCurve.Affine.map_negPolynomial {R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : Affine R} (f : R →+* S) : (map W' f).toAffine.negPolynomial = Polynomial.map (Polynomial.mapRingHom f) W'.negPolynomial

theorem WeierstrassCurve.Affine.map_negY {R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : Affine R} (f : R →+* S) (x y : R) : (map W' f).toAffine.negY (f x) (f y) = f (W'.negY x y)

theorem WeierstrassCurve.Affine.map_linePolynomial {R : Type r} {S : Type s} [CommRing R] [CommRing S] (f : R →+* S) (x y ℓ : R) : linePolynomial (f x) (f y) (f ℓ) = Polynomial.map f (linePolynomial x y ℓ)

theorem WeierstrassCurve.Affine.map_addPolynomial {R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : Affine R} (f : R →+* S) (x y ℓ : R) : (map W' f).toAffine.addPolynomial (f x) (f y) (f ℓ) = Polynomial.map f (W'.addPolynomial x y ℓ)

theorem WeierstrassCurve.Affine.map_addX {R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : Affine R} (f : R →+* S) (x₁ x₂ ℓ : R) : (map W' f).toAffine.addX (f x₁) (f x₂) (f ℓ) = f (W'.addX x₁ x₂ ℓ)

theorem WeierstrassCurve.Affine.map_negAddY {R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : Affine R} (f : R →+* S) (x₁ y₁ x₂ ℓ : R) : (map W' f).toAffine.negAddY (f x₁) (f x₂) (f y₁) (f ℓ) = f (W'.negAddY x₁ x₂ y₁ ℓ)

theorem WeierstrassCurve.Affine.map_addY {R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : Affine R} (f : R →+* S) (x₁ y₁ x₂ ℓ : R) : (map W' f).toAffine.addY (f x₁) (f x₂) (f y₁) (f ℓ) = f ((toAffine W').addY x₁ x₂ y₁ ℓ)

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

Base changes across algebra homomorphisms

theorem WeierstrassCurve.Affine.baseChange_polynomial {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Affine R} [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) : (baseChange W' B).toAffine.polynomial = Polynomial.map (Polynomial.mapRingHom ↑f) (baseChange W' A).toAffine.polynomial

theorem WeierstrassCurve.Affine.Equation.baseChange {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Affine R} [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) {x y : A} (h : (WeierstrassCurve.baseChange W' A).toAffine.Equation x y) : (WeierstrassCurve.baseChange W' B).toAffine.Equation (f x) (f y)

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

theorem WeierstrassCurve.Affine.baseChange_polynomialX {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Affine R} [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) : (baseChange W' B).toAffine.polynomialX = Polynomial.map (Polynomial.mapRingHom ↑f) (baseChange W' A).toAffine.polynomialX

theorem WeierstrassCurve.Affine.baseChange_polynomialY {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Affine R} [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) : (baseChange W' B).toAffine.polynomialY = Polynomial.map (Polynomial.mapRingHom ↑f) (baseChange W' A).toAffine.polynomialY

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

theorem WeierstrassCurve.Affine.baseChange_negPolynomial {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Affine R} [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) : (baseChange W' B).toAffine.negPolynomial = Polynomial.map (Polynomial.mapRingHom ↑f) (baseChange W' A).toAffine.negPolynomial

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

theorem WeierstrassCurve.Affine.baseChange_addPolynomial {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Affine R} [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (x y ℓ : A) : (baseChange W' B).toAffine.addPolynomial (f x) (f y) (f ℓ) = Polynomial.map (↑f) ((baseChange W' A).toAffine.addPolynomial x y ℓ)

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

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

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

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

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

The function from W⟮F⟯ to W⟮K⟯ induced by an algebra homomorphism f : 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 f WeierstrassCurve.Affine.Point.zero = 0
• WeierstrassCurve.Affine.Point.mapFun f (WeierstrassCurve.Affine.Point.some h) = WeierstrassCurve.Affine.Point.some ⋯

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

The group homomorphism from W⟮F⟯ to W⟮K⟯ induced by an algebra homomorphism f : 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 f = { toFun := WeierstrassCurve.Affine.Point.mapFun f, map_zero' := ⋯, map_add' := ⋯ }

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

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

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

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

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

@[reducible, inline]

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

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 F K = WeierstrassCurve.Affine.Point.map (Algebra.ofId F K)

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

Elliptic curves

theorem WeierstrassCurve.nonsingular {R : Type u} [CommRing R] (E : WeierstrassCurve R) [E.IsElliptic] [Nontrivial R] {x y : R} (h : E.toAffine.Equation x y) : E.toAffine.Nonsingular x y