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. This file also defines the negation and addition operations of the group law for this
type, and proves that they respect the Weierstrass equation and the nonsingular condition. The fact
that they form an abelian group is proven in Mathlib.AlgebraicGeometry.EllipticCurve.Group
.
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.
Note that most computational proofs follow from their analogous proofs for affine coordinates.
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.WeierstrassCurve.Projective.neg
: the negation operation on a point representative.WeierstrassCurve.Projective.negMap
: the negation operation on a point class.WeierstrassCurve.Projective.add
: the addition operation on a point representative.WeierstrassCurve.Projective.addMap
: the addition operation on a point class.WeierstrassCurve.Projective.Point
: a nonsingular rational point.WeierstrassCurve.Projective.Point.neg
: the negation operation on a nonsingular rational point.WeierstrassCurve.Projective.Point.add
: the addition operation on a nonsingular rational point.WeierstrassCurve.Projective.Point.toAffineAddEquiv
: the equivalence between the nonsingular rational points on a projective Weierstrass curve with those on an affine Weierstrass curve.
Main statements #
WeierstrassCurve.Projective.polynomial_relation
: Euler's homogeneous function theorem.WeierstrassCurve.Projective.nonsingular_neg
: negation preserves the nonsingular condition.WeierstrassCurve.Projective.nonsingular_add
: addition preserves the nonsingular condition.
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 $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]
Instances For
Negation on point representatives #
The negation of a point representative.
Equations
- W'.neg P = ![P 0, W'.negY P, P 2]
Instances For
The negation of a point class. If P
is a point representative,
then W'.negMap ⟦P⟧
is definitionally equivalent to W'.neg P
.
Equations
- W'.negMap P = Quotient.map W'.neg ⋯ P
Instances For
Addition on point representatives #
The addition of two point representatives.
Instances For
The addition of two point classes. If P
is a point representative,
then W.addMap ⟦P⟧ ⟦Q⟧
is definitionally equivalent to W.add P Q
.
Equations
- W'.addMap P Q = Quotient.map₂ W'.add ⋯ P Q
Instances For
Nonsingular rational points #
A nonsingular rational point on W'
.
- point : WeierstrassCurve.Projective.PointClass R
The point class underlying a nonsingular rational point on
W'
. - nonsingular : W'.NonsingularLift self.point
The nonsingular condition underlying a nonsingular rational point on
W'
.
Instances For
Equations
- WeierstrassCurve.Projective.Point.instZeroPoint = { zero := WeierstrassCurve.Projective.Point.mk ⋯ }
The map from a nonsingular rational point on a Weierstrass curve W'
in affine coordinates
to the corresponding nonsingular rational point on W'
in projective coordinates.
Equations
- WeierstrassCurve.Projective.Point.fromAffine WeierstrassCurve.Affine.Point.zero = 0
- WeierstrassCurve.Projective.Point.fromAffine (WeierstrassCurve.Affine.Point.some h) = WeierstrassCurve.Projective.Point.mk ⋯
Instances For
The negation of a nonsingular rational point on W
.
Given a nonsingular rational point P
on W
, use -P
instead of neg P
.
Equations
Instances For
Equations
- WeierstrassCurve.Projective.Point.instNegPoint = { neg := WeierstrassCurve.Projective.Point.neg }
The addition of two nonsingular rational points on W
.
Given two nonsingular rational points P
and Q
on W
, use P + Q
instead of add P Q
.
Equations
- P.add Q = WeierstrassCurve.Projective.Point.mk ⋯
Instances For
Equations
- WeierstrassCurve.Projective.Point.instAddPoint = { add := WeierstrassCurve.Projective.Point.add }
Equivalence with affine coordinates #
The map from a point representative that is nonsingular on a Weierstrass curve W
in projective
coordinates to the corresponding nonsingular rational point on W
in affine coordinates.
Equations
- WeierstrassCurve.Projective.Point.toAffine W P = if hP : W.Nonsingular P ∧ P 2 ≠ 0 then WeierstrassCurve.Affine.Point.some ⋯ else 0
Instances For
The map from a nonsingular rational point on a Weierstrass curve W
in projective coordinates
to the corresponding nonsingular rational point on W
in affine coordinates.
Equations
- P.toAffineLift = Quotient.lift (fun (x : Fin 3 → F) => WeierstrassCurve.Projective.Point.toAffine W x) ⋯ P.point
Instances For
The equivalence between the nonsingular rational points on a Weierstrass curve W
in Projective
coordinates with the nonsingular rational points on W
in affine coordinates.
Equations
- One or more equations did not get rendered due to their size.
Instances For
An abbreviation for WeierstrassCurve.Projective.Point.fromAffine
for dot notation.
Equations
- P.toProjective = WeierstrassCurve.Projective.Point.fromAffine P