Pointedness is decided by the x-coordinate

MapsInfinity asks that every element of the source coordinate ring, read in the source function field, be integral over the target coordinate ring acting through the pullback. That is a condition on infinitely many elements, but it is equivalent to the single case of the generic x-coordinate — one direction because that coordinate is one of them, the other because:

• the generic y-coordinate is then integral too, because the Weierstrass equation exhibits it as a root of a monic quadratic whose coefficients are polynomial in x;
• every element of the coordinate ring lies in the subalgebra generated by the two coordinates, and integrality is preserved by the ring operations.

So a construction that produces a coordinate pullback only has to exhibit one integral witness.

Main results

• TauCeti.CoordinatePullback.mapsInfinity_iff_isIntegralElem_genericX: a coordinate pullback maps infinity to infinity exactly when the generic x-coordinate is integral over it.

Implementation notes

The hypothesis is stated with RingHom.IsIntegralElem against p.toRingHom rather than as IsIntegral W₂.CoordinateRing, because for an endomorphism the source and target coordinate rings coincide and W₁.FunctionField then carries two Algebra W₂.CoordinateRing structures — the fraction-field embedding and the one pulled back along p. Naming the homomorphism leaves no instance to be resolved.

References

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

theorem TauCeti.CoordinatePullback.mapsInfinity_iff_isIntegralElem_genericX {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (p : CoordinatePullback W₁ W₂) : p.MapsInfinity ↔ p.IsIntegralElem W₁.genericX

Pointedness is decided by the x-coordinate. A coordinate pullback maps infinity to infinity exactly when the generic x-coordinate of the source is integral over the target coordinate ring acting through it, so a construction producing a coordinate pullback has to exhibit one integral witness.