Fibres of multiplication by n are finite #
Theorem statement: WeierstrassCurve.Affine.fibSet_finite (d1b840cd-018f-5bca-9508-90b9fb006ef1),
by Claude, 2026-09-05.
Proof: submission 6812f5c9-90dd-56c9-99cf-10d3c43d2e28, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $F$ and $K$ be fields with $K$ an $F$-algebra and $K$ algebraically closed, let $W$ be a
Weierstrass curve over $F$ which is elliptic, and let $n$ be a natural number whose image in $K$ is
nonzero. Write $(W⁄K)$ for the base change of $W$ to $K$ and $(W⁄K)$.Point for its group of affine
points together with the point at infinity. Then for every point $Q$ of $(W⁄K)$, the set fibSet W K n Q, that is $\{P : n \cdot P = Q\}$, the fibre over $Q$ of multiplication by the integer $n$ on
$(W⁄K)$.Point, is finite. No claim is made about the cardinality of this fibre, nor about its
non-emptiness; the assertion is finiteness alone, and in particular it holds vacuously when $Q$ is
not divisible by $n$.
This is the finiteness half of the classical description of the fibres of the isogeny $[n]$ on an
elliptic curve over an algebraically closed field of residue characteristic prime to $n$: a fibre is
empty or a translate of the $n$-torsion subgroup, which has $n^2$ elements. It underlies the
counting and valuation statements used in the construction of the Weil pairing, being cited by
WeierstrassCurve.Affine.ncard_fibSet and by the
lemmas on valuations of Weil functions.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_WeierstrassCurve_Affine_fibSet_finite.lean
<!-- Generated by add_prove2me_provenance.py -->