The group law of an elliptic curve commutes with base change #
Let E be an elliptic curve over a scheme S and E' an elliptic curve over a scheme S'. A
morphism g : E' ⟶ E lying over f : S' ⟶ S such that the square formed by g, f and the two
structure morphisms is a pullback square, and carrying the zero section of E' to that of E,
exhibits E' as the base change of E along f. This file shows that such a morphism carries
the addition morphism of E' to that of E
(EllipticCurveGeom.addition_comp_of_isPullback) and the negation morphism of E' to that of E
(EllipticCurveGeom.neg_comp_of_isPullback). In particular the group law of the base change
E.baseChange f is the base change of the group law of E, for every morphism f : S' ⟶ S
(EllipticCurveGeom.addition_baseChangeIso_hom_fst and
EllipticCurveGeom.neg_baseChangeIso_hom_fst).
The addition morphism of E' is characterised by its restrictions to the charts of any pointed
Weierstrass atlas (EllipticCurveGeom.eq_addition_of_atlas). The charts of E' whose bases
map over f into bases of charts of E form an atlas of E'
(EllipticCurveGeom.exists_chart_comp_baseMap). On such a chart k, lying over a chart c of
E, the morphism g restricts to a morphism from the restriction of E' to the base of k to
the restriction of E to the base of c (PointedWeierstrassChart.carrierMap). Through the
isomorphisms with the projective models of the equations of k and c, it is a base change
square of projective models carrying the zero section to the zero section
(PointedWeierstrassChart.modelMap), and the Bosma–Lenstra addition morphism and the negation
morphism commute with such squares
(WeierstrassCurve.additionMorphism_comp_of_isPullback and
WeierstrassCurve.projModelNeg_comp_of_isPullback).
Main results #
TauCeti.AlgebraicGeometry.EllipticCurveGeom.addition_comp_of_isPullbackandTauCeti.AlgebraicGeometry.EllipticCurveGeom.neg_comp_of_isPullback: a pointed morphism of elliptic curves forming a pullback square over a morphism of bases carries the addition and negation morphisms of its source to those of its target.TauCeti.AlgebraicGeometry.EllipticCurveGeom.addition_baseChangeIso_hom_fstandTauCeti.AlgebraicGeometry.EllipticCurveGeom.neg_baseChangeIso_hom_fst: the projection from the base changeE.baseChange ftoEcarries the addition morphism and the negation morphism ofE.baseChange fto those ofE.
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.
The group law on charts over a base change square #
Pointed pullback squares of elliptic curves #
The addition morphism commutes with base change. Let g : E' ⟶ E be a morphism of
elliptic curves lying over f : S' ⟶ S, such that the square formed by g, f and the structure
morphisms is a pullback square, and carrying the zero section of E' to that of E. Then g
carries the addition morphism of E' to that of E.
The addition morphism commutes with base change. Let g : E' ⟶ E be a morphism of
elliptic curves lying over f : S' ⟶ S, such that the square formed by g, f and the structure
morphisms is a pullback square, and carrying the zero section of E' to that of E. Then g
carries the addition morphism of E' to that of E.
The negation morphism commutes with base change. Let g : E' ⟶ E be a morphism of
elliptic curves lying over f : S' ⟶ S, such that the square formed by g, f and the structure
morphisms is a pullback square, and carrying the zero section of E' to that of E. Then g
carries the negation morphism of E' to that of E.
The negation morphism commutes with base change. Let g : E' ⟶ E be a morphism of
elliptic curves lying over f : S' ⟶ S, such that the square formed by g, f and the structure
morphisms is a pullback square, and carrying the zero section of E' to that of E. Then g
carries the negation morphism of E' to that of E.
The base change of an elliptic curve #
The addition morphism of a base change. The projection from the base change
E.baseChange f to E carries the addition morphism of E.baseChange f to that of E.
The addition morphism of a base change. The projection from the base change
E.baseChange f to E carries the addition morphism of E.baseChange f to that of E.
The negation morphism of a base change. The projection from the base change
E.baseChange f to E carries the negation morphism of E.baseChange f to that of E.
The negation morphism of a base change. The projection from the base change
E.baseChange f to E carries the negation morphism of E.baseChange f to that of E.