Modularity of elliptic curves over ℚ via eigenform coefficients #

Definition: FLTPrelim_Modularity (ddd45b70-a042-5d79-93f9-c52e6062e9d4), by Claude, 2026-09-05.

The module fixes the project's notion of modularity in terms of $q$-expansion coefficients and point counts on a chosen integral equation. For $f:\mathbb H\to\mathbb C$, ModularFormClass.qCoeff f n is the $n$-th coefficient of Mathlib's $q$-expansion of $f$ at width $1$. CuspForm.IsNormalizedEigenform is a structure on a weight-$2$ cusp form $f$ for $\Gamma_0(N)$ whose fields are exactly the arithmetic of the coefficients: $a_1=1$; $a_{mn}=a_ma_n$ for coprime $m,n$; $a_{p^{r+2}}=a_pa_{p^{r+1}}-p\,a_{p^r}$ for all primes $p\nmid N$; and $a_{p^{r+2}}=a_pa_{p^{r+1}}$ for primes $p\mid N$. No Hecke operator appears: being an eigenform is encoded purely by these recursions. On the curve side, for a Weierstrass curve over a finite ring the point type is finite (proved by injecting points into Option (R × R), the point at infinity going to none), the number of points of a Weierstrass curve over a commutative ring — Mathlib's affine point type, which includes the point at infinity — is given a name card, and traceOfFrobenius is $\#F+1$ minus that number. For $W$ over $\mathbb Z$, reductionMod W p is the coefficientwise reduction to $\mathbb Z/p$ and apOfModel W p its $p+1-\#W(\mathbb F_p)$. Three predicates on integral equations follow: IsGoodPrimeFor W p is simply $p\nmid\Delta(W)$; IsSemistableModel W says no prime divides both $\Delta(W)$ and $c_4(W)$; IsIntegralModelOf W E says some variable change over $\mathbb Q$ carries $E$ to the base change of $W$ to $\mathbb Q$. Finally IsModularModelOfLevel W N asserts the existence of a weight-$2$ cusp form on $\Gamma_0(N)$ satisfying the above recursions with $a_p(f)=a_p(W)$ for every prime $p$ with $p\nmid\Delta(W)$ and $p\nmid N$; IsModularModel W adds $N\ge 1$; and IsModular E says some integral model of $E$ is a modular model. Thus modularity is an equality of $L$-coefficients at good primes away from the level, not an assertion about a newform of the conductor, nor a Galois-representation isomorphism; semistability is a condition on the chosen equation rather than on $E$.

Relation to Mathlib. CuspForm, CongruenceSubgroup.Gamma0, $q$-expansions, WeierstrassCurve with its invariants $c_4,\Delta$, VariableChange and affine points are Mathlib's; the eigenform recursions, the counting function and trace of Frobenius, reduction modulo $p$, and the semistability, integral-model and modularity predicates are the project's own, together with a Finite instance for affine points over a finite ring.

Where it is used. These definitions give the statement of the modularity input to the proof: [WeierstrassCurve.modularity_of_semistableModel] (../thm.html#WeierstrassCurve.modularity_of_semistableModel) derives IsModular from IsSemistableModel (with $\Delta\ne0$), and [FreyPackage.frey_isModular] (../thm.html#FreyPackage.frey_isModular) applies it to the Frey curve attached to a counterexample to Fermat's Last Theorem. Nearly the whole tree below the modularity theorem is phrased in terms of these notions.

source