The Bosma–Lenstra addition morphism on points #
Let W be an elliptic Weierstrass curve over a commutative ring R, let E = projModel W be its
projective model and let E ×_{Spec R} E ⟶ E be the Bosma–Lenstra addition morphism
WeierstrassCurve.additionMorphism. This file computes the addition morphism on points.
Let g : R →+* A be a ring homomorphism and let P and Q be solutions of the projective
Weierstrass equation of W.map g with unit coordinates Pᵢ and Qⱼ, the homogeneous coordinates
of the A-points projModelPoint W g P and projModelPoint W g Q of E. If some coordinate of
the addition law addXYZ P Q (resp. dblAddXYZ P Q) is a unit, then the addition morphism sends
the pair of these points to the point with homogeneous coordinates addXYZ P Q
(resp. dblAddXYZ P Q).
When g : R →+* K goes to a field, P and Q are nonsingular, since W is elliptic. One of the
two laws then does not vanish at P and Q, and its value represents their sum add P Q in
Mathlib's projective group law on W.map g: the addition morphism sends the pair of K-points to
the point with homogeneous coordinates add P Q. For a curve over a field K, through the
identification WeierstrassCurve.projModelPointsEquiv of the sections of E ⟶ Spec K with the
points W.toAffine.Point of W, the addition morphism is the addition of these points.
Main results #
WeierstrassCurve.lift_projModelPoint_additionMorphism_of_isUnit_addXYZandWeierstrassCurve.lift_projModelPoint_additionMorphism_of_isUnit_dblAddXYZ: the addition morphism sends the pair of points with homogeneous coordinatesPandQto the point with homogeneous coordinatesaddXYZ P Q(resp.dblAddXYZ P Q), when one of its coordinates is a unit.WeierstrassCurve.lift_projModelPoint_additionMorphism_eq_add: forg : R →+* Kto a field, the addition morphism sends the pair ofK-points with homogeneous coordinatesPandQto the point with homogeneous coordinates their sumadd P Q.WeierstrassCurve.projModelPointsEquiv_lift_additionMorphism: over a fieldK, the addition morphism agrees with the addition of the pointsW.toAffine.Pointon the sections ofprojModel W ⟶ Spec K.
References #
- W. Bosma and H. W. Lenstra, Jr., Complete systems of two addition laws for elliptic curves, J. Number Theory 53 (1995), 229–240.
Provenance #
Adapted from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit
c3415f32a313e19ace43e05479aeaa0d56ca287a, file
projects/ModularCurves/ModularCurves/EllipticCurve/AdditionSpecPoints.lean:
SpecPoint.factors_blOpen, within lift_projModelPoint_additionMorphism_of_isUnit_addXYZ and
lift_projModelPoint_additionMorphism_of_isUnit_dblAddXYZ; SpecPoint.arm_Z, SpecPoint.arm_Y
and mulModelHom_specPoints_atlas, within lift_projModelPoint_additionMorphism_eq_add; and
mulModelHom_specPoints, as lift_projModelPoint_additionMorphism_eq_add and
projModelPointsEquiv_lift_additionMorphism.
The source works with the universal elliptic curve over a Jacobson domain, factors a field point of
E ×_{Spec R} E through the open set where one of the two laws is regular, splits the products of
charts into its Z- and Y-families, and transports the result to every curve by base change. It
states the agreement for the K-points of E over every field K that is an R-algebra. Here a
pair of points with unit coordinates, over any ring homomorphism, is factored directly through a
piece of the chart cover WeierstrassCurve.additionCover. The agreement with the group law is
stated on homogeneous coordinates for every g : R →+* K to a field, and on W.toAffine.Point
for a curve over the field K itself.
The addition morphism on points, through the law addXYZ. Let P and Q be solutions
of the projective Weierstrass equation of W.map g, for a ring homomorphism g : R →+* A, with
unit coordinates Pᵢ and Qⱼ. If the coordinate of index m of the addition law addXYZ P Q
attached to the line Z = 0 is a unit, then the addition morphism E ×_{Spec R} E ⟶ E sends the
pair of A-points with homogeneous coordinates P and Q to the A-point with homogeneous
coordinates addXYZ P Q.
The addition morphism on points, through the law dblAddXYZ. Let P and Q be solutions
of the projective Weierstrass equation of W.map g, for a ring homomorphism g : R →+* A, with
unit coordinates Pᵢ and Qⱼ. If the coordinate of index m of the addition law dblAddXYZ P Q
attached to the line Y = 0 is a unit, then the addition morphism E ×_{Spec R} E ⟶ E sends the
pair of A-points with homogeneous coordinates P and Q to the A-point with homogeneous
coordinates dblAddXYZ P Q.
The addition morphism on field-valued points. Let g : R →+* K be a ring homomorphism to a
field, and let P and Q be solutions of the projective Weierstrass equation of W.map g with
unit coordinates Pᵢ and Qⱼ; as W is elliptic, they are nonsingular. Then the addition morphism
E ×_{Spec R} E ⟶ E sends the pair of K-points of E with homogeneous coordinates P and Q to
the K-point with homogeneous coordinates their sum add P Q in Mathlib's projective group law on
W.map g, read on any chart D₊(Xₘ) on which it has a unit coordinate.
The addition morphism on field points. Let W be an elliptic Weierstrass curve over a
field K and let E = projModel W. Through the identification projModelPointsEquiv of the
sections of the structure morphism E ⟶ Spec K with the points W.toAffine.Point of W, the
Bosma–Lenstra addition morphism E ×_{Spec K} E ⟶ E is the addition of W.toAffine.Point: it
sends the pair of sections (x, y) to the section corresponding to the sum of the points
corresponding to x and y. For points over an arbitrary homomorphism g : R →+* K to a field,
given by homogeneous coordinates, see lift_projModelPoint_additionMorphism_eq_add.