Base change of points of an elliptic curve #
Let E be an elliptic curve over a scheme S and E' an elliptic curve over a scheme S', and
let g : E' ⟶ E be a morphism 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. Every S-point P of E then has a base change P', the unique S'-point of E' with
P' ≫ g = f ≫ P. This file shows that base change of points is a homomorphism for the group laws
on points (EllipticCurveGeom.pointsPullback), that it is functorial in the pullback square, and
that it is compatible with the ideal sheaves of sections: the divisor [P'] on E' is the inverse
image of the divisor [P] on E (EllipticCurveGeom.ker_pointsPullback_left), and the inverse
image of a closed subgroup scheme of E is a closed subgroup scheme of E'
(EllipticCurveGeom.exists_grpObj_isMonHom_comap). This is what makes level structures defined
through divisors of points, such as points of exact order N, pull back along base change.
Main definitions #
TauCeti.AlgebraicGeometry.EllipticCurveGeom.pointsPullback hg h0: base change ofS-points ofEtoS'-points ofE', as a group homomorphism.TauCeti.AlgebraicGeometry.EllipticCurveGeom.pointsBaseChangeEquiv hg h0: the group equivalence between points ofE'and points ofEvalued inS'.TauCeti.AlgebraicGeometry.EllipticCurveGeom.universalPoint E: the diagonal section ofE ×_S E, as a point of the base change ofEtoE.TauCeti.AlgebraicGeometry.EllipticCurveGeom.toBaseChangeSelf hg P': the morphism fromE'to the base change ofEtoE, lying over the morphismS' ⟶ Egiven by anS'-pointP'.
Main results #
TauCeti.AlgebraicGeometry.EllipticCurveGeom.mul_left_comp_of_isPullback:gcarries the sum of two points ofE', with values in any scheme overS', to the sum of their images inE;mul_left_comp_eq_of_isPullbackstates this with the group law on points ofE.TauCeti.AlgebraicGeometry.EllipticCurveGeom.pointsPullback_left_comp: the base changeP'ofPsatisfiesP' ≫ g = f ≫ P, andeq_pointsPullback_iffcharacterises it by this property.TauCeti.AlgebraicGeometry.EllipticCurveGeom.pointsPullback_idandTauCeti.AlgebraicGeometry.EllipticCurveGeom.pointsPullback_comp: base change of points along the identity square is the identity, and along a pasted square it is the composite.TauCeti.AlgebraicGeometry.EllipticCurveGeom.pointsPullback_universalPoint: every point of every base change ofEis the base change of the universal point, along the pullback squareisPullback_toBaseChangeSelf.TauCeti.AlgebraicGeometry.EllipticCurveGeom.isPullback_zero_of_isPullback: the zero section ofE'is the base change of the zero section ofE.TauCeti.AlgebraicGeometry.EllipticCurveGeom.left_apply_eq_zero_iff_of_isPullback: anS'-point ofE'meets the zero section ats'exactly when its image inEmeets the zero section ofEthere; in particular (pointsPullback_left_apply_eq_zero_iff) the base changeP'ofPmeets the zero section at a points'ofS'exactly whenPmeets the zero section atf s'.TauCeti.AlgebraicGeometry.EllipticCurveGeom.ker_pointsPullback_left: the ideal sheaf ofP'is the inverse image of the ideal sheaf ofPalongg.TauCeti.AlgebraicGeometry.EllipticCurveGeom.exists_grpObj_isMonHom_comap: the inverse image of a closed subgroup scheme ofEalonggis a closed subgroup scheme ofE'.
References #
- N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, 2.1 and Chapter 4.
An S-point of an elliptic curve over S is a section of its structure morphism.
An S-point of an elliptic curve over S is a section of its structure morphism.
Base change carries sums of points to sums of points. For points x and y of E' with
values in a scheme Z over S', the composite of their sum with g is the sum, under the
addition morphism of E, of the composites of x and y with g.
Base change carries sums of points to sums of points, in terms of the group law on points
of E. If points x and y of E' with values in a scheme Z over S' lie over points x₀
and y₀ of E with values in Z, viewed as a scheme over S, then the sum of x and y lies
over the sum of x₀ and y₀. The structure map f' of Z over S is identified with
Z.hom ≫ f by e.
Base change of points of an elliptic curve. For a morphism g : E' ⟶ E of elliptic curves
lying over f : S' ⟶ S, forming a pullback square with the structure morphisms and carrying the
zero section of E' to that of E, the base change of an S-point P of E is the unique
S'-point P' of E' with P' ≫ g = f ≫ P (eq_pointsPullback_iff). Base change of points is
a homomorphism for the group laws on points.
Instances For
Points of a base change are the points of the original elliptic curve valued in the new base. Composition with the pullback projection gives an equivalence of groups.
Instances For
The underlying morphism of the point corresponding to a base-changed point is its composite with the pullback projection.
The S'-point of E' given by a point x of E with values in S' is the unique section
P of E' with P ≫ g = x.
The S'-point of E' given by a point x of E with values in S' is the unique section
P of E' with P ≫ g = x.
The base change P' of a point P satisfies P' ≫ g = f ≫ P.
The base change P' of a point P satisfies P' ≫ g = f ≫ P.
The characterising property of the base change of a point: an S'-point Q of E' is
the base change of the S-point P of E exactly when Q ≫ g = f ≫ P.
Base change of points along the identity square is the identity.
Base change of points is functorial: base change of points along a pasted pullback square is the composite of the base changes along the two squares.
The universal point of E: the diagonal section of E ×_S E, viewed as a point of the
base change of E to E itself. Every point of every base change of E is a base change of it,
along the morphism to E that the point defines (pointsPullback_universalPoint).
Instances For
The universal point composed with the projection to E is the identity.
The universal point composed with the projection to E is the identity.
The morphism from a base change E' of E to the base change of E to E itself, lying over
the morphism S' ⟶ E given by an S'-point P' of E'.
Instances For
toBaseChangeSelf composed with the projection to E is g.
toBaseChangeSelf lies over the morphism S' ⟶ E given by the point P'.
E' is the base change of the base change of E to E along the morphism S' ⟶ E given by
an S'-point P' of E', via toBaseChangeSelf.
toBaseChangeSelf carries the zero section of E' to that of the base change of E to E.
Every point of a base change of E is a base change of the universal point, along the
morphism S' ⟶ E it defines.
Along a morphism t : T ⟶ S', the base change P' of an S-point P of E agrees with the
zero section of E' exactly when P agrees with the zero section of E along t ≫ f.
The zero section of a base change is the base change of the zero section. For a pullback
square of elliptic curves over f : S' ⟶ S, the square formed by the zero sections, f and g
is a pullback square.
A section of a base change meets the zero section where its image does. For a pullback
square of elliptic curves over f : S' ⟶ S, an S'-point P of E' meets the zero section of
E' at a point s' of S' exactly when g sends P s' to the value of the zero section of E
at f s'.
A base-changed point meets the zero section exactly over the points where the original
point does. For a pullback square of elliptic curves over f : S' ⟶ S and an S-point P of
E, the base change P' of P agrees with the zero section of E' at a point s' of S' if and
only if P agrees with the zero section of E at f s'.
The divisor of a base-changed point. The ideal sheaf of the base change P' of an
S-point P of E, which cuts out the divisor [P'] on E', is the inverse image along g of
the ideal sheaf of P.
Closed subgroup schemes are stable under base change. Let g : E' ⟶ E be a morphism of
elliptic curves lying over f : S' ⟶ S, forming a pullback square with the structure morphisms and
carrying the zero section of E' to that of E. If the closed subscheme of E cut out by an
ideal sheaf D is a subgroup scheme, then so is the closed subscheme of E' cut out by the
inverse image of D along g.