The place at infinity under change of the coefficient field

The place at infinity of a base-changed Weierstrass curve restricts to the original place at infinity. The restriction is trivial on the original constants and the generic x-coordinate still has a pole, so uniqueness of the infinity place identifies it. The conclusion identifies their valuation rings, which is the place-level notion of equality.

No ellipticity or algebraicity hypothesis on the extension is needed. The base map may be any homomorphism of fields, including a coefficient automorphism.

References

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

theorem WeierstrassCurve.Affine.isEquiv_comap_infinityPlace_map {F : Type u_1} {K : Type u_2} [Field F] [Field K] (W : Affine F) (f : F →+* K) : (Valuation.comap (FunctionField.map W f) (W.map f).infinityPlace).IsEquiv W.infinityPlace

The place at infinity after changing coefficients restricts to the original place at infinity: the generic x-coordinate retains its pole and the restriction is trivial on F.