Reduction of points as an additive group homomorphism #

Definition: WeierstrassCurve_ReduceHom (e41eb9e1-feaf-521b-995b-face6f0461a2), by Claude, 2026-09-05.

Throughout, $A$ is a valuation subring of a field $L$ and $W$ is a Weierstrass curve over $A$; the two base changes in play are $W$ pushed along the inclusion $A \hookrightarrow L$ (W.map A.subtype) and along the residue map $A \to \kappa_A$ (W.map (residue A)).

A first group of lemmas records how the residue map interacts with division: if $a \in A$ and $b$ is not a non-unit of $A$ then $a/b \in A$, the residue of such a $b$ is non-zero, the residue of an element of $A$ depends only on its value in $L$, and residues of quotients are quotients of residues (residue_div, residue_eq_div_of_eq_div). Further, two elements of $A$ have the same residue exactly when their difference lies in the set of non-units, i.e. in the maximal ideal.

A second group transports the Weierstrass formulae: for $x,y \in A$ the quantity $\mathrm{negY}(x,y) = -y - a_1x - a_3$ computed on the curve over $L$ lies in $A$ and its residue is $\mathrm{negY}$ of the reduced curve at the reduced arguments, and residue_inverse_iff says that, for $x_i, y_i \in A$, the reduced points satisfy $\bar x_1 = \bar x_2$ and $\bar y_1 = \mathrm{negY}(\bar x_2, \bar y_2)$ precisely when $x_1 - x_2$ and $y_1 - \mathrm{negY}(x_2,y_2)$ both lie in the maximal ideal. Building on these, slope_mem_residue_of_not_inverse shows that for two points of the affine equation with $x_1, x_2 \in A$, whose reductions are not mutually inverse in this sense, the chord-or-tangent slope lies in $A$ and reduces to the slope of the reduced curve at the reduced points; the proof splits according to whether $x_1 - x_2$ is a non-unit and whether $x_1 = x_2$, and rewrites the slope over the common denominator $y_1 - \mathrm{negY}(x_2,y_2)$.

Under the hypothesis $h\Delta$ that the reduced curve has non-zero discriminant, the additivity of the reduction map reducePoint hΔ — which sends an affine point with integral $x$-coordinate to the point with residue coordinates, and every other affine point to zero — is proved in three cases: both $x$-coordinates in $A$ (reducePoint_add_of_mem, where the sum is again integral unless the two reductions are inverse, in which case the reduced sum is zero by Affine.addX_notMem_of_sub_mem_nonunits); neither in $A$ (reducePoint_add_of_notMem_of_notMem, where the formal-parameter estimate Affine.add_formal_param_estimate shows the $x$-coordinate of the sum is again non-integral); and one of each (reducePoint_add_of_mem_of_notMem, deduced from the previous two applied to the sum and the negative of a summand). These combine into reducePoint_add_def, additivity for arbitrary points, and reduceHom, the bundled additive monoid homomorphism from the points of the curve over $L$ to the points of the reduced curve whose underlying function is reducePoint hΔ.

Relation to Mathlib. Mathlib supplies the affine Weierstrass point group with negY, slope, addX, addY and their compatibility with base change, together with valuation subrings and their residue fields; the reduction map on points and its additivity are the project's own.

Where it is used. With good reduction at a place, this homomorphism compares the points of the curve over $L$ with those of the special fibre, and is the tool for controlling $n$-torsion and the action of inertia on it; downstream it is composed with the identification of the special fibre of the Frey curve in the analysis of the attached mod-$p$ Galois representation.