Definitions/Def_ModularCurve_JZeroTorsionFinite.lean

Two propositions are introduced. The first, ModularCurve.JZeroTorsionFinite M n for a nonzero natural number M and a natural number n, asserts that the additive subgroup Pic0.torsion (AlgebraicClosure ℚ) (modularFunctionFieldBar M) n is finite. Here the degree-zero divisor class group Pic0 K F of a field extension F/K is the quotient of the group of degree-zero divisors — finitely supported \mathbb{Z}-valued functions on the set of places of F/K, a place being a valuation subring of F containing the image of K, distinct from F and a principal ideal ring, with degree the residue-field degree over K — by the subgroup of principal divisors \operatorname{div}(f), f \in F^{\times}, that lie in it; and Pic0.torsion K F n is the \mathbb{Z}-torsion submodule annihilated by (n : \mathbb{Z}), regarded as an additive subgroup. The extension used is the one modelling the modular curve of level M through q-expansions: modularFunctionFieldFull M is the subfield of \mathbb{Q}-Laurent series generated over \mathbb{Q} by the series q \mapsto j(q^{d}) for the nonzero divisors d \mid M, and modularFunctionFieldBar M is its base change to \overline{\mathbb{Q}}, namely the subfield of Laurent series over \overline{\mathbb{Q}} generated by \overline{\mathbb{Q}} together with the coefficientwise images of that field. Thus the predicate says that the n-torsion of J_0(M) over \overline{\mathbb{Q}}, in this function-field presentation, is finite.

The second, FreyPackage.MazurJZeroPTorsionFiniteFamily P q for a Frey package P = (a,b,c,p) (nonzero integers with a^{p}+b^{p}=c^{p}, p \ge 5 prime, \gcd(a,b)=1, a \equiv 3 \bmod 4, b even) and a nonzero natural number q, packages the first predicate into a family: it asserts JZeroTorsionFinite (N * q) P.p for every nonzero natural number N with q \nmid N, i.e. finiteness of J_0(Nq)[p] at all levels Nq with q exactly dividing the q-part.