The additive group of morphisms between elliptic curves #
The carrier Isogeny.Hom W₁ W₂ — the isogenies W₁ → W₂ together with the zero map — is
identified with the point at infinity together with the points of W₂ over the function field of
W₁ whose x-coordinate has a pole at the place at infinity, and inherits the group law of those
points.
A morphism is determined by its tautological point: the point at infinity for the zero map,
and for an isogeny the point of W₂ over F(W₁) cut out by the pulled-back coordinate functions.
That point has a pole at infinity exactly because an isogeny is pointed, and every point with such
a pole arises from a pointed coordinate pullback, so the tautological point is a bijection onto
the subgroup polePoints W₂ (Place.infinity W₁). The addition on Hom W₁ W₂ is the one making
this bijection additive; the zero and the negation are those the carrier already has.
Main definitions #
TauCeti.Isogeny.Hom.tautologicalPoint: the tautological point of a morphism.TauCeti.Isogeny.Hom.polePointsAddEquiv:Hom W₁ W₂ ≃+ polePoints W₂ (Place.infinity W₁).TauCeti.Isogeny.Hom.compRightHom: precomposition by a morphism, as an additive homomorphism;zsmul_compandnsmul_compare itsmap_zsmulandmap_nsmul.- The
AddCommGroup (Hom W₁ W₂)instance.
Main results #
TauCeti.Isogeny.Hom.ofIsogeny_add_ofIsogeny: the sum of two isogenies whose tautological points do not cancel is the isogeny with pullbackCoordinatePullback.add.TauCeti.Isogeny.Hom.add_comp: composition is additive in the outer morphism.
Provenance #
The identification of the morphisms with the pole points is Silverman III.4 read at the generic
point. Its ingredients are the tautological point of a coordinate pullback and its injectivity
(CoordinatePullback.tautologicalPoint, CoordinatePullback.tautologicalPoint_injective), the sum
of two coordinate pullbacks (CoordinatePullback.add), the pole criterion for pointedness
(CoordinatePullback.mapsInfinity_of_one_lt_infinityPlace) and the subgroup of points with a pole
at a place (polePoints).
References #
The tautological point of a morphism: the point at infinity for the zero map, and the tautological point of the coordinate pullback for an isogeny.
Equations
- f.tautologicalPoint = if hf : f = 0 then 0 else (TauCeti.Isogeny.Hom.toIsogeny hf).pullback.tautologicalPoint
Instances For
A morphism vanishes exactly when its tautological point is the point at infinity.
A morphism is determined by its tautological point.
Extensionality: morphisms with the same tautological point are equal.
The tautological point of -f is the negative of that of f.
The tautological point of a morphism has a pole at infinity, or is the point at infinity.
The morphism with a given tautological point: the zero map at the point at infinity, and
otherwise the isogeny whose pullback evaluates the coordinate functions at the point, pointed
because x has a pole at infinity there.
Equations
- TauCeti.Isogeny.Hom.ofPolePoint Q = if hQ : ↑Q = 0 then 0 else TauCeti.Isogeny.Hom.ofIsogeny { pullback := WeierstrassCurve.Affine.CoordinateRing.evalAlgHom ⋯, mapsInfinity := ⋯ }
Instances For
The tautological point of ofPolePoint Q is Q.
Addition of morphisms: the morphism whose tautological point is the sum of the tautological points.
Equations
- TauCeti.Isogeny.Hom.instAdd = { add := fun (f g : TauCeti.Isogeny.Hom W₁ W₂) => TauCeti.Isogeny.Hom.ofPolePoint (⟨f.tautologicalPoint, ⋯⟩ + ⟨g.tautologicalPoint, ⋯⟩) }
Equations
- TauCeti.Isogeny.Hom.instSub = { sub := fun (f g : TauCeti.Isogeny.Hom W₁ W₂) => f + -g }
Equations
- TauCeti.Isogeny.Hom.instSMulNat = { smul := nsmulRec }
Equations
- TauCeti.Isogeny.Hom.instSMulInt = { smul := zsmulRec }
The tautological point of a sum is the sum of the tautological points.
The tautological point of a difference is the difference of the tautological points.
The tautological point of n • f is n • f.tautologicalPoint.
The tautological point of n • f is n • f.tautologicalPoint, for an integer n.
The additive group of morphisms, transported from the points with a pole at infinity along the tautological point.
Equations
- TauCeti.Isogeny.Hom.instAddCommGroup = Function.Injective.addCommGroup (fun (f : TauCeti.Isogeny.Hom W₁ W₂) => ⟨f.tautologicalPoint, ⋯⟩) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Morphisms are the point at infinity together with the points with a pole at infinity, as additive groups.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inverse of the additive equivalence is ofPolePoint.
Two isogenies whose tautological points cancel sum to the zero map.
Addition of morphisms is the sum of coordinate pullbacks where the latter is defined.
The tautological point of a composite with an isogeny is the image of the outer morphism's tautological point under the isogeny's function-field pullback.
Composition is additive in the outer morphism.
Composition respects subtraction in the outer morphism.
Precomposition by f, as a homomorphism of the additive groups of morphisms.
Equations
- f.compRightHom = { toFun := fun (g : TauCeti.Isogeny.Hom W₂ W₃) => g.comp f, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Composition is ℤ-linear in the outer morphism.
Composition is ℕ-linear in the outer morphism, the rule for a natural scalar.