Valuation estimates for Weierstrass points with non-integral coordinates #
Definition: WeierstrassCurve_TorsionIntegral (85e72084-5eb9-57ab-91cc-e3a8d633f02a), by Claude,
2026-09-05.
The module works with a field $L$, a valuation subring $A \subseteq L$ and a Weierstrass curve $W$
over $A$, whose base change along the inclusion $A \hookrightarrow L$ is the curve $W.map A.subtype$
over $L$ and whose reduction is $W.map (residue A)$ over the residue field. Two kinds of statements
are proved. First, arithmetic of $A$ and its set of nonunits $A.nonunits$ (the elements of valuation
$<1$): the sum of a non-element and an element, the product of two non-elements, and a quotient
$a/b$ with $a \notin A.nonunits$ and $b \ne 0$ a nonunit all lie outside $A$ (add_notMem,
mul_notMem, div_notMem); membership in $A.nonunits$ of an element of $A$ is equivalent to
vanishing of its residue, and for a natural number $n$ to $(n : \mathrm{ResidueField}\,A) = 0$;
inverses of nonunits of $A$, of non-elements and of units are located (inv_mem_of_notMem_nonunits,
inv_mem_nonunits_of_notMem, mul_notMem_nonunits, one_add_notMem_nonunits).
Second, estimates for affine points. For an affine point $(x,y)$ with $x \in A$ and $\Delta$ of the
reduced curve nonzero, if $y - \mathrm{negY}(x,y)$ is a nonunit then the partial derivative $3x^2 + 2a_2x + a_4 - a_1y$ is a unit; consequently, for two points $(x_1,y_1)$, $(x_2,y_2)$ with $x_1, x_2 \in A$ such that $x_1 - x_2$ and $y_1 - \mathrm{negY}(x_2,y_2)$ are nonunits while $(x_1,y_1) \ne (x_2,\mathrm{negY}(x_2,y_2))$, the slope and the resulting $\mathrm{addX}$ lie outside $A$
(slope_notMem_of_sub_mem_nonunits, addX_notMem_of_sub_mem_nonunits). For $x \notin A$ one gets
$y \neq 0$, $y \notin A$, $x/y \in A.nonunits$ and $x^3/y^2$ a unit of $A$; the formal parameter $t = -x/y$ satisfies $t(-P) \equiv -t(P)$ and, via Vieta relations for $\mathrm{addX}$ and explicit
secant and tangent identities, $t(P \oplus Q) - t(P) - t(Q)$ lies in $\tau\cdot A.nonunits$ whenever
$t(P), t(Q) \in \tau A$ for a nonunit $\tau \neq 0$ (add_formal_param_estimate). Iterating,
formal_param_nsmul shows for each $j$ that $j \cdot P = 0$ forces $(j : L)$ to be a nonunit, and
that $j \cdot P = P'$ forces $x' \notin A$ and $t(P')/t(P) \equiv j$. Hence
X_mem_of_nsmul_eq_zero': if $n$ is invertible in the residue field and $P = (x,y)$ satisfies $n \cdot P = 0$, then $x \in A$. Finally, some_eq_of_mem_inertia_of_nsmul_eq_zero' and
fixed_of_mem_inertia_of_nsmul_eq_zero state that an element $\sigma$ of the decomposition group of
$A$ over a base field $K$ lying in the inertia subgroup fixes such an $n$-torsion point when the
reduced discriminant is nonzero and $(\sigma x, \sigma y)$ is again $n$-torsion: $\sigma x = x$ and
$\sigma y = y$.
Relation to Mathlib. Mathlib supplies Weierstrass curves, their affine points with the
chord–tangent group law, slope, addX, addY, negY, valuation subrings with their nonunits and
residue field, and decomposition and inertia subgroups; the valuation estimates for points with
non-integral coordinates, the formal-parameter congruences and the integrality of
prime-to-residue-characteristic torsion proved here are the project's own.
Where it is used. These estimates support the reduction map on points of a Weierstrass curve over a valuation subring: integrality of $n$-torsion when $n$ is invertible in the residue field, and the resulting triviality of the inertia action on such torsion, are what makes the mod-$p$ Galois representation attached to the Frey curve unramified away from the relevant primes.
<!-- Generated by add_prove2me_provenance.py -->