Associativity 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 associative:
the two morphisms (E ×_S E) ×_S E ⟶ E that add the three components of the triple fibre
product, as (a + b) + c and as a + (b + c), are equal.
Over a Noetherian integral domain R, the triple fibre product (E ×_S E) ×_S E is reduced and
E is a separated scheme, so two morphisms (E ×_S E) ×_S E ⟶ E are equal as soon as they agree
on the points of (E ×_S E) ×_S E with values in its residue fields. Such a point is a triple of
points of E with homogeneous coordinates P, Q and T over a field. The addition morphism
sends a pair of points given by homogeneous coordinates to the point with homogeneous coordinates
their sum for Mathlib's addition of point representatives, so the two morphisms send the triple to
the points with homogeneous coordinates add (add P Q) T and add P (add Q T). These represent
the same point (WeierstrassCurve.Projective.add_assoc_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). Associativity 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): the base change morphism turns
the two sums of the three projections of the triple fibre product of projModel (W.map f) into
the two sums of their composites with the base change morphism, which are three morphisms to
projModel W over the same morphism to S.
Main results #
WeierstrassCurve.additionMorphism_assoc: the addition morphism of an elliptic Weierstrass curve over a commutative ring is associative.
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_assoc is adapted from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at
commit c3415f32a313e19ace43e05479aeaa0d56ca287a, file
projects/ModularCurves/ModularCurves/EllipticCurve/GroupLawAxioms.lean, declarations
mulModelHom_assoc_specPoints, associativity on three points with values in a field,
mulOver_assoc_atlas, associativity over the universal base, and mulOver_assoc_of_map,
mulOver_assoc_of_eq and mulOver_assoc, its transport to every elliptic Weierstrass curve. The
other files named below lie in the same directory.
The source states associativity as an equation of morphisms of Over (Spec R), for its morphism
mulOver (file GroupLawConstruction.lean), with the whiskerings and the associator of the
cartesian monoidal structure:
(mulOver W ▷ modelOver W) ≫ mulOver W = (α_ (modelOver W) (modelOver W) (modelOver W)).hom ≫ (modelOver W ◁ mulOver W) ≫ mulOver W.
Here it is an equation of morphisms of schemes (E ×_S E) ×_S E ⟶ E, for the two morphisms
(E ×_S E) ×_S E ⟶ E ×_S E built with pullback.lift from the projections and the addition
morphism. The source also has the pullback.lift form of the equation, for three morphisms from
a scheme to E over the same morphism to the base, as its private theorem model_mul_assoc_lift
(file GroupLawDescent.lean), deduced from Mathlib's CategoryTheory.MonObj.lift_lift_assoc for
its group object.
The source proves associativity 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 pairs of points over a field with mulModelHom_specPoints (file
AdditionSpecPoints.lean), and concludes from add_assoc in WeierstrassCurve.Affine.Point
through its dictionary projModelPointsEquiv (file PointsDictionary.lean). Here the same
argument is carried out for every curve whose triple fibre product is reduced, in particular 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, WeierstrassCurve.exists_eq_projModelPoint and
WeierstrassCurve.lift_projModelPoint_additionMorphism_eq_add), and concludes from
WeierstrassCurve.Projective.add_assoc_equiv, the form for point representatives of add_assoc in
Mathlib's WeierstrassCurve.Projective.Point.
For the transport, the source constructs the morphism of triple fibre products induced by the
base change morphism (BaseChangeOf.tripleMap), and shows that the two sides of the associativity
equation commute with it: the right whiskering of the multiplication within
mulOver_assoc_of_map, and the associator followed by the left whiskering in
BaseChangeOf.assoc_whiskerLeft, through BaseChangeOf.assocSnd_pairMap and the other private
BaseChangeOf lemmas of the file. Here that morphism is not constructed: associativity for W is
applied to the composites with the base change morphism of the three projections of the triple
fibre product of projModel (W.map f). The reduction
WeierstrassCurve.exists_map_eq_of_isElliptic takes the place of the source's named universal
curve universalWeierstrassLocU over WeierstrassAtlasRingU. The source's mulModelHom_lift_π,
that the sum of two morphisms to E lies over the same morphism to the base as the first of
them, is written here in the proof arguments of pullback.lift, with
WeierstrassCurve.additionMorphism_projModelOver.
The addition morphism is associative. Let W be an elliptic Weierstrass curve over a
commutative ring R, and write E = projModel W and S = Spec R, with Bosma–Lenstra addition
morphism μ : E ×_S E ⟶ E. Write fst and snd for the projections of the triple fibre product
(E ×_S E) ×_S E to E ×_S E and to E, and for those of E ×_S E. The morphism
(E ×_S E) ×_S E ⟶ E ×_S E with components fst ≫ μ and snd, followed by μ, is equal to the
morphism with components fst ≫ fst and (fst ≫ snd, snd) ≫ μ, followed by μ: adding the first
two components and then the third is adding the first component and the sum of the last two. The
two morphisms to E ×_S E are the underlying morphisms of the pairs
CartesianMonoidalCategory.lift of the corresponding morphisms of the cartesian monoidal category
Over S (CategoryTheory.Over.lift_left), and the equation is that of
CategoryTheory.MonObj.lift_lift_assoc for the three projections fst ≫ fst, fst ≫ snd and
snd, the first two of which are the components of fst.