Reduction of Weierstrass points along a valuation subring #
Definition: WeierstrassCurve_ReductionMap (b2456017-3633-5aa3-a641-d221438b26e6), by Claude,
2026-09-05.
Let $L$ be a field, $A \subseteq L$ a valuation subring with residue field $\kappa_A$, and $W$ a
Weierstrass curve over $A$, i.e. a tuple $a_1,a_2,a_3,a_4,a_6 \in A$. Writing $W_L$ for the base
change along the inclusion $A \to L$ and $\tilde W$ for the base change along the residue map $A \to \kappa_A$, the main definition
WeierstrassCurve.reducePoint takes a hypothesis
$h_\Delta$ asserting $\Delta(\tilde W) \neq 0$ and produces a map from the affine points of $W_L$ to
the affine points of $\tilde W$: the point at infinity goes to the point at infinity; an affine
point $(x,y)$ goes to $(\bar x, \bar y)$ if $x \in A$, and to the point at infinity otherwise. This
is a map of pointed sets defined by cases, not yet a homomorphism. Two facts make it well posed:
Affine.Y_mem_of_X_mem, which says that a solution of the Weierstrass equation of $W_L$ with $x \in A$ automatically has $y \in A$ (otherwise $1$ would lie in the nonunits of $A$), and
Affine.nonsingular_residue, which upgrades the reduced equation to nonsingularity using
$\Delta(\tilde W) \neq 0$. The criterion map_residue_Δ_ne_zero_iff identifies that hypothesis with
$\Delta(W)$ being a unit of $A$.
The equational lemmas record the three branches, and reducePoint_neg states that reduction
commutes with negation. Under a $K$-algebra structure on $L$,
reducePoint_some_apply_of_mem_inertia states that if $\sigma : L \simeq_K L$ stabilises $A$ and
acts trivially on $\kappa_A$, then $(\sigma x, \sigma y)$ and $(x,y)$ have the same reduction; this
rests on smul_mem_of_mem_decompositionSubgroup ($\sigma$ preserves $A$) and
residue_smul_eq_of_mem_inertiaSubgroup. Further supporting lemmas concern the predicate
LiesOverPrime A q, which says that $q \in L$ is a nonunit of $A$: such an $A$ has $q$ in its
maximal ideal and residue field of characteristic $q$ (charP_residueField_of_liesOverPrime_def),
and for $L$ of characteristic zero and $q$ prime such an $A$ exists (exists_liesOverPrime).
Finally, mem_inertiaSubgroupIn unfolds membership in the image of the inertia subgroup inside $L \simeq_K L$.
Relation to Mathlib. Mathlib supplies WeierstrassCurve, affine points, base change, and the
decomposition and inertia subgroups of a valuation subring; the reduction map on points along a
valuation subring, the predicate LiesOverPrime and the subgroup inertiaSubgroupIn of $L \simeq_K L$ are the project's own.
Where it is used. The reduction map is the basis for comparing the $p$-torsion of the Frey curve
with the points of its special fibre, and reducePoint_some_apply_of_mem_inertia is the
computational input to the statement that the mod $p$ Galois representation is unramified at a prime
of good reduction.
<!-- Generated by add_prove2me_provenance.py -->
Reduce integral affine coordinates to the good-reduction curve, sending nonintegral points and infinity to infinity.
Equations
- One or more equations did not get rendered due to their size.
- WeierstrassCurve.reducePoint hΔ WeierstrassCurve.Affine.Point.zero = WeierstrassCurve.Affine.Point.zero