A class-group map on points associated to an isogeny #
An isogeny φ : W₁ → W₂ is a map of function fields, backwards, and carries no map of points with
it. The ideal class groups nevertheless define a map on points: Isogeny.pushClass extends an
ideal of W₁.CoordinateRing into the intermediate ring and norms it down to
W₂.CoordinateRing, and Point.toClassEquiv identifies the points of a Weierstrass curve with
the classes of its coordinate ring. Conjugating the first by the second gives
Isogeny.toPointHom : W₁.Point →+ W₂.Point,
a homomorphism by construction, since the class-group map and the point–class dictionary are additive.
The normality hypothesis IsIntegrallyClosed W₂.CoordinateRing is the one pushClass already
asks of the target; for an elliptic curve it is supplied by
WeierstrassCurve.Affine.isIntegrallyClosed_coordinateRing. Nothing here needs W₁ or W₂ to be
elliptic.
The geometric reading is that the image of a point is the point lying under it, in the sense that
its place restricts along φ to the place of the image. Its first half is proved here: a point of
W₁ whose place lies over the point at infinity of W₂ — a point of the fibre φ⁻¹(O₂) — is sent
to 0, because its ideal extends to the unit ideal of the intermediate ring
(TauCeti.Isogeny.map_XYIdeal_eq_top_of_one_lt_valuation). The affine half needs the relative norm
of the prime of the intermediate ring at such a point; it is computed in PointHom/Affine.lean
(TauCeti.Isogeny.toPointHom_some_eq_some_of_isEquiv_comap_pointPlace), for a separable isogeny
over a separably closed field. Functoriality in φ beyond the identity is not proved here.
Main definitions #
TauCeti.Isogeny.toPointHom: the class-group-defined additive map on points.
Main results #
TauCeti.Isogeny.toClass_toPointHom: the defining computation — the class of the image point is the pushed-forward class.TauCeti.Isogeny.toPointHom_eq_iff: a point is the image ofPexactly when its class is the pushed-forward class ofP, the point–class dictionary being injective.TauCeti.Isogeny.toPointHom_id: the map on points induced by the identity isogeny is the identity.TauCeti.Isogeny.toPointHom_some_eq_zero_of_isEquiv_comap_infinityPlace: a point lying over the point at infinity of the target is sent to0.
Provenance #
The construction — conjugate the class-group map induced by extension and relative norm by the
point--class dictionary — is adapted from D. Angdinata's shared isogeny development,
Isogeny.lean, by David Kurniadi Angdinata, declaration toPointHom, restated in the
coordinate-ring form this repository gives pushClass. The identity law is not in that source;
it is original here.
References #
- J. Silverman, The Arithmetic of Elliptic Curves, II.3 (the pushforward of divisors along a map of curves, dual to the pullback and computed by the norm) and III.3.4-3.5 (the identification of the points of an elliptic curve with a divisor class group).
The class-group-defined map on points associated to an isogeny: the map
Isogeny.pushClass, read
through the identification WeierstrassCurve.Affine.Point.toClassEquiv of the points of a
Weierstrass curve with the ideal classes of its coordinate ring.
Equations
Instances For
The class-group-defined map sends P to the point corresponding to its pushed-forward
class.
The class of the image point is the pushed-forward class. This characterises toPointHom,
since WeierstrassCurve.Affine.Point.toClass is injective.
A point is the image of P exactly when its class is the pushed-forward class of P.
The map on points induced by the identity isogeny is the identity.
A point over the point at infinity is sent to 0. If the place of the affine point
(x, y) of W₁ restricts along φ to the place at infinity of W₂ — the point lies in the fibre
φ⁻¹(O₂) — then φ.toPointHom sends it to the point at infinity.