The inverse law for the Bosma–Lenstra addition morphism

Let W be an elliptic Weierstrass curve over a commutative ring R, let E = projModel W be its projective model over S = Spec R, with structure morphism π : E ⟶ S and zero section 0 : S ⟶ E, and let E ×_S E ⟶ E be the Bosma–Lenstra addition morphism WeierstrassCurve.additionMorphism. This file shows that the negation morphism WeierstrassCurve.projModelNeg is a right inverse for it: the morphism E ⟶ E ×_S E with components the identity and negation, followed by the addition morphism, is π ≫ 0.

Over a Noetherian integral domain R, the scheme E is integral, hence reduced, and it is separated, so two morphisms E ⟶ E are equal as soon as they agree on the points of E with values in its residue fields. Such a point has homogeneous coordinates P over a field, negation sends it to the point with homogeneous coordinates neg P, and the addition morphism sends the pair to the point with homogeneous coordinates add P (neg P). This represents the point at infinity (WeierstrassCurve.Projective.add_neg_equiv), which is the value of π ≫ 0.

An elliptic Weierstrass curve over an arbitrary commutative ring is the base change of one over a Noetherian integral domain (WeierstrassCurve.exists_map_eq_of_isElliptic), and the inverse law passes to a base change W.map f, since the addition morphism, negation and the zero section all commute with base change.

Main results

• WeierstrassCurve.additionMorphism_right_inv: the sum of the identity and negation of projModel W is the structure morphism followed by the zero section.

References

• W. Bosma and H. W. Lenstra, Jr., Complete systems of two addition laws for elliptic curves, J. Number Theory 53 (1995), 229–240.
• The argument is the one of WeierstrassCurve.additionMorphism_comm, whose provenance records its adaptation from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0), file projects/ModularCurves/ModularCurves/EllipticCurve/GroupLawAxioms.lean at commit c3415f32a313e19ace43e05479aeaa0d56ca287a.

@[simp]

theorem WeierstrassCurve.additionMorphism_right_inv {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.id W.projModel) W.projModelNeg ⋯) W.additionMorphism = CategoryTheory.CategoryStruct.comp W.projModelOver W.projModelZero

The inverse law for the addition morphism. Let W be an elliptic Weierstrass curve over a commutative ring R, and write E = projModel W and S = Spec R. The morphism E ⟶ E ×_S E with components the identity and the negation morphism projModelNeg, followed by the Bosma–Lenstra addition morphism E ×_S E ⟶ E, is the structure morphism E ⟶ S followed by the zero section: every point plus its negation is zero.

@[simp]

theorem WeierstrassCurve.additionMorphism_right_inv_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {Z : AlgebraicGeometry.Scheme} (h : W.projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.id W.projModel) W.projModelNeg ⋯) (CategoryTheory.CategoryStruct.comp W.additionMorphism h) = CategoryTheory.CategoryStruct.comp W.projModelOver (CategoryTheory.CategoryStruct.comp W.projModelZero h)

The inverse law for the addition morphism. Let W be an elliptic Weierstrass curve over a commutative ring R, and write E = projModel W and S = Spec R. The morphism E ⟶ E ×_S E with components the identity and the negation morphism projModelNeg, followed by the Bosma–Lenstra addition morphism E ×_S E ⟶ E, is the structure morphism E ⟶ S followed by the zero section: every point plus its negation is zero.