The Bosma–Lenstra addition morphism on `E ×_S E` #

Let W be an elliptic Weierstrass curve over a commutative ring R, let E = projModel W be its projective model and let S = Spec R. The Bosma–Lenstra chart cover WeierstrassCurve.additionCover of E ×_S E has pieces Spec (Localization.Away (chartPairLaw W i j k)), on which the addition law selected by k has a unit coordinate and defines a morphism WeierstrassCurve.additionOnPiece W i j k to E. This file shows that these morphisms agree, as morphisms of schemes, on the overlaps of the pieces, and glues them to the addition morphism E ×_S E ⟶ E over S.

Main definitions #

WeierstrassCurve.additionMorphism W: the addition morphism E ×_S E ⟶ E.

Main results #

WeierstrassCurve.fst_additionOnPiece_eq_snd_additionOnPiece: the addition morphisms on two pieces of the chart cover agree on their overlap.
WeierstrassCurve.SpecMap_chartPairι_additionMorphism: on each piece of the chart cover, the addition morphism is additionOnPiece.
WeierstrassCurve.additionMorphism_projModelOver: the addition morphism lies over S.

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, directory projects/ModularCurves/ModularCurves/EllipticCurve/:

from AdditionChartOverlap.lean: pieceMorOfTriple_agree and pieceMorOfTriple_cross_agree, within fst_additionOnPiece_eq_snd_additionOnPiece;
from AdditionChartGlue.lean: chartHomOfTriple_lawOne_eq_lawTwo, within fst_additionOnPiece_eq_snd_additionOnPiece;
from AdditionChartGlobal.lean: addOn_agree and blCoverMor_agree, within fst_additionOnPiece_eq_snd_additionOnPiece; mulModelHom, as additionMorphism; blOpenZ_ι_mulModelHom and blOpenY_ι_mulModelHom, as SpecMap_chartPairι_additionMorphism; and mulModelHom_projModelπ, as additionMorphism_projModelOver.

The source works over a Jacobson domain, on the four products of the Y- and Z-charts, whose rings are then domains, and glues each law on the open where it is regular before gluing the two laws. Here the base ring is arbitrary, all nine products of two charts are used, and the pieces of both laws are glued in one step over the whole of E ×_S E.

source

theorem WeierstrassCurve.fst_additionOnPiece_eq_snd_additionOnPiece {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] (a b : W.additionCover.I₀) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (W.additionCover.f a) (W.additionCover.f b)) (W.additionOnPiece a.1.1 a.1.2 a.2) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (W.additionCover.f a) (W.additionCover.f b)) (W.additionOnPiece b.1.1 b.1.2 b.2)

The Bosma–Lenstra addition morphisms on the pieces of the chart cover additionCover W of E ×_S E agree on overlaps: for any two pieces a and b, the composites of additionOnPiece on a and on b with the two projections from the fibre product of the pieces over E ×_S E are equal. This is the compatibility condition of Scheme.Cover.glueMorphisms.

source

noncomputable def WeierstrassCurve.additionMorphism {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] :

CategoryTheory.Limits.pullback W.projModelOver W.projModelOver ⟶ W.projModel

The Bosma–Lenstra addition morphism E ×_S E ⟶ E of an elliptic Weierstrass curve W over R, for E = projModel W and S = Spec R: the morphism whose restriction to each piece of the chart cover additionCover W is the addition morphism additionOnPiece on that piece (SpecMap_chartPairι_additionMorphism). It lies over S (additionMorphism_projModelOver).

Equations

W.additionMorphism = AlgebraicGeometry.Scheme.Cover.glueMorphisms W.additionCover.openCover (fun (a : W.additionCover.openCover.I₀) => W.additionOnPiece a.1.1 a.1.2 a.2) ⋯

Instances For

source

@[simp]

theorem WeierstrassCurve.SpecMap_chartPairι_additionMorphism {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] (i j : Fin 3) (k : Fin 3 ⊕ Fin 3) :

CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap (TensorProduct R (W.toProjective.ChartRing i) (W.toProjective.ChartRing j)) (Localization.Away (W.chartPairLaw i j k))))) (CategoryTheory.CategoryStruct.comp (W.chartPairι i j) W.additionMorphism) = W.additionOnPiece i j k

On the piece Spec (Localization.Away (chartPairLaw W i j k)) of the chart cover additionCover W, the addition morphism E ×_S E ⟶ E is the addition morphism additionOnPiece W i j k of that piece.

source

@[simp]