The action of a morphism on points #
A morphism f : Hom W₁ W₂ of elliptic curves is recorded by its tautological point, a point of
W₂ over the function field of W₁. Its value at a point P of W₁ is the reduction of that
point at the place of P (WeierstrassCurve.Affine.reductionOfDegreeEqOne). This file defines
that map, Hom.pointMap, and proves the facts that make it the action of f on points:
- it is additive in the morphism;
- for an isogeny
φ, the place ofφ Pis the restriction of the place ofPalongφ^*, and composites act by composition; - the zero morphism sends every point to
Oand the identity fixes every point; - for a separable isogeny over a separably closed field it agrees with the additive class-group
point map
TauCeti.Isogeny.toPointHom, so it is additive there.
Rigidity. A nonzero morphism has finite fibres on points. Thus two morphisms agreeing on infinitely many points are equal. Over a separably closed field the points are infinitely many, and a morphism is determined by its action on them.
Rigidity yields additivity of composition in the inner variable wherever the outer morphism
acts additively on points. That every morphism does, and hence that composition is additive in
the inner morphism over every field, is proved in Isogeny/Hom/Ring.lean.
Main definitions #
TauCeti.Isogeny.Hom.pointMap: the action of a morphism on points.
Main results #
TauCeti.Isogeny.Hom.add_pointMap: the action is additive in the morphism.TauCeti.Isogeny.Hom.pointMap_ofIsogeny_eq_iff: an isogeny sendsPtoQexactly when the place ofPrestricts along its pullback to the place ofQ.TauCeti.Isogeny.Hom.pointMap_ofIsogeny_eq_iff_restrict: the criterion as equality of places.TauCeti.Isogeny.Hom.comp_pointMap: a composite acts by composition.TauCeti.Isogeny.Hom.pointMap_ofIsogeny_eq_toPointHom: for a separable isogeny over a separably closed field the action is the class-group point map.TauCeti.Isogeny.Hom.finite_setOf_pointMap_eq: a nonzero morphism has finite fibres.TauCeti.Isogeny.Hom.eq_of_infinite_setOf_pointMap_eqandTauCeti.Isogeny.Hom.ext_pointMap: rigidity.TauCeti.Isogeny.Hom.ext_pointMap_of_prime_zsmul_eq_zero: rigidity on prime torsion, over a separably closed field.TauCeti.Isogeny.Hom.comp_add_of_pointMap_add: composition is additive in the inner morphism when the outer point map is additive and the source has infinitely many points.
References #
- J. Silverman, The Arithmetic of Elliptic Curves, II.2 (the map on points of a map of curves, read off the restriction of places), III.4.8 and III.4.10.
The action of a morphism on points: f sends P to the reduction of its tautological
point at the place of P. For an isogeny this is the point under P
(pointMap_ofIsogeny_eq_iff), and the zero morphism sends every point to O.
Equations
Instances For
The image of P is the point congruent to the tautological point at the place of P.
The zero morphism sends every point to O.
The action on points is additive in the morphism.
Every morphism sends O to O.
The identity morphism fixes every point.
An isogeny sends a point to the point under it. If the place of P restricts along φ^*
to the place of Q, then φ sends P to Q.
The place of the image of P is the restriction of the place of P along the pullback of
the isogeny, expressed as equivalence of valuations.
An isogeny sends P to Q exactly when the place of P restricts to the place of Q
along its pullback.
An isogeny sends P to Q exactly when the place of P restricts to the place of Q.
For a separable isogeny over a separably closed field the action on points is the
class-group point map, both sending P to the point under it. In particular it is additive
in the point there.
A composite acts on points by composition.
A power of an endomorphism acts by iterating its action on points.
A nonzero morphism has finite fibres on points.
Rigidity: two morphisms agreeing on infinitely many points are equal.
Rigidity: when W₁ has infinitely many points, a morphism is determined by its action on
them. Over a separably closed field this is always the case.
Rigidity on torsion: over a separably closed field, two morphisms agreeing on the
ℓ-torsion points for every prime ℓ other than the characteristic are equal. The ℓ-torsion
alone has ℓ ² points, so the agreement set is infinite.
Composition is additive in the inner morphism when the source has infinitely many points and the outer morphism acts additively on points.