Group law on Weierstrass curves

This file proves that the nonsingular rational points on a Weierstrass curve form an abelian group under the geometric group law defined in Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean, in Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean, and in Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean.

Mathematical background

Let W be a Weierstrass curve over a field F given by a Weierstrass equation W(X, Y) = 0 in affine coordinates. As in Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean, the set of nonsingular rational points W⟮F⟯ of W consist of the unique point at infinity 𝓞 and nonsingular affine points (x, y). With this description, there is an addition-preserving injection between W⟮F⟯ and the ideal class group of the affine coordinate ring F[W] := F[X, Y] / ⟨W(X, Y)⟩ of W. This is given by mapping 𝓞 to the trivial ideal class and a nonsingular affine point (x, y) to the ideal class of the invertible ideal ⟨X - x, Y - y⟩. Proving that this is well-defined and preserves addition reduces to equalities of integral ideals checked in WeierstrassCurve.Affine.CoordinateRing.XYIdeal_neg_mul and in WeierstrassCurve.Affine.CoordinateRing.XYIdeal_mul_XYIdeal via explicit ideal computations. Now F[W] is a free rank two F[X]-algebra with basis {1, Y}, so every element of F[W] is of the form p + qY for some p, q in F[X], and there is an algebra norm N : F[W] → F[X]. Injectivity can then be shown by computing the degree of such a norm N(p + qY) in two different ways, which is done in WeierstrassCurve.Affine.CoordinateRing.degree_norm_smul_basis and in the auxiliary lemmas in the proof of WeierstrassCurve.Affine.Point.instAddCommGroup.

When W is given in Jacobian coordinates, WeierstrassCurve.Jacobian.Point.toAffineAddEquiv pulls back the group law on WeierstrassCurve.Affine.Point to WeierstrassCurve.Jacobian.Point.

When W is given in projective coordinates, WeierstrassCurve.Projective.Point.toAffineAddEquiv pulls back the group law on WeierstrassCurve.Affine.Point to WeierstrassCurve.Projective.Point.

Main definitions

• WeierstrassCurve.Affine.CoordinateRing: the coordinate ring F[W] of a Weierstrass curve W.
• WeierstrassCurve.Affine.CoordinateRing.basis: the power basis of F[W] over F[X].

Main statements

• WeierstrassCurve.Affine.CoordinateRing.instIsDomainCoordinateRing: the affine coordinate ring of a Weierstrass curve is an integral domain.
• WeierstrassCurve.Affine.CoordinateRing.degree_norm_smul_basis: the degree of the norm of an element in the affine coordinate ring in terms of its power basis.
• WeierstrassCurve.Affine.Point.instAddCommGroup: the type of nonsingular points W⟮F⟯ in affine coordinates forms an abelian group under addition.
• WeierstrassCurve.Jacobian.Point.instAddCommGroup: the type of nonsingular points on a Weierstrass curve in Jacobian coordinates forms an abelian group under addition.
• WeierstrassCurve.Projective.Point.instAddCommGroup: the type of nonsingular points on a Weierstrass curve in projective coordinates forms an abelian group under addition.

References

https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.6/LIPIcs.ITP.2023.6.pdf

Tags

elliptic curve, group law, class group

Weierstrass curves in affine coordinates

@[reducible, inline]

abbrev WeierstrassCurve.Affine.CoordinateRing {R : Type u} [CommRing R] (W : Affine R) : Type u

The affine coordinate ring R[W] := R[X, Y] / ⟨W(X, Y)⟩ of a Weierstrass curve W.

Equations

• W.CoordinateRing = AdjoinRoot W.polynomial

@[reducible, inline]

abbrev WeierstrassCurve.Affine.FunctionField {R : Type u} [CommRing R] (W : Affine R) : Type u

The function field R(W) := Frac(R[W]) of a Weierstrass curve W.

Equations

• W.FunctionField = FractionRing W.CoordinateRing

The coordinate ring as an R[X]-algebra

noncomputable instance WeierstrassCurve.Affine.CoordinateRing.instAlgebra {R : Type u} [CommRing R] (W : Affine R) : Algebra R W.CoordinateRing

Equations

• WeierstrassCurve.Affine.CoordinateRing.instAlgebra W = Ideal.Quotient.algebra R

noncomputable instance WeierstrassCurve.Affine.CoordinateRing.instAlgebraPolynomial {R : Type u} [CommRing R] (W : Affine R) : Algebra (Polynomial R) W.CoordinateRing

Equations

• WeierstrassCurve.Affine.CoordinateRing.instAlgebraPolynomial W = Ideal.Quotient.algebra (Polynomial R)

instance WeierstrassCurve.Affine.CoordinateRing.instIsScalarTowerPolynomial {R : Type u} [CommRing R] (W : Affine R) : IsScalarTower R (Polynomial R) W.CoordinateRing

instance WeierstrassCurve.Affine.CoordinateRing.instSubsingleton {R : Type u} [CommRing R] (W : Affine R) [Subsingleton R] : Subsingleton W.CoordinateRing

@[reducible, inline]

noncomputable abbrev WeierstrassCurve.Affine.CoordinateRing.mk {R : Type u} [CommRing R] (W : Affine R) : Polynomial (Polynomial R) →+* W.CoordinateRing

The natural ring homomorphism mapping R[X][Y] to R[W].

Equations

• WeierstrassCurve.Affine.CoordinateRing.mk W = AdjoinRoot.mk W.polynomial

noncomputable def WeierstrassCurve.Affine.CoordinateRing.basis {R : Type u} [CommRing R] (W : Affine R) : Basis (Fin 2) (Polynomial R) W.CoordinateRing

The power basis {1, Y} for R[W] over R[X].

Equations

• WeierstrassCurve.Affine.CoordinateRing.basis W = ⋯.by_cases (fun (x : Subsingleton R) => default) fun (x : Nontrivial R) => (AdjoinRoot.powerBasis' ⋯).basis.reindex (finCongr ⋯)

theorem WeierstrassCurve.Affine.CoordinateRing.basis_apply {R : Type u} [CommRing R] (W : Affine R) (n : Fin 2) : (CoordinateRing.basis W) n = (AdjoinRoot.powerBasis' ⋯).gen ^ ↑n

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.basis_zero {R : Type u} [CommRing R] (W : Affine R) : (CoordinateRing.basis W) 0 = 1

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.basis_one {R : Type u} [CommRing R] (W : Affine R) : (CoordinateRing.basis W) 1 = (mk W) Polynomial.X

theorem WeierstrassCurve.Affine.CoordinateRing.coe_basis {R : Type u} [CommRing R] (W : Affine R) : ⇑(CoordinateRing.basis W) = ![1, (mk W) Polynomial.X]

theorem WeierstrassCurve.Affine.CoordinateRing.smul {R : Type u} [CommRing R] {W : Affine R} (x : Polynomial R) (y : W.CoordinateRing) : x • y = (mk W) (Polynomial.C x) * y

theorem WeierstrassCurve.Affine.CoordinateRing.smul_basis_eq_zero {R : Type u} [CommRing R] {W : Affine R} {p q : Polynomial R} (hpq : p • 1 + q • (mk W) Polynomial.X = 0) : p = 0 ∧ q = 0

theorem WeierstrassCurve.Affine.CoordinateRing.exists_smul_basis_eq {R : Type u} [CommRing R] {W : Affine R} (x : W.CoordinateRing) : ∃ (p : Polynomial R) (q : Polynomial R), p • 1 + q • (mk W) Polynomial.X = x

theorem WeierstrassCurve.Affine.CoordinateRing.smul_basis_mul_C {R : Type u} [CommRing R] (W : Affine R) (y p q : Polynomial R) : (p • 1 + q • (mk W) Polynomial.X) * (mk W) (Polynomial.C y) = (p * y) • 1 + (q * y) • (mk W) Polynomial.X

theorem WeierstrassCurve.Affine.CoordinateRing.smul_basis_mul_Y {R : Type u} [CommRing R] (W : Affine R) (p q : Polynomial R) : (p • 1 + q • (mk W) Polynomial.X) * (mk W) Polynomial.X = (q * (Polynomial.X ^ 3 + Polynomial.C W.a₂ * Polynomial.X ^ 2 + Polynomial.C W.a₄ * Polynomial.X + Polynomial.C W.a₆)) • 1 + (p - q * (Polynomial.C W.a₁ * Polynomial.X + Polynomial.C W.a₃)) • (mk W) Polynomial.X

noncomputable def WeierstrassCurve.Affine.CoordinateRing.map {R : Type u} {S : Type v} [CommRing R] [CommRing S] (W : Affine R) (f : R →+* S) : W.CoordinateRing →+* (WeierstrassCurve.map W f).toAffine.CoordinateRing

The ring homomorphism R[W] →+* S[W.map f] induced by a ring homomorphism f : R →+* S.

Equations

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

theorem WeierstrassCurve.Affine.CoordinateRing.map_mk {R : Type u} {S : Type v} [CommRing R] [CommRing S] (W : Affine R) (f : R →+* S) (x : Polynomial (Polynomial R)) : (map W f) ((mk W) x) = (mk (WeierstrassCurve.map W f)) (Polynomial.map (Polynomial.mapRingHom f) x)

theorem WeierstrassCurve.Affine.CoordinateRing.map_smul {R : Type u} {S : Type v} [CommRing R] [CommRing S] {W : Affine R} (f : R →+* S) (x : Polynomial R) (y : W.CoordinateRing) : (map W f) (x • y) = Polynomial.map f x • (map W f) y

theorem WeierstrassCurve.Affine.CoordinateRing.map_injective {R : Type u} {S : Type v} [CommRing R] [CommRing S] (W : Affine R) {f : R →+* S} (hf : Function.Injective ⇑f) : Function.Injective ⇑(map W f)

instance WeierstrassCurve.Affine.CoordinateRing.instIsDomain {R : Type u} [CommRing R] (W : Affine R) [IsDomain R] : IsDomain W.CoordinateRing

Ideals in the coordinate ring over a ring

noncomputable def WeierstrassCurve.Affine.CoordinateRing.XClass {R : Type u} [CommRing R] (W : Affine R) (x : R) : W.CoordinateRing

The class of the element X - x in R[W] for some x in R.

Equations

• WeierstrassCurve.Affine.CoordinateRing.XClass W x = (WeierstrassCurve.Affine.CoordinateRing.mk W) (Polynomial.C (Polynomial.X - Polynomial.C x))

theorem WeierstrassCurve.Affine.CoordinateRing.XClass_ne_zero {R : Type u} [CommRing R] (W : Affine R) [Nontrivial R] (x : R) : XClass W x ≠ 0

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

The class of the element Y - y(X) in R[W] for some y(X) in R[X].

Equations

• WeierstrassCurve.Affine.CoordinateRing.YClass W y = (WeierstrassCurve.Affine.CoordinateRing.mk W) (Polynomial.X - Polynomial.C y)

theorem WeierstrassCurve.Affine.CoordinateRing.YClass_ne_zero {R : Type u} [CommRing R] (W : Affine R) [Nontrivial R] (y : Polynomial R) : YClass W y ≠ 0

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

noncomputable def WeierstrassCurve.Affine.CoordinateRing.XIdeal {R : Type u} [CommRing R] (W : Affine R) (x : R) : Ideal W.CoordinateRing

The ideal ⟨X - x⟩ of R[W] for some x in R.

Equations

• WeierstrassCurve.Affine.CoordinateRing.XIdeal W x = Ideal.span {WeierstrassCurve.Affine.CoordinateRing.XClass W x}

noncomputable def WeierstrassCurve.Affine.CoordinateRing.YIdeal {R : Type u} [CommRing R] (W : Affine R) (y : Polynomial R) : Ideal W.CoordinateRing

The ideal ⟨Y - y(X)⟩ of R[W] for some y(X) in R[X].

Equations

• WeierstrassCurve.Affine.CoordinateRing.YIdeal W y = Ideal.span {WeierstrassCurve.Affine.CoordinateRing.YClass W y}

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

The ideal ⟨X - x, Y - y(X)⟩ of R[W] for some x in R and y(X) in R[X].

Equations

• WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x y = Ideal.span {WeierstrassCurve.Affine.CoordinateRing.XClass W x, WeierstrassCurve.Affine.CoordinateRing.YClass W y}

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

theorem WeierstrassCurve.Affine.CoordinateRing.XYIdeal_add_eq {R : Type u} [CommRing R] (W : Affine R) (x₁ x₂ y₁ L : R) : XYIdeal W (W.addX x₁ x₂ L) (Polynomial.C (W.addY x₁ x₂ y₁ L)) = Ideal.span {(mk W) (W.negPolynomial - Polynomial.C (linePolynomial x₁ y₁ L))} ⊔ XIdeal W (W.addX x₁ x₂ L)

noncomputable def WeierstrassCurve.Affine.CoordinateRing.quotientXYIdealEquiv {R : Type u} [CommRing R] (W : Affine R) {x : R} {y : Polynomial R} (h : Polynomial.eval x (Polynomial.eval y W.polynomial) = 0) : (W.CoordinateRing ⧸ XYIdeal W x y) ≃ₐ[R] R

The R-algebra isomorphism from R[W] / ⟨X - x, Y - y(X)⟩ to R obtained by evaluation at some y(X) in R[X] and at some x in R provided that W(x, y(x)) = 0.

Equations

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

Ideals in the coordinate ring over a field

theorem WeierstrassCurve.Affine.CoordinateRing.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₂)) : (mk W) (Polynomial.C (W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) = -(XClass W x₁ * XClass W x₂ * XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)))

theorem WeierstrassCurve.Affine.CoordinateRing.XYIdeal_eq₂ {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₂)) : XYIdeal W x₂ (Polynomial.C y₂) = XYIdeal W x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))

theorem WeierstrassCurve.Affine.CoordinateRing.XYIdeal_neg_mul {F : Type u} [Field F] {W : Affine F} {x y : F} (h : W.Nonsingular x y) : XYIdeal W x (Polynomial.C (W.negY x y)) * XYIdeal W x (Polynomial.C y) = XIdeal W x

theorem WeierstrassCurve.Affine.CoordinateRing.XYIdeal_mul_XYIdeal {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₂)) : XIdeal W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) * (XYIdeal W x₁ (Polynomial.C y₁) * XYIdeal W x₂ (Polynomial.C y₂)) = YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) * XYIdeal W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (Polynomial.C (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)))

noncomputable def WeierstrassCurve.Affine.CoordinateRing.XYIdeal' {F : Type u} [Field F] {W : Affine F} {x y : F} (h : W.Nonsingular x y) : (FractionalIdeal (nonZeroDivisors W.CoordinateRing) W.FunctionField)ˣ

The non-zero fractional ideal ⟨X - x, Y - y⟩ of F(W) for some x and y in F.

Equations

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

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

theorem WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal'_of_Yeq {F : Type u} [Field F] {W : Affine F} {x y : F} (h : W.Nonsingular x y) : ClassGroup.mk (XYIdeal' ⋯) * ClassGroup.mk (XYIdeal' h) = 1

theorem WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal' {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₂)) : ClassGroup.mk (XYIdeal' h₁) * ClassGroup.mk (XYIdeal' h₂) = ClassGroup.mk (XYIdeal' ⋯)

Norms on the coordinate ring

theorem WeierstrassCurve.Affine.CoordinateRing.norm_smul_basis {R : Type u} [CommRing R] (W : Affine R) (p q : Polynomial R) : (Algebra.norm (Polynomial R)) (p • 1 + q • (mk W) Polynomial.X) = p ^ 2 - p * q * (Polynomial.C W.a₁ * Polynomial.X + Polynomial.C W.a₃) - q ^ 2 * (Polynomial.X ^ 3 + Polynomial.C W.a₂ * Polynomial.X ^ 2 + Polynomial.C W.a₄ * Polynomial.X + Polynomial.C W.a₆)

theorem WeierstrassCurve.Affine.CoordinateRing.coe_norm_smul_basis {R : Type u} [CommRing R] (W : Affine R) (p q : Polynomial R) : (AdjoinRoot.of W.polynomial) ((Algebra.norm (Polynomial R)) (p • 1 + q • (mk W) Polynomial.X)) = (mk W) ((Polynomial.C p + Polynomial.C q * Polynomial.X) * (Polynomial.C p + Polynomial.C q * (-Polynomial.X - Polynomial.C (Polynomial.C W.a₁ * Polynomial.X + Polynomial.C W.a₃))))

theorem WeierstrassCurve.Affine.CoordinateRing.degree_norm_smul_basis {R : Type u} [CommRing R] (W : Affine R) [IsDomain R] (p q : Polynomial R) : ((Algebra.norm (Polynomial R)) (p • 1 + q • (mk W) Polynomial.X)).degree = 2 • p.degree ⊔ (2 • q.degree + 3)

theorem WeierstrassCurve.Affine.CoordinateRing.degree_norm_ne_one {R : Type u} [CommRing R] {W : Affine R} [IsDomain R] (x : W.CoordinateRing) : ((Algebra.norm (Polynomial R)) x).degree ≠ 1

theorem WeierstrassCurve.Affine.CoordinateRing.natDegree_norm_ne_one {R : Type u} [CommRing R] {W : Affine R} [IsDomain R] (x : W.CoordinateRing) : ((Algebra.norm (Polynomial R)) x).natDegree ≠ 1

The axioms for nonsingular rational points on a Weierstrass curve

noncomputable def WeierstrassCurve.Affine.Point.toClassFun {F : Type u} [Field F] {W : Affine F} : W.Point → Additive (ClassGroup W.CoordinateRing)

The set function mapping a nonsingular affine point (x, y) of a Weierstrass curve W to the class of the non-zero fractional ideal ⟨X - x, Y - y⟩ in the ideal class group of F[W].

Equations

• WeierstrassCurve.Affine.Point.zero.toClassFun = 0
• (WeierstrassCurve.Affine.Point.some h).toClassFun = Additive.ofMul (ClassGroup.mk (WeierstrassCurve.Affine.CoordinateRing.XYIdeal' h))

noncomputable def WeierstrassCurve.Affine.Point.toClass {F : Type u} [Field F] {W : Affine F} : W.Point →+ Additive (ClassGroup W.CoordinateRing)

The group homomorphism mapping a nonsingular affine point (x, y) of a Weierstrass curve W to the class of the non-zero fractional ideal ⟨X - x, Y - y⟩ in the ideal class group of F[W].

Equations

• WeierstrassCurve.Affine.Point.toClass = { toFun := WeierstrassCurve.Affine.Point.toClassFun, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

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

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

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

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

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

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

Equations

• WeierstrassCurve.Affine.Point.instAddCommGroup = AddCommGroup.mk ⋯

Weierstrass curves in projective coordinates

noncomputable instance WeierstrassCurve.Projective.Point.instAddCommGroup {F : Type u} [Field F] {W : Projective F} : AddCommGroup W.Point

Equations

• WeierstrassCurve.Projective.Point.instAddCommGroup = AddCommGroup.mk ⋯

Weierstrass curves in Jacobian coordinates

noncomputable instance WeierstrassCurve.Jacobian.Point.instAddCommGroup {F : Type u} [Field F] {W : Jacobian F} : AddCommGroup W.Point

Equations

• WeierstrassCurve.Jacobian.Point.instAddCommGroup = AddCommGroup.mk ⋯

Elliptic curves in affine coordinates

def WeierstrassCurve.Affine.Point.mk {R : Type u_1} [Nontrivial R] [CommRing R] (E : WeierstrassCurve R) [E.IsElliptic] {x y : R} (h : E.toAffine.Equation x y) : E.toAffine.Point

An affine point on an elliptic curve E over a commutative ring R.

Equations

• WeierstrassCurve.Affine.Point.mk E h = WeierstrassCurve.Affine.Point.some ⋯