Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_GenusNumerics.lean

definition module

Elliptic point counts, cusp count and genus formula for

Four arithmetic functions of a natural number N are introduced, together with one evaluation lemma.

ModularCurve.nuTwo N is the cardinality (as a Nat.card) of the subtype of \mathbb{Z}/N consisting of those x with x^2+1=0, and ModularCurve.nuThree N is the cardinality of the subtype of \mathbb{Z}/N consisting of those x with x^2+x+1=0; classically these are the numbers of elliptic points of order 2 and of order 3 on X_0(N). ModularCurve.cuspCount N is defined as the finite sum \sum_{d \mid N} \varphi\bigl(\gcd(d, N/d)\bigr) over the divisors of N, with \varphi Euler's totient; ModularCurve.cuspCount_one records that this equals 1 for N = 1.

ModularCurve.genusFormula N is the rational number 1 + \frac{\psi(N)}{12} - \frac{\nu_2(N)}{4} - \frac{\nu_3(N)}{3} - \frac{\nu_\infty(N)}{2}, where \nu_2, \nu_3, \nu_\infty are nuTwo, nuThree, cuspCount and \psi(N) is ModularCurve.dedekindPsi N, itself defined as the sum \sum_{d \mid N,\ d \text{ squarefree}} N/d, i.e. N \prod_{p \mid N}(1 + 1/p), the index of \Gamma_0(N) in \mathrm{SL}_2(\mathbb{Z}).

Thus genusFormula is a purely arithmetic expression in N, taking values in \mathbb{Q}; it is defined as the right-hand side of the classical Riemann–Hurwitz computation for the covering X_0(N) \to X(1), and no integrality assertion, nor any identification with the genus of a curve, is part of the definitions themselves.

Relation to Mathlib

Mathlib supplies the ingredients used here (ZMod, Nat.divisors, Nat.totient, Nat.card) but has no counts of elliptic points or cusps for \Gamma_0(N) and no genus formula for X_0(N); these functions, like ModularCurve.dedekindPsi, are the project's own.

Where it is used

These four functions are the numerical inputs to the genus and ramification computations for the modular curves X_0(N) used throughout the project's treatment of X_0(N), in particular for the small levels occurring after level lowering.

References

  1. F. Diamond and J. Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005, §3.1
  2. G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Princeton University Press, 1971, Prop. 1.43

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_GenusNumerics.lean

Imports

Imported by

Declarations

Source

import Mathlib.NumberTheory.LegendreSymbol.Basic ↗
import Mathlib.FieldTheory.Finite.Basic ↗
import Mathlib.Data.Nat.Totient ↗
import Mathlib.NumberTheory.Divisors ↗
import Definitions.Def_ModularCurve_X0

namespace ModularCurve

noncomputable def nuTwo (N : ℕ) : ℕ := Nat.card {x : ZMod N // x ^ 2 + 1 = 0}

noncomputable def nuThree (N : ℕ) : ℕ := Nat.card {x : ZMod N // x ^ 2 + x + 1 = 0}

def cuspCount (N : ℕ) : ℕ :=
  ∑ d ∈ N.divisors, Nat.totient (Nat.gcd d (N / d))

@[simp]
lemma cuspCount_one : cuspCount 1 = 1 := by
  simp [cuspCount]

noncomputable def genusFormula (N : ℕ) : ℚ :=
  1 + (dedekindPsi N : ℚ) / 12 - (nuTwo N : ℚ) / 4 - (nuThree N : ℚ) / 3
    - (cuspCount N : ℚ) / 2

end ModularCurve

Statements phrased using this module (116)