Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_EichlerMass.lean

definition module

Eichler mass and supersingular count as rational functions

Two rational-valued arithmetic functions of a pair of natural numbers N,q are introduced.

The first, ModularCurve.eichlerMass N q, is \bigl((q-1)\,\psi(N)\bigr)/12, where \psi(N) denotes ModularCurve.dedekindPsi N, itself defined as the divisor sum \sum_{d \mid N,\ d \text{ squarefree}} N/d (so \psi(1)=1, and for N \geq 1 this is the usual N\prod_{p \mid N}(1+p^{-1})); the natural number \psi(N) is cast into \mathbb{Q}, and the division is division in \mathbb{Q}.

The second, ModularCurve.ssCountFormula N q, adds to the Eichler mass the two correction terms \frac{(2-\nu_2(q))\,\nu_2(N)}{4} + \frac{(2-\nu_3(q))\,\nu_3(N)}{3}, again with all counts cast into \mathbb{Q}. Here \nu_2(M) is ModularCurve.nuTwo M, the cardinality of the subtype of \mathbb{Z}/M cut out by x^2+1=0, and \nu_3(M) is ModularCurve.nuThree M, the cardinality of the subtype cut out by x^2+x+1=0; these are the counts of solutions of the two quadratic congruences modulo M that govern the elliptic points of order 2 and 3 on X_0(M).

Both declarations are arithmetic functions pure and simple: N and q are arbitrary natural numbers, with no primality of q, no coprimality \gcd(N,q)=1 and no positivity assumed, and neither definition asserts anything about an actual supersingular locus or a quaternionic class number. The interpretation of \nu_2,\nu_3 as elliptic-point counts and of \mathrm{ssCountFormula} as a count of supersingular points weighted by automorphisms is supplied elsewhere, by identities relating these expressions to ModularCurve.genusFormula.

Relation to Mathlib

Mathlib provides no Dedekind psi function, no elliptic-point counts \nu_2,\nu_3 and no Eichler mass formula; these, together with ModularCurve.dedekindPsi, ModularCurve.nuTwo, ModularCurve.nuThree and ModularCurve.genusFormula from the imported modules, are the project's own numerical definitions.

Where it is used

These expressions are the general-level form of the numerical count attached to the special fibre of X_0(Nq) at q, compared with the genus expression ModularCurve.genusFormula through the identity \mathrm{ssCountFormula}(N,q) = g(Nq) - 2g(N) + 1. They feed the computations of character-group and component-group ranks across levels used in the level-lowering step.

References

  1. G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Publications of the Mathematical Society of Japan 11, Princeton University Press, 1971, §1.6
  2. F. Diamond and J. Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005, §3.1
  3. M. Deuring, Die Typen der Multiplikatorenringe elliptischer Funktionenkörper, Abhandlungen aus dem Mathematischen Seminar der Universität Hamburg 14 (1941), 197–272

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

Source file: Definitions/Def_ModularCurve_EichlerMass.lean

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_GenusNumerics

set_option autoImplicit false

namespace ModularCurve

noncomputable def eichlerMass (N q : ℕ) : ℚ :=
  ((q : ℚ) - 1) * (dedekindPsi N : ℚ) / 12

noncomputable def ssCountFormula (N q : ℕ) : ℚ :=
  eichlerMass N q
    + (2 - (nuTwo q : ℚ)) * (nuTwo N : ℚ) / 4
    + (2 - (nuThree q : ℚ)) * (nuThree N : ℚ) / 3

end ModularCurve

Statements phrased using this module (7)