Projective coordinates for Weierstrass curves #
This file defines the type of points on a Weierstrass curve as a tuple, consisting of an equivalence class of triples up to scaling by a unit, satisfying a Weierstrass equation with a nonsingular condition.
Mathematical background #
Let W
be a Weierstrass curve over a field F
. A point on the projective plane is an equivalence
class of triples $[x:y:z]$ with coordinates in F
such that $(x, y, z) \sim (x', y', z')$ precisely
if there is some unit u
of F
such that $(x, y, z) = (ux', uy', uz')$, with an extra condition
that $(x, y, z) \ne (0, 0, 0)$. As described in Mathlib.AlgebraicGeometry.EllipticCurve.Affine
, a
rational point is a point on the projective plane satisfying a homogeneous Weierstrass equation, and
being nonsingular means the partial derivatives $W_X(X, Y, Z)$, $W_Y(X, Y, Z)$, and $W_Z(X, Y, Z)$
do not vanish simultaneously. Note that the vanishing of the Weierstrass equation and its partial
derivatives are independent of the representative for $[x:y:z]$, and the nonsingularity condition
already implies that $(x, y, z) \ne (0, 0, 0)$, so a nonsingular rational point on W
can simply be
given by a tuple consisting of $[x:y:z]$ and the nonsingular condition on any representative.
As in Mathlib.AlgebraicGeometry.EllipticCurve.Affine
, the set of nonsingular rational points forms
an abelian group under the same secant-and-tangent process, but the polynomials involved are
homogeneous, and any instances of division become multiplication in the $Z$-coordinate.
Main definitions #
WeierstrassCurve.Projective.PointClass
: the equivalence class of a point representative.WeierstrassCurve.Projective.toAffine
: the Weierstrass curve in affine coordinates.WeierstrassCurve.Projective.Nonsingular
: the nonsingular condition on a point representative.WeierstrassCurve.Projective.NonsingularLift
: the nonsingular condition on a point class.
Main statements #
WeierstrassCurve.Projective.polynomial_relation
: Euler's homogeneous function theorem.
Implementation notes #
A point representative is implemented as a term P
of type Fin 3 → R
, which allows for the vector
notation ![x, y, z]
. However, P
is not definitionally equivalent to the expanded vector
![P x, P y, P z]
, so the lemmas fin3_def
and fin3_def_ext
can be used to convert between the
two forms. The equivalence of two point representatives P
and Q
is implemented as an equivalence
of orbits of the action of Rˣ
, or equivalently that there is some unit u
of R
such that
P = u • Q
. However, u • Q
is not definitionally equal to ![u * Q x, u * Q y, u * Q z]
, so the
lemmas smul_fin3
and smul_fin3_ext
can be used to convert between the two forms.
References #
J Silverman, The Arithmetic of Elliptic Curves
Tags #
elliptic curve, rational point, projective coordinates
Weierstrass curves #
An abbreviation for a Weierstrass curve in projective coordinates.
Equations
Instances For
The coercion to a Weierstrass curve in projective coordinates.
Equations
- W.toProjective = W
Instances For
Projective coordinates #
The equivalence setoid for a point representative.
Equations
- WeierstrassCurve.Projective.instSetoidPoint = MulAction.orbitRel Rˣ (Fin 3 → R)
Instances For
The equivalence class of a point representative.
Equations
Instances For
The coercion to a Weierstrass curve in affine coordinates.
Equations
- W'.toAffine = W'
Instances For
Weierstrass equations #
The polynomial $W(X, Y, Z) := Y^2Z + a_1XYZ + a_3YZ^2 - (X^3 + a_2X^2Z + a_4XZ^2 + a_6Z^3)$
associated to a Weierstrass curve W'
over R
. This is represented as a term of type
MvPolynomial (Fin 3) R
, where X 0
, X 1
, and X 2
represent $X$, $Y$, and $Z$ respectively.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The proposition that a point representative $(x, y, z)$ lies in W'
.
In other words, $W(x, y, z) = 0$.
Equations
- W'.Equation P = ((MvPolynomial.eval P) W'.polynomial = 0)
Instances For
Nonsingular Weierstrass equations #
The partial derivative $W_X(X, Y, Z)$ of $W(X, Y, Z)$ with respect to $X$.
Equations
- W'.polynomialX = (MvPolynomial.pderiv 0) W'.polynomial
Instances For
The partial derivative $W_Y(X, Y, Z)$ of $W(X, Y, Z)$ with respect to $Y$.
Equations
- W'.polynomialY = (MvPolynomial.pderiv 1) W'.polynomial
Instances For
The partial derivative $W_Z(X, Y, Z)$ of $W(X, Y, Z)$ with respect to $Z$.
Equations
- W'.polynomialZ = (MvPolynomial.pderiv 2) W'.polynomial
Instances For
Euler's homogeneous function theorem.
The proposition that a point representative $(x, y, z)$ in W'
is nonsingular.
In other words, either $W_X(x, y, z) \ne 0$, $W_Y(x, y, z) \ne 0$, or $W_Z(x, y, z) \ne 0$.
Note that this definition is only mathematically accurate for fields.
Equations
- W'.Nonsingular P = (W'.Equation P ∧ ((MvPolynomial.eval P) W'.polynomialX ≠ 0 ∨ (MvPolynomial.eval P) W'.polynomialY ≠ 0 ∨ (MvPolynomial.eval P) W'.polynomialZ ≠ 0))
Instances For
The proposition that a point class on W'
is nonsingular. If P
is a point representative,
then W.NonsingularLift ⟦P⟧
is definitionally equivalent to W.Nonsingular P
.
Equations
- W'.NonsingularLift P = Quotient.lift W'.Nonsingular ⋯ P
Instances For
Alias of WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero
.
Alias of WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero
.
Alias of WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero
.
Negation formulae #
Doubling formulae #
The unit associated to the doubling of a 2-torsion point P
.
More specifically, the unit u
such that W.add P P = u • ![0, 1, 0]
where P = W.neg P
.
Equations
- W.dblU P = (MvPolynomial.eval P) W.polynomialX ^ 3 / P 2 ^ 2
Instances For
The $Z$-coordinate of a representative of 2 • P
for a point P
.
Instances For
The $X$-coordinate of a representative of 2 • P
for a point P
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The $Y$-coordinate of a representative of -(2 • P)
for a point P
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The $Y$-coordinate of a representative of 2 • P
for a point P
.
Equations
- W'.dblY P = W'.negY ![W'.dblX P, W'.negDblY P, W'.dblZ P]
Instances For
The coordinates of a representative of 2 • P
for a point P
.
Equations
- W'.dblXYZ P = ![W'.dblX P, W'.dblY P, W'.dblZ P]
Instances For
Addition formulae #
The unit associated to the addition of a non-2-torsion point P
with its negation.
More specifically, the unit u
such that W.add P Q = u • ![0, 1, 0]
where P x / P z = Q x / Q z
but P ≠ W.neg P
.
Instances For
The $Z$-coordinate of a representative of P + Q
for two distinct points P
and Q
.
Note that this returns the value 0 if the representatives of P
and Q
are equal.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The $X$-coordinate of a representative of P + Q
for two distinct points P
and Q
.
Note that this returns the value 0 if the representatives of P
and Q
are equal.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The $Y$-coordinate of a representative of -(P + Q)
for two distinct points P
and Q
.
Note that this returns the value 0 if the representatives of P
and Q
are equal.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The $Y$-coordinate of a representative of P + Q
for two distinct points P
and Q
.
Note that this returns the value 0 if the representatives of P
and Q
are equal.
Equations
- W'.addY P Q = W'.negY ![W'.addX P Q, W'.negAddY P Q, W'.addZ P Q]
Instances For
The coordinates of a representative of P + Q
for two distinct points P
and Q
.
Note that this returns the value ![0, 0, 0]
if the representatives of P
and Q
are equal.
Equations
- W'.addXYZ P Q = ![W'.addX P Q, W'.addY P Q, W'.addZ P Q]