Commutativity of 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, and let E ×_S E ⟶ E be the Bosma–Lenstra addition morphism WeierstrassCurve.additionMorphism. This file shows that the addition morphism is commutative: it is unchanged by composition with the isomorphism of E ×_S E swapping the two factors.

Over a Noetherian integral domain R, the fibre product E ×_S E is reduced and E is a separated scheme, so two morphisms E ×_S E ⟶ E are equal as soon as they agree on the points of E ×_S E with values in its residue fields. Such a point is a pair of points of E with homogeneous coordinates P and Q over a field. The addition morphism sends it to the point with homogeneous coordinates the sum add P Q of Mathlib's addition of point representatives, and add P Q and add Q P represent the same point (WeierstrassCurve.Projective.add_comm_equiv).

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). Commutativity passes to a base change W.map f, because projModel (W.map f) is the base change of projModel W (WeierstrassCurve.isPullback_projModelBaseChange) and the addition morphism commutes with base change (WeierstrassCurve.additionMorphism_projModelBaseChange).

Main results

• WeierstrassCurve.additionMorphism_comm: the addition morphism of an elliptic Weierstrass curve over a commutative ring is commutative.

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

additionMorphism_comm is adapted from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit c3415f32a313e19ace43e05479aeaa0d56ca287a, file projects/ModularCurves/ModularCurves/EllipticCurve/GroupLawAxioms.lean, declarations mulModelHom_comm_atlas, commutativity over the universal base, and mulModelHom_comm, its transport to every elliptic Weierstrass curve. The other files named below lie in the same directory.

The source proves commutativity over one ring, the copy WeierstrassAtlasRingU in Type u of its universal ring (file AdditionBaseChange.lean), by its extensionality principle hom_ext_of_forall_specPoint for field-valued points (file PointsDictionary.lean). It evaluates the multiplication on a pair of points over a field with mulModelHom_specPoints (file AdditionSpecPoints.lean), and concludes from the commutativity of WeierstrassCurve.Affine.Point through its dictionary projModelPointsEquiv (file PointsDictionary.lean). Here the same argument is carried out over every Noetherian integral domain, with Mathlib's AlgebraicGeometry.ext_of_fromSpecResidueField_eq in place of hom_ext_of_forall_specPoint, on points given by homogeneous coordinates (WeierstrassCurve.exists_eq_lift_projModelPoint and WeierstrassCurve.lift_projModelPoint_additionMorphism_eq_add), and concludes from WeierstrassCurve.Projective.add_comm_equiv, which is not stated in the source. The transport to every curve follows the source, with the reduction WeierstrassCurve.exists_map_eq_of_isElliptic in place of the source's named universal curve universalWeierstrassLocU over WeierstrassAtlasRingU.

@[simp]

theorem WeierstrassCurve.additionMorphism_comm {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry W.projModelOver W.projModelOver).hom W.additionMorphism = W.additionMorphism

The addition morphism is commutative. Let W be an elliptic Weierstrass curve over a commutative ring R, and write E = projModel W and S = Spec R. The Bosma–Lenstra addition morphism E ×_S E ⟶ E is unchanged by composition with the isomorphism pullbackSymmetry of E ×_S E that swaps the two factors. This isomorphism is the underlying morphism of the braiding of the cartesian monoidal category Over S (CategoryTheory.Over.braiding_hom_left).

@[simp]

theorem WeierstrassCurve.additionMorphism_comm_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {Z : AlgebraicGeometry.Scheme} (h : W.projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry W.projModelOver W.projModelOver).hom (CategoryTheory.CategoryStruct.comp W.additionMorphism h) = CategoryTheory.CategoryStruct.comp W.additionMorphism h

The addition morphism is commutative. Let W be an elliptic Weierstrass curve over a commutative ring R, and write E = projModel W and S = Spec R. The Bosma–Lenstra addition morphism E ×_S E ⟶ E is unchanged by composition with the isomorphism pullbackSymmetry of E ×_S E that swaps the two factors. This isomorphism is the underlying morphism of the braiding of the cartesian monoidal category Over S (CategoryTheory.Over.braiding_hom_left).