Weierstrass equations and the nonsingular condition in affine coordinates

Let W be a Weierstrass curve over a commutative ring R 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.

This file defines polynomials associated to Weierstrass equations and the nonsingular condition in affine coordinates. The group law on the actual type of nonsingular points in affine coordinates will be defined in Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean, based on the formulae for group operations in Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Formula.lean.

Main definitions

• WeierstrassCurve.Affine.Equation: the Weierstrass equation in affine coordinates.
• WeierstrassCurve.Affine.Nonsingular: the nonsingular condition in affine coordinates.

Main statements

• WeierstrassCurve.Affine.equation_iff_nonsingular: an elliptic curve in affine coordinates is nonsingular at every point.

Implementation notes

All definitions and lemmas for Weierstrass curves in affine coordinates live in the namespace WeierstrassCurve.Affine to distinguish them from those in other coordinates. This is simply an abbreviation for WeierstrassCurve that can be converted using WeierstrassCurve.toAffine.

References

J Silverman, The Arithmetic of Elliptic Curves

Tags

elliptic curve, affine, Weierstrass equation, nonsingular

Affine coordinates

@[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 in affine coordinates

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 ↔ (toAffine ({ u := 1, r := x, s := 0, t := y } • W)).Equation 0 0

The nonsingular condition in affine coordinates

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 ↔ (toAffine ({ u := 1, r := x, s := 0, t := y } • W)).Nonsingular 0 0

theorem WeierstrassCurve.Affine.equation_iff_nonsingular_of_Δ_ne_zero {R : Type r} [CommRing R] {W : Affine R} {x y : R} (hΔ : Δ W ≠ 0) : W.Equation x y ↔ W.Nonsingular x y

theorem WeierstrassCurve.Affine.equation_iff_nonsingular {R : Type r} [CommRing R] {W : Affine R} [Nontrivial R] [WeierstrassCurve.IsElliptic W] {x y : R} : (toAffine W).Equation x y ↔ (toAffine W).Nonsingular x y

@[deprecated WeierstrassCurve.Affine.equation_iff_nonsingular_of_Δ_ne_zero (since := "2025-03-01")]

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

Alias of WeierstrassCurve.Affine.equation_iff_nonsingular_of_Δ_ne_zero.

@[deprecated WeierstrassCurve.Affine.equation_iff_nonsingular_of_Δ_ne_zero (since := "2025-03-01")]

theorem WeierstrassCurve.Affine.nonsingular_of_Δ_ne_zero {R : Type r} [CommRing R] {W : Affine R} {x y : R} (hΔ : Δ W ≠ 0) : W.Equation x y ↔ W.Nonsingular x y

Alias of WeierstrassCurve.Affine.equation_iff_nonsingular_of_Δ_ne_zero.

@[deprecated WeierstrassCurve.Affine.equation_iff_nonsingular (since := "2025-03-01")]

theorem WeierstrassCurve.Affine.nonsingular {R : Type r} [CommRing R] {W : Affine R} [Nontrivial R] [WeierstrassCurve.IsElliptic W] {x y : R} : (toAffine W).Equation x y ↔ (toAffine W).Nonsingular x y

Alias of WeierstrassCurve.Affine.equation_iff_nonsingular.

Maps and base changes

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