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 and in
Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.
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.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.
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 an affine 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 of an affine Weierstrass curve in terms of the power basis.WeierstrassCurve.Affine.Point.instAddCommGroup: the type of nonsingular rational points on an affine Weierstrass curve forms an abelian group under addition.WeierstrassCurve.Jacobian.Point.instAddCommGroup: the type of nonsingular rational points on a Jacobian Weierstrass curve forms an abelian group under addition.
References #
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)
:
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
@[reducible, inline]
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
The coordinate ring as an R[X]-algebra #
noncomputable instance
WeierstrassCurve.Affine.CoordinateRing.instAlgebra
{R : Type u}
[CommRing R]
(W : WeierstrassCurve.Affine R)
:
Algebra R W.CoordinateRing
noncomputable instance
WeierstrassCurve.Affine.CoordinateRing.instAlgebraPolynomial
{R : Type u}
[CommRing R]
(W : WeierstrassCurve.Affine R)
:
Algebra (Polynomial R) W.CoordinateRing
instance
WeierstrassCurve.Affine.CoordinateRing.instIsScalarTowerPolynomial
{R : Type u}
[CommRing R]
(W : WeierstrassCurve.Affine R)
:
IsScalarTower R (Polynomial R) W.CoordinateRing
Equations
- ⋯ = ⋯
instance
WeierstrassCurve.Affine.CoordinateRing.instSubsingleton
{R : Type u}
[CommRing R]
(W : WeierstrassCurve.Affine R)
[Subsingleton R]
:
Subsingleton 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
The natural ring homomorphism mapping an element of R[X][Y] to an element of R[W].
Equations
- WeierstrassCurve.Affine.CoordinateRing.mk W = AdjoinRoot.mk W.polynomial
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)
:
@[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
noncomputable def
WeierstrassCurve.Affine.CoordinateRing.map
{R : Type u}
{S : Type v}
[CommRing R]
[CommRing S]
(W : WeierstrassCurve.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.
Instances For
theorem
WeierstrassCurve.Affine.CoordinateRing.map_mk
{R : Type u}
{S : Type v}
[CommRing R]
[CommRing S]
(W : WeierstrassCurve.Affine R)
(f : R →+* S)
(x : Polynomial (Polynomial R))
:
theorem
WeierstrassCurve.Affine.CoordinateRing.map_smul
{R : Type u}
{S : Type v}
[CommRing R]
[CommRing S]
{W : WeierstrassCurve.Affine R}
(f : R →+* S)
(x : Polynomial R)
(y : W.CoordinateRing)
:
(WeierstrassCurve.Affine.CoordinateRing.map W f) (x • y) = Polynomial.map f x • (WeierstrassCurve.Affine.CoordinateRing.map W f) y
theorem
WeierstrassCurve.Affine.CoordinateRing.map_injective
{R : Type u}
{S : Type v}
[CommRing R]
[CommRing S]
(W : WeierstrassCurve.Affine R)
{f : R →+* S}
(hf : Function.Injective ⇑f)
:
instance
WeierstrassCurve.Affine.CoordinateRing.instIsDomain
{R : Type u}
[CommRing R]
(W : WeierstrassCurve.Affine R)
[IsDomain R]
:
IsDomain W.CoordinateRing
Equations
- ⋯ = ⋯
Ideals in the coordinate ring over a ring #
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 (WeierstrassCurve.Affine.linePolynomial x y L)) * (W.negPolynomial - Polynomial.C (WeierstrassCurve.Affine.linePolynomial x 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 (WeierstrassCurve.Affine.linePolynomial x 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 (WeierstrassCurve.Affine.linePolynomial x₁ y₁ L))} ⊔ WeierstrassCurve.Affine.CoordinateRing.XIdeal W (W.addX x₁ x₂ L)
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
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₂
(WeierstrassCurve.Affine.linePolynomial x₁ 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 (WeierstrassCurve.Affine.linePolynomial x₁ 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' ⋯)
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)
:
((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.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
noncomputable instance
WeierstrassCurve.Affine.Point.instAddCommGroup
{F : Type u}
[Field F]
{W : WeierstrassCurve.Affine F}
:
AddCommGroup W.Point
Equations
- WeierstrassCurve.Affine.Point.instAddCommGroup = AddCommGroup.mk ⋯
Weierstrass curves in Jacobian coordinates #
noncomputable instance
WeierstrassCurve.Jacobian.Point.instAddCommGroup
{F : Type u}
[Field F]
{W : WeierstrassCurve.Jacobian F}
:
AddCommGroup W.Point
Equations
- WeierstrassCurve.Jacobian.Point.instAddCommGroup = 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.