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 ringF[W]of a Weierstrass curveW.WeierstrassCurve.Affine.CoordinateRing.basis: the power basis ofF[W]overF[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 #
@[inline, reducible]
abbrev
WeierstrassCurve.Affine.CoordinateRing
{R : Type u}
[CommRing R]
(W : WeierstrassCurve.Affine R)
:
Type u
The coordinate ring $R[W] := R[X, Y] / \langle W(X, Y) \rangle$ of W.
Equations
- W.CoordinateRing = AdjoinRoot W.polynomial
Instances For
@[inline, reducible]
abbrev
WeierstrassCurve.Affine.FunctionField
{R : Type u}
[CommRing R]
(W : WeierstrassCurve.Affine R)
:
Type u
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
- (_ : IsDomain W.CoordinateRing) = (_ : IsDomain (Polynomial (Polynomial R) ⧸ Ideal.span {W.polynomial}))
instance
WeierstrassCurve.Affine.CoordinateRing.instIsDomainCoordinateRing_of_Field
{F : Type u}
[Field F]
(W : WeierstrassCurve.Affine F)
:
IsDomain W.CoordinateRing
@[inline, reducible]
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)
:
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)
:
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
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
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
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' (_ : W.nonsingular x (W.negY x y))) * 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'
(_ : W.nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))))
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
noncomputable instance
WeierstrassCurve.Affine.CoordinateRing.instAlgebraCoordinateRing'
{R : Type u}
[CommRing R]
(W : WeierstrassCurve.Affine R)
:
Algebra R W.CoordinateRing
instance
WeierstrassCurve.Affine.CoordinateRing.instIsScalarTowerCoordinateRing
{R : Type u}
[CommRing R]
(W : WeierstrassCurve.Affine R)
:
IsScalarTower R (Polynomial R) W.CoordinateRing
Equations
- (_ : IsScalarTower R (Polynomial R) W.CoordinateRing) = (_ : IsScalarTower R (Polynomial R) (Polynomial (Polynomial R) ⧸ Ideal.span {W.polynomial}))
instance
WeierstrassCurve.Affine.CoordinateRing.instSubsingletonCoordinateRing
{R : Type u}
[CommRing R]
(W : WeierstrassCurve.Affine R)
[Subsingleton R]
:
Subsingleton W.CoordinateRing
Equations
- (_ : Subsingleton W.CoordinateRing) = (_ : Subsingleton W.CoordinateRing)
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
- One or more equations did not get rendered due to their size.
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' (_ : Polynomial.Monic W.polynomial)).gen ^ ↑n
@[simp]
theorem
WeierstrassCurve.Affine.CoordinateRing.basis_zero
{R : Type u}
[CommRing R]
(W : WeierstrassCurve.Affine R)
:
@[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)
:
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)
:
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)
:
Polynomial.degree
((Algebra.norm (Polynomial R)) (p • 1 + q • (WeierstrassCurve.Affine.CoordinateRing.mk W) Polynomial.X)) = max (2 • Polynomial.degree p) (2 • Polynomial.degree q + 3)
theorem
WeierstrassCurve.Affine.CoordinateRing.degree_norm_ne_one
{R : Type u}
[CommRing R]
{W : WeierstrassCurve.Affine R}
[IsDomain R]
(x : W.CoordinateRing)
:
Polynomial.degree ((Algebra.norm (Polynomial R)) x) ≠ 1
theorem
WeierstrassCurve.Affine.CoordinateRing.natDegree_norm_ne_one
{R : Type u}
[CommRing R]
{W : WeierstrassCurve.Affine R}
[IsDomain R]
(x : W.CoordinateRing)
:
Polynomial.natDegree ((Algebra.norm (Polynomial R)) x) ≠ 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 = WeierstrassCurve.Affine.Point.toClassFun a
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
- One or more equations did not get rendered due to their size.
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)
:
theorem
WeierstrassCurve.Affine.Point.add_left_neg
{F : Type u}
[Field F]
{W : WeierstrassCurve.Affine F}
(P : W.Point)
:
theorem
WeierstrassCurve.Affine.Point.neg_add_eq_zero
{F : Type u}
[Field F]
{W : WeierstrassCurve.Affine F}
(P : W.Point)
(Q : W.Point)
:
theorem
WeierstrassCurve.Affine.Point.toClass_eq_zero
{F : Type u}
[Field F]
{W : WeierstrassCurve.Affine F}
(P : W.Point)
:
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)
:
theorem
WeierstrassCurve.Affine.Point.add_assoc
{F : Type u}
[Field F]
{W : WeierstrassCurve.Affine F}
(P : W.Point)
(Q : W.Point)
(R : W.Point)
:
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 (_ : ∀ (P Q : W.Point), P + Q = Q + P)
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 (_ : E.toAffine.nonsingular x y)