Documentation

Mathlib.AlgebraicGeometry.EllipticCurve.Group

Group law on Weierstrass curves #

This file proves that the nonsingular rational points on a Weierstrass curve forms an abelian group under the geometric group law defined in Mathlib.AlgebraicGeometry.EllipticCurve.Affine.

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, the set of nonsingular rational points W⟮F⟯ of W consist of the unique point at infinity $0$ 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 coordinate ring $F[W] := F[X, Y] / \langle W(X, Y)\rangle$ of W. This is defined by mapping the point at infinity $0$ to the trivial ideal class and an affine point $(x, y)$ to the ideal class of the invertible fractional ideal $\langle X - x, Y - y\rangle$. Proving that this is well-defined and preserves addition reduce to checking several equalities of integral ideals, which is done 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] \to 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.instAddCommGroupPoint.

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 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 coordinate ring in terms of the power basis.
WeierstrassCurve.Affine.Point.instAddCommGroupPoint: the type of nonsingular rational points on a Weierstrass curve 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 : WeierstrassCurve.Affine R) :

The coordinate ring $R[W] := R[X, Y] / \langle W(X, Y) \rangle$ of W.

Equations

W.CoordinateRing = AdjoinRoot W.polynomial

Instances For

@[reducible, inline]

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

The function field $R(W) := \mathrm{Frac}(R[W])$ of W.

Equations

W.FunctionField = FractionRing W.CoordinateRing

Instances For

Ideals in the coordinate ring over a ring #

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

IsDomain W.CoordinateRing

Equations

⋯ = ⋯

instance WeierstrassCurve.Affine.CoordinateRing.instIsDomainCoordinateRing_of_Field {F : Type u} [Field F] (W : WeierstrassCurve.Affine F) :

IsDomain W.CoordinateRing

Equations

⋯ = ⋯

@[reducible, inline]

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

Polynomial (Polynomial R) →+* W.CoordinateRing

An element of the coordinate ring R[W] of W over R.

Equations

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

Instances For

noncomputable def WeierstrassCurve.Affine.CoordinateRing.XClass {R : Type u} [CommRing R] (W : WeierstrassCurve.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))

Instances For

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

WeierstrassCurve.Affine.CoordinateRing.XClass W x ≠ 0

noncomputable def WeierstrassCurve.Affine.CoordinateRing.YClass {R : Type u} [CommRing R] (W : WeierstrassCurve.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)

Instances For

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

WeierstrassCurve.Affine.CoordinateRing.YClass W y ≠ 0

theorem WeierstrassCurve.Affine.CoordinateRing.C_addPolynomial {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) (L : R) :

(WeierstrassCurve.Affine.CoordinateRing.mk W) (Polynomial.C (W.addPolynomial x y L)) = (WeierstrassCurve.Affine.CoordinateRing.mk W) ((Polynomial.X - Polynomial.C (x.linePolynomial y L)) * (W.negPolynomial - Polynomial.C (x.linePolynomial y L)))

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

Ideal W.CoordinateRing

The ideal $\langle X - x \rangle$ of $R[W]$ for some $x \in R$.

Equations

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

Instances For

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

Ideal W.CoordinateRing

The ideal $\langle Y - y(X) \rangle$ 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}

Instances For

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

Ideal W.CoordinateRing

The ideal $\langle X - x, Y - y(X) \rangle$ 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}

Instances For

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

WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x (Polynomial.C y) = WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x (x.linePolynomial y L)

theorem WeierstrassCurve.Affine.CoordinateRing.XYIdeal_add_eq {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x₁ : R) (x₂ : R) (y₁ : R) (L : R) :

WeierstrassCurve.Affine.CoordinateRing.XYIdeal W (W.addX x₁ x₂ L) (Polynomial.C (W.addY x₁ x₂ y₁ L)) = Ideal.span {(WeierstrassCurve.Affine.CoordinateRing.mk W) (W.negPolynomial - Polynomial.C (x₁.linePolynomial y₁ L))} ⊔ WeierstrassCurve.Affine.CoordinateRing.XIdeal W (W.addX x₁ x₂ L)

Ideals in the coordinate ring over a field #

theorem WeierstrassCurve.Affine.CoordinateRing.C_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₂) :

(WeierstrassCurve.Affine.CoordinateRing.mk W) (Polynomial.C (W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) = -(WeierstrassCurve.Affine.CoordinateRing.XClass W x₁ * WeierstrassCurve.Affine.CoordinateRing.XClass W x₂ * WeierstrassCurve.Affine.CoordinateRing.XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)))

theorem WeierstrassCurve.Affine.CoordinateRing.XYIdeal_eq₂ {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₂) :

WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x₂ (Polynomial.C y₂) = WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x₂ (x₁.linePolynomial y₁ (W.slope x₁ x₂ y₁ y₂))

theorem WeierstrassCurve.Affine.CoordinateRing.XYIdeal_neg_mul {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x : F} {y : F} (h : W.nonsingular x y) :

WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x (Polynomial.C (W.negY x y)) * WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x (Polynomial.C y) = WeierstrassCurve.Affine.CoordinateRing.XIdeal W x

theorem WeierstrassCurve.Affine.CoordinateRing.XYIdeal_mul_XYIdeal {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₂) :

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

(FractionalIdeal (nonZeroDivisors W.CoordinateRing) W.FunctionField)ˣ

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

Equations

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

Instances For

theorem WeierstrassCurve.Affine.CoordinateRing.XYIdeal'_eq {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x : F} {y : F} (h : W.nonsingular x y) :

↑(WeierstrassCurve.Affine.CoordinateRing.XYIdeal' h) = ↑(WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x (Polynomial.C y))

theorem WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal'_of_Yeq {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x : F} {y : F} (h : W.nonsingular x y) :

ClassGroup.mk (WeierstrassCurve.Affine.CoordinateRing.XYIdeal' ⋯) * ClassGroup.mk (WeierstrassCurve.Affine.CoordinateRing.XYIdeal' h) = 1

theorem WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal' {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₂) :

ClassGroup.mk (WeierstrassCurve.Affine.CoordinateRing.XYIdeal' h₁) * ClassGroup.mk (WeierstrassCurve.Affine.CoordinateRing.XYIdeal' h₂) = ClassGroup.mk (WeierstrassCurve.Affine.CoordinateRing.XYIdeal' ⋯)

The coordinate ring as an `R[X]`-algebra #

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

Algebra (Polynomial R) W.CoordinateRing

Equations

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

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

Algebra R W.CoordinateRing

Equations

WeierstrassCurve.Affine.CoordinateRing.instAlgebraCoordinateRing' W = Ideal.Quotient.algebra R

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

IsScalarTower R (Polynomial R) W.CoordinateRing

Equations

⋯ = ⋯

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

Subsingleton W.CoordinateRing

Equations

⋯ = ⋯

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

(W.CoordinateRing ⧸ WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x y) ≃ₐ[R] R

The $R$-algebra isomorphism from $R[W] / \langle X - x, Y - y(X) \rangle$ to $R$ obtained by evaluation at $y(X)$ and at $x$ provided that $W(x, y(x)) = 0$.

Equations

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

Instances For

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

Basis (Fin 2) (Polynomial R) W.CoordinateRing

The basis ${1, Y}$ for the coordinate ring $R[W]$ over the polynomial ring $R[X]$.

Equations

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

Instances For

theorem WeierstrassCurve.Affine.CoordinateRing.basis_apply {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (n : Fin 2) :

(WeierstrassCurve.Affine.CoordinateRing.basis W) n = (AdjoinRoot.powerBasis' ⋯).gen ^ ↑n

@[simp]

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

(WeierstrassCurve.Affine.CoordinateRing.basis W) 0 = 1

@[simp]

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

(WeierstrassCurve.Affine.CoordinateRing.basis W) 1 = (WeierstrassCurve.Affine.CoordinateRing.mk W) Polynomial.X

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

⇑(WeierstrassCurve.Affine.CoordinateRing.basis W) = ![1, (WeierstrassCurve.Affine.CoordinateRing.mk W) Polynomial.X]

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

x • y = (WeierstrassCurve.Affine.CoordinateRing.mk W) (Polynomial.C x) * y

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

p = 0 ∧ q = 0

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

∃ (p : Polynomial R) (q : Polynomial R), p • 1 + q • (WeierstrassCurve.Affine.CoordinateRing.mk W) Polynomial.X = x

theorem WeierstrassCurve.Affine.CoordinateRing.smul_basis_mul_C {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (y : Polynomial R) (p : Polynomial R) (q : Polynomial R) :

(p • 1 + q • (WeierstrassCurve.Affine.CoordinateRing.mk W) Polynomial.X) * (WeierstrassCurve.Affine.CoordinateRing.mk W) (Polynomial.C y) = (p * y) • 1 + (q * y) • (WeierstrassCurve.Affine.CoordinateRing.mk W) Polynomial.X

theorem WeierstrassCurve.Affine.CoordinateRing.smul_basis_mul_Y {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (p : Polynomial R) (q : Polynomial R) :

(p • 1 + q • (WeierstrassCurve.Affine.CoordinateRing.mk W) Polynomial.X) * (WeierstrassCurve.Affine.CoordinateRing.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₃)) • (WeierstrassCurve.Affine.CoordinateRing.mk W) Polynomial.X

Norms on the coordinate ring #

theorem WeierstrassCurve.Affine.CoordinateRing.norm_smul_basis {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (p : Polynomial R) (q : Polynomial R) :

(Algebra.norm (Polynomial R)) (p • 1 + q • (WeierstrassCurve.Affine.CoordinateRing.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 : WeierstrassCurve.Affine R) (p : Polynomial R) (q : Polynomial R) :

(AdjoinRoot.of W.polynomial) ((Algebra.norm (Polynomial R)) (p • 1 + q • (WeierstrassCurve.Affine.CoordinateRing.mk W) Polynomial.X)) = (WeierstrassCurve.Affine.CoordinateRing.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 : WeierstrassCurve.Affine R) [IsDomain R] (p : Polynomial R) (q : Polynomial R) :

((Algebra.norm (Polynomial R)) (p • 1 + q • (WeierstrassCurve.Affine.CoordinateRing.mk W) Polynomial.X)).degree = max (2 • p.degree) (2 • q.degree + 3)

theorem WeierstrassCurve.Affine.CoordinateRing.degree_norm_ne_one {R : Type u} [CommRing R] {W : WeierstrassCurve.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 : WeierstrassCurve.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 : WeierstrassCurve.Affine F} :

W.Point → Additive (ClassGroup W.CoordinateRing)

The set function mapping an affine point $(x, y)$ of W to the class of the non-zero fractional ideal $\langle X - x, Y - y \rangle$ of $F(W)$ in the class group of $F[W]$.

Equations

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

Instances For

@[simp]

theorem WeierstrassCurve.Affine.Point.toClass_apply {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} :

∀ (a : W.Point), WeierstrassCurve.Affine.Point.toClass a = a.toClassFun

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

W.Point →+ Additive (ClassGroup W.CoordinateRing)

The group homomorphism mapping an affine point $(x, y)$ of W to the class of the non-zero fractional ideal $\langle X - x, Y - y \rangle$ of $F(W)$ in the class group of $F[W]$.

Equations

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

Instances For

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

WeierstrassCurve.Affine.Point.toClass 0 = 0

theorem WeierstrassCurve.Affine.Point.toClass_some {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x : F} {y : F} (h : W.nonsingular x y) :

WeierstrassCurve.Affine.Point.toClass (WeierstrassCurve.Affine.Point.some h) = ClassGroup.mk (WeierstrassCurve.Affine.CoordinateRing.XYIdeal' h)

theorem WeierstrassCurve.Affine.Point.add_eq_zero {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} (P : W.Point) (Q : W.Point) :

P + Q = 0 ↔ P = -Q

theorem WeierstrassCurve.Affine.Point.add_left_neg {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} (P : W.Point) :

-P + P = 0

theorem WeierstrassCurve.Affine.Point.neg_add_eq_zero {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} (P : W.Point) (Q : W.Point) :

-P + Q = 0 ↔ P = Q

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

WeierstrassCurve.Affine.Point.toClass P = 0 ↔ P = 0

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

Function.Injective ⇑WeierstrassCurve.Affine.Point.toClass

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

P + Q = Q + P

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

P + Q + R = P + (Q + R)

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

AddCommGroup W.Point

Equations

WeierstrassCurve.Affine.Point.instAddCommGroupPoint = AddCommGroup.mk ⋯

Elliptic curves in affine coordinates #

def EllipticCurve.Affine.Point.mk {R : Type} [Nontrivial R] [CommRing R] (E : EllipticCurve R) {x : R} {y : R} (h : E.toAffine.equation x y) :

E.toAffine.Point

An affine point on an elliptic curve E over R.

Equations

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

Instances For