Base change 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 f : R →+* R' be a ring homomorphism. The curve W.map f is elliptic, and its projective model E' = projModel (W.map f) over S' = Spec R' is the base change of E along Spec f, through the base change morphism WeierstrassCurve.projModelBaseChange W f : E' ⟶ E. This file shows that the Bosma–Lenstra addition morphism WeierstrassCurve.additionMorphism is compatible with base change: the addition morphism E' ×_{S'} E' ⟶ E' of W.map f followed by E' ⟶ E is the morphism E' ×_{S'} E' ⟶ E ×_S E induced by E' ⟶ E followed by the addition morphism E ×_S E ⟶ E of W.

The two composites are compared on the pieces of the chart cover WeierstrassCurve.additionCover of E' ×_{S'} E'. Such a piece is a pair of points of E', with homogeneous coordinates P and Q having a unit coordinate each, at which one of the two addition laws has a unit coordinate. The base change morphism does not change homogeneous coordinates (WeierstrassCurve.projModelPoint_projModelBaseChange), and both addition morphisms send the pair to the point whose homogeneous coordinates are the value of that law at P and Q.

Main results

• WeierstrassCurve.additionMorphism_projModelBaseChange: the addition morphism commutes with base change along any ring homomorphism.

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

The statement of additionMorphism_projModelBaseChange is adapted from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit c3415f32a313e19ace43e05479aeaa0d56ca287a, file projects/ModularCurves/ModularCurves/EllipticCurve/GroupLawConstruction.lean, declaration mulModelHom_map. Only the statement is taken from the source. The source defines the addition morphism of every elliptic curve by base change from the universal curve over a Jacobson domain (mulModelHomBC, file AdditionBaseChange.lean), so that its compatibility with base change follows from the uniqueness of a morphism into a fibre product. Here the addition morphism of each curve is glued from its own chart cover, so the compatibility is checked piece by piece, using WeierstrassCurve.lift_projModelPoint_additionMorphism_of_isUnit_addXYZ and WeierstrassCurve.lift_projModelPoint_additionMorphism_of_isUnit_dblAddXYZ.

@[simp]

theorem WeierstrassCurve.additionMorphism_projModelBaseChange {R : Type u} [CommRing R] (W : WeierstrassCurve R) {R' : Type u} [CommRing R'] (f : R →+* R') [W.IsElliptic] : CategoryTheory.CategoryStruct.comp (W.map f).additionMorphism (W.projModelBaseChange f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map (W.map f).projModelOver (W.map f).projModelOver W.projModelOver W.projModelOver (W.projModelBaseChange f) (W.projModelBaseChange f) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom f)) ⋯ ⋯) W.additionMorphism

The addition morphism commutes with base change. Let W be an elliptic Weierstrass curve over R and f : R →+* R' a ring homomorphism, and write E = projModel W over S = Spec R and E' = projModel (W.map f) over S' = Spec R'. The Bosma–Lenstra addition morphism E' ×_{S'} E' ⟶ E' of W.map f, followed by the base change morphism E' ⟶ E, is the morphism E' ×_{S'} E' ⟶ E ×_S E induced by the base change morphism on both factors, followed by the addition morphism E ×_S E ⟶ E of W.

@[simp]

theorem WeierstrassCurve.additionMorphism_projModelBaseChange_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) {R' : Type u} [CommRing R'] (f : R →+* R') [W.IsElliptic] {Z : AlgebraicGeometry.Scheme} (h : W.projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp (W.map f).additionMorphism (CategoryTheory.CategoryStruct.comp (W.projModelBaseChange f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map (W.map f).projModelOver (W.map f).projModelOver W.projModelOver W.projModelOver (W.projModelBaseChange f) (W.projModelBaseChange f) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom f)) ⋯ ⋯) (CategoryTheory.CategoryStruct.comp W.additionMorphism h)

The addition morphism commutes with base change. Let W be an elliptic Weierstrass curve over R and f : R →+* R' a ring homomorphism, and write E = projModel W over S = Spec R and E' = projModel (W.map f) over S' = Spec R'. The Bosma–Lenstra addition morphism E' ×_{S'} E' ⟶ E' of W.map f, followed by the base change morphism E' ⟶ E, is the morphism E' ×_{S'} E' ⟶ E ×_S E induced by the base change morphism on both factors, followed by the addition morphism E ×_S E ⟶ E of W.