The addition morphism commutes with pointed cartesian morphisms of Weierstrass models

Let W and W' be elliptic Weierstrass curves over commutative rings R and R'. This file shows that the Bosma–Lenstra addition morphisms E ×_S E ⟶ E of their projective models are compatible with every morphism F : projModel W ⟶ projModel W' that carries the zero section to the zero section and makes projModel W the base change of projModel W' along a morphism ψ : Spec R ⟶ Spec R'. No hypothesis relates W to W': the morphism F alone determines the comparison.

This is what makes the addition morphism independent of the local Weierstrass equation chosen for an elliptic curve over a scheme: two local models over the same affine open differ by a pointed isomorphism over the base, and the restriction of a local model to a smaller affine open is a pointed cartesian morphism.

Over the same base, a pointed isomorphism is induced by a change of variables (WeierstrassCurve.existsUnique_eq_eqToHom_comp_projModelVariableChangeIso_hom), and the addition morphism commutes with those (WeierstrassCurve.additionMorphism_projModelVariableChangeIso_hom). In general, F factors as a pointed isomorphism projModel W ≅ projModel (W'.map φ) over Spec R, with Spec φ = ψ, followed by the base change morphism projModel (W'.map φ) ⟶ projModel W', and the addition morphism commutes with base change (WeierstrassCurve.additionMorphism_projModelBaseChange).

Main results

• WeierstrassCurve.additionMorphism_comp_hom_of_iso: a pointed isomorphism of projective Weierstrass models over Spec R commutes with the addition morphisms.
• WeierstrassCurve.additionMorphism_comp_of_isPullback: a pointed cartesian morphism of projective Weierstrass models commutes with the addition morphisms.

References

• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, 2.1–2.2.
• P. Deligne and M. Rapoport, Les schémas de modules de courbes elliptiques, II.1.

theorem WeierstrassCurve.additionMorphism_comp_hom_of_iso {R : Type u} [CommRing R] {W W' : WeierstrassCurve R} [W.IsElliptic] [W'.IsElliptic] (e : W.projModel ≅ W'.projModel) (he : CategoryTheory.CategoryStruct.comp e.hom W'.projModelOver = W.projModelOver) (h0 : CategoryTheory.CategoryStruct.comp W.projModelZero e.hom = W'.projModelZero) : CategoryTheory.CategoryStruct.comp W.additionMorphism e.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map W.projModelOver W.projModelOver W'.projModelOver W'.projModelOver e.hom e.hom (CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧R)) ⋯ ⋯) W'.additionMorphism

The addition morphism commutes with pointed isomorphisms. An isomorphism e : projModel W ≅ projModel W' of projective models of elliptic Weierstrass curves over R, over Spec R and carrying the zero section to the zero section, carries the addition morphism of W to that of W'.

theorem WeierstrassCurve.additionMorphism_comp_of_isPullback {R R' : Type u} [CommRing R] [CommRing R'] {W : WeierstrassCurve R} {W' : WeierstrassCurve R'} [W.IsElliptic] [W'.IsElliptic] {F : W.projModel ⟶ W'.projModel} {ψ : AlgebraicGeometry.Spec ↧R ⟶ AlgebraicGeometry.Spec ↧R'} (hF : CategoryTheory.IsPullback F W.projModelOver W'.projModelOver ψ) (h0 : CategoryTheory.CategoryStruct.comp W.projModelZero F = CategoryTheory.CategoryStruct.comp ψ W'.projModelZero) : CategoryTheory.CategoryStruct.comp W.additionMorphism F = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map W.projModelOver W.projModelOver W'.projModelOver W'.projModelOver F F ψ ⋯ ⋯) W'.additionMorphism

The addition morphism commutes with pointed cartesian morphisms. Let F : projModel W ⟶ projModel W' be a morphism of projective models of elliptic Weierstrass curves over R and R', lying over ψ : Spec R ⟶ Spec R', such that the square formed by F, the structure morphisms and ψ is a pullback square, and carrying the zero section to the zero section. Then F carries the addition morphism of W to that of W'.