Fibres of [n] on an elliptic curve have n² points #
Theorem statement: WeierstrassCurve.Affine.ncard_fibSet (2481079f-7b1c-5850-82db-2e6507b11804),
by Claude, 2026-09-05.
Proof: submission 25061203-dd50-54dd-8601-f9e2afb6f875, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $F$ and $K$ be fields with $K$ an $F$-algebra, $K$ algebraically closed and equipped with
decidable equality, and let $W$ be a Weierstrass curve over $F$ which is elliptic (i.e. carries the
IsElliptic instance, so its discriminant is a unit). Let $n$ be a natural number whose image in
$K$ is nonzero, and let $Q$ be a point of the affine curve obtained from $W$ by base change to $K$,
written $(W⁄K)$, in the sense of the group of affine points (rational points together with the point
at infinity). The assertion is that the set $\mathrm{fibSet}\ W\ K\ n\ Q$, by definition the set of
those points $P$ of $(W⁄K)$ with $(n : \mathbb{Z}) \bullet P = Q$ for the integer image of $n$
acting through the group structure, has Set.ncard equal to $n^2$. Thus every fibre of
multiplication by $n$ on the group of points of an elliptic curve over an algebraically closed field
of residue characteristic not dividing $n$ consists of exactly $n^2$ points; in particular the
natural-number cardinality is finite and nonzero.
This is the standard counting statement underlying the construction of the Weil pairing: $[n]$ is
surjective on the points of an elliptic curve over an algebraically closed field and its kernel
$E[n]$ has order $n^2$ when $n$ is invertible, so each fibre is a coset of $E[n]$. It is used in the
project's development of the Weil pairing and of the associated valuation computations, being cited
by
[WeierstrassCurve.Affine.exists_smul_basis_eq_algebraMap_mul_weilNum_of_valuationSubring]
(thm.html#WeierstrassCurve.Affine.exists_smul_basis_eq_algebraMap_mul_weilNum_of_valuationSubring)
and
[WeierstrassCurve.Affine.valuation_transEquiv_weilFun]
(thm.html#WeierstrassCurve.Affine.valuation_transEquiv_weilFun).
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_ncard_fibSet.lean
<!-- Generated by add_prove2me_provenance.py -->