Generic point and function-field pull-backs for elliptic curves #

Definition: EllipticCurve_FunctionFieldPullback (cc616e54-6b99-5922-988e-22ce404946c4), by Claude, 2026-09-05.

Throughout, $W$ is a Weierstrass curve over a field $R$ and $K$ an $R$-algebra which is a field; $E = W_{/K}$ denotes the base-changed affine curve, $K[E]$ its Mathlib coordinate ring $K[X][Y]/(\,W\text{-polynomial})$ and $L = K(E)$ its function field (the fraction field of $K[E]$). A first group of results concerns $K[E]$ as a $K[X]$-algebra: it is finite and integral over $K[X]$, every nonzero prime ideal of it is maximal, and for $K$ algebraically closed every nonzero prime equals $\mathrm{XYIdeal}(a, C\,b) = (X-a,\;Y-b)$ for some solution $(a,b)$ of the affine equation, these ideals being maximal. Point.xc, Point.yc read off the coordinates of an affine point (value $0$ at the point at infinity). The generic point is the $L$-point $\gamma$ whose coordinates genericX, genericY are the images in $L$ of the classes of $X$ and $Y$; that it satisfies the equation, hence is nonsingular when $W$ is elliptic, is proved here. For a nonzero point $Q \in E(L)$, pointHom Q is the $K$-algebra map $K[E] \to L$ determined by $X \mapsto x(Q)$, $Y \mapsto y(Q)$; it is injective whenever $K$ is algebraically closed and $Q$ is not the base change of a $K$-point, and pointPull Q is then its extension $L \to L$ along the fraction field. Specialising $Q$ gives transPull/transEquiv (pull-back along translation by a $K$-point $S$, i.e. the map sending $\gamma$ to $\gamma + S$), negPull/negEquiv (pull-back along inversion), and mulPull W K n, defined from the point $n\cdot\gamma$ when the predicate MulGood W K n holds — namely $n\cdot\gamma \ne 0$ and $n\cdot\gamma$ is not the base change of any $K$-point — and as the identity otherwise. The expected identities are proved: additivity and injectivity of $S \mapsto \tau_S^{*}$, $\iota^{*}\circ\iota^{*} = \mathrm{id}$, $[m]^{*}[n]^{*} = [nm]^{*}$, and $\tau_S^{*}\circ[n]^{*} = [n]^{*}$ when $nS = 0$. placeOf W K P packages $(X-x(P),\,Y-y(P))$ as a height-one prime of $K[E]$; it is injective, and surjective onto the height-one spectrum for $K$ algebraically closed and $W$ elliptic, with CoordinateRing.evalAt the evaluation homomorphism $K[E] \to K$ at a solution of the equation. Finally, Valuation.Cong v a b is the relation $v(a-b) < 1$ — congruence modulo the valuation ideal, not an identity — shown stable under sums, products and powers of elements of valuation $\le 1$, under inversion and division by elements of valuation $1$, and under two-variable polynomial evaluation; from it and a valuation-transfer lemma for a ring map between fraction fields of Dedekind domains, the module deduces that $v_P(\mathrm{pointPull}\,Q\,(h)) \le e^{-k}$ whenever $v_{P'}(h) \le e^{-k}$, for points whose coordinates are congruent at $P$, and the corresponding statement for mulPull in terms of polynomials $\Phi, \Psi, \omega, \psi$ expressing the coordinates of $n\cdot\gamma$ and of $n\cdot P$ as rational functions of the coordinates.

Relation to Mathlib. Mathlib supplies the affine Weierstrass curve, its coordinate ring with XClass, YClass, XYIdeal, the function field, the group of affine points and base change of points; the generic point, the homomorphisms pointHom/pointPull and their translation, inversion and multiplication-by-$n$ specialisations, the map from points to the height-one spectrum, and the valuation congruence relation Valuation.Cong are the project's own.

Where it is used. The material sets up the action of translations, inversion and multiplication by $n$ on the function field of an elliptic curve, together with the dictionary between affine points over an algebraically closed field and height-one places of the coordinate ring, and a valuation comparison between a point $P$ and its multiple $n\cdot P$.