Pointedness at the place at infinity

An isogeny of affine Weierstrass curves is a coordinate pullback φ : R(W₂) → K(W₁) carrying the integrality condition MapsInfinity, the algebraic form of φ(O₁) = O₂. This file reads that condition off as a statement about places: restricting the place at infinity of W₁ along the function-field pullback gives the place at infinity of W₂,

((W₁.infinityPlace).comap φ.fieldPullback).IsEquiv W₂.infinityPlace.

The proof is the pole of x. Suppose the pulled-back coordinate φ x₂ had no pole at O₁. The Weierstrass equation of W₂, pulled back, then forces φ y₂ to have no pole either — a pole of φ y₂ would make the left-hand side dominate a right-hand side of value at most 1 — so the whole image φ(R(W₂)) lies in the valuation ring at infinity of W₁. That ring is integrally closed, so MapsInfinity puts x₁ in it as well, contradicting the double pole v_∞ x₁ = exp 2. Hence φ x₂ has a pole at O₁, and WeierstrassCurve.Affine.isEquiv_infinityPlace_of_one_lt identifies the restricted valuation.

Conversely, a coordinate pullback is pointed as soon as the pullback of some function of the target acquires a pole at the source's infinity, with no injectivity assumed; the coordinate x₂ is the usual witness, so pointedness of an arbitrary coordinate pullback is exactly a pole of the pulled-back x₂.

Neither direction uses ellipticity, separability, or the degree of an isogeny.

Main results

• TauCeti.Isogeny.one_lt_infinityPlace_pullback_X: the pulled-back coordinate has a pole at infinity, 1 < v_∞ (φ x₂).
• TauCeti.Isogeny.isEquiv_comap_infinityPlace: the place at infinity restricts to the place at infinity along an isogeny.
• TauCeti.CoordinatePullback.mapsInfinity_iff_one_lt_infinityPlace: pointedness is exactly a pole of x at infinity, for any coordinate pullback — the form in which a construction can establish it by one valuation computation.
• TauCeti.CoordinatePullback.mapsInfinity_map_iff: base change reflects pointedness.
• TauCeti.CoordinatePullback.mapsInfinity_iff_isEquiv_comap_infinityPlace: the pointedness criterion, MapsInfinity σ ↔ σ_*(O₁) = O₂, for an embedding σ of function fields.

References

• J. Silverman, The Arithmetic of Elliptic Curves, II.2, III.4.

theorem TauCeti.Isogeny.one_lt_infinityPlace_pullback_X {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) : 1 < W₁.infinityPlace (φ.pullback ((algebraMap (Polynomial F) W₂.CoordinateRing) Polynomial.X))

The pullback of the target's coordinate x has a pole at the source's point at infinity. If it did not, then neither would the pullback of y — by the Weierstrass equation of the target — so the whole pulled-back coordinate ring would lie in the valuation ring at infinity of the source; that ring is integrally closed, so MapsInfinity would put the source coordinate x₁ in it, against its double pole.

theorem TauCeti.Isogeny.isEquiv_comap_infinityPlace {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) : (Valuation.comap φ.fieldPullback.toRingHom W₁.infinityPlace).IsEquiv W₂.infinityPlace

An isogeny carries the place at infinity to the place at infinity: the restriction of the source's place at infinity along the function-field pullback is equivalent to the target's. This is the place-level reading of MapsInfinity, that is, of φ(O₁) = O₂.

theorem TauCeti.CoordinatePullback.mapsInfinity_of_one_lt_infinityPlace {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (p : CoordinatePullback W₁ W₂) (a : W₂.CoordinateRing) (h : 1 < W₁.infinityPlace (p a)) : p.MapsInfinity

A coordinate pullback under which some function acquires a pole at infinity maps infinity to infinity. Any one function of W₂ whose pullback has a pole at the source's point at infinity suffices; the coordinate x is the usual witness (mapsInfinity_iff_one_lt_infinityPlace). Injectivity of p is not assumed, in contrast with the criterion for embeddings of function fields, mapsInfinity_iff_isEquiv_comap_infinityPlace.

theorem TauCeti.CoordinatePullback.mapsInfinity_iff_one_lt_infinityPlace {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (p : CoordinatePullback W₁ W₂) : p.MapsInfinity ↔ 1 < W₁.infinityPlace (p ((algebraMap (Polynomial F) W₂.CoordinateRing) Polynomial.X))

Pointedness is exactly a pole of x at infinity. A coordinate pullback maps infinity to infinity precisely when it sends the target's coordinate x to a function with a pole at the source's point at infinity, so a construction can establish pointedness by a single valuation computation.

@[simp]

theorem TauCeti.CoordinatePullback.mapsInfinity_map_iff {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} {K : Type u_2} [Field K] (p : CoordinatePullback W₁ W₂) (f : F →+* K) : (p.map f).MapsInfinity ↔ p.MapsInfinity

Changing the coefficient field reflects pointedness. The pole criterion for MapsInfinity is unchanged because the infinity valuation after base change restricts to the original one.

theorem TauCeti.CoordinatePullback.mapsInfinity_iff_isEquiv_comap_infinityPlace {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (σ : W₂.FunctionField →ₐ[F] W₁.FunctionField) : MapsInfinity (σ.comp (IsScalarTower.toAlgHom F W₂.CoordinateRing W₂.FunctionField)) ↔ (Valuation.comap σ.toRingHom W₁.infinityPlace).IsEquiv W₂.infinityPlace

The pointedness criterion. An embedding σ : F(W₂) → F(W₁) restricts to a coordinate pullback which maps infinity to infinity exactly when the source's place at infinity restricts along σ to the target's place at infinity.