Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_CuspidalClass.lean

definition module

Fricke involution, the cusps , , and the cuspidal class

Working with a fixed level N\ge 1 ([NeZero N]), this module produces closed terms, for every such N, for the Fricke involution and the cuspidal divisor class of X_0(N) over \overline{\mathbb{Q}}, at the grain of function fields and places. First, frickeInvolutionBar N is the base change to \overline{\mathbb{Q}}, via the project's geomAut, of the all-divisors Fricke involution frickeInvolutionFull N of modularFunctionFieldFull N; it is an \overline{\mathbb{Q}}-algebra automorphism of modularFunctionFieldBar N. Next, cuspZeroBar N is defined as the image of the cusp at infinity under this automorphism, i.e. the place frickeInvolutionBar N • cuspInftyBar N of modularFunctionFieldBar N over \overline{\mathbb{Q}} — so the cusp 0 is by definition w_N(\infty), not characterised intrinsically. The divisor cuspidalDivisor N is the formal difference Finsupp.single (cuspZeroBar N) 1 - Finsupp.single (cuspInftyBar N) 1, that is (0)-(\infty). The one substantive lemma, degree_cuspidalDivisor, shows its degree is 0; the proof uses only that a place and its translate under an automorphism have equal degree (Place.deg_smul), the individual degrees being left uncomputed. Accordingly cuspidalDivisor₀ N bundles the divisor with a proof of membership in Divisor.degZero, and cuspidalClass N : JZero N is its class Pic0.mk (cuspidalDivisor₀ N) in the degree-zero divisor class group of modularFunctionFieldBar N over \overline{\mathbb{Q}}. The remaining declarations (frickeInvolutionBar_def, cuspZeroBar_def, cuspidalDivisor_def, coe_cuspidalDivisor₀, cuspidalClass_def) are unfolding lemmas restating the definitions. The definitions are total: nothing here asserts that frickeInvolutionFull N really is a Fricke involution, nor that the two cusps are distinct, so downstream statements about these objects must carry those hypotheses separately.

Relation to Mathlib

Mathlib has no modular curves, cusps, Fricke involutions or divisor class groups of function fields in this form; the ambient notions (Place, Divisor, Divisor.degZero, Pic0, geomAut, modularFunctionFieldFull, cuspInftyBar) are all the project's own, built on Mathlib's Finsupp and AlgEquiv.

Where it is used

The class c_N=[(0)-(\infty)] in J_0(N)(\overline{\mathbb{Q}}) is the cuspidal class whose torsion order and Galois behaviour enter the level-lowering and Galois-representation arguments for J_0(N); these terms are the objects on which the subsequent statements about the divisor of the Fricke-antiinvariant modular unit, the two-cusp enumeration at prime level, and the Hecke action on J_0(N) are phrased.

References

  1. B. Mazur, Modular curves and the Eisenstein ideal, Publications Mathématiques de l'IHÉS 47 (1977), 33–186
  2. G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Publications of the Mathematical Society of Japan 11, Princeton University Press, 1971
  3. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154

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

Imports

Imported by

Declarations

Source

import Definitions.Def_ModularCurve_AtkinLehner
import Definitions.Def_ModularCurve_GeometricBaseChange

set_option autoImplicit false

noncomputable section

open AlgebraicCurve

namespace ModularCurve

variable (N : ℕ) [NeZero N]

def frickeInvolutionBar :
    modularFunctionFieldBar N ≃ₐ[AlgebraicClosure ℚ] modularFunctionFieldBar N :=
  geomAut (AlgebraicClosure ℚ) (modularFunctionFieldFull N) (frickeInvolutionFull N)

theorem frickeInvolutionBar_def :
    frickeInvolutionBar N =
      geomAut (AlgebraicClosure ℚ) (modularFunctionFieldFull N) (frickeInvolutionFull N) :=
  rfl

def cuspZeroBar : Place (AlgebraicClosure ℚ) (modularFunctionFieldBar N) :=
  frickeInvolutionBar N • cuspInftyBar N

theorem cuspZeroBar_def : cuspZeroBar N = frickeInvolutionBar N • cuspInftyBar N := rfl

def cuspidalDivisor : Divisor (AlgebraicClosure ℚ) (modularFunctionFieldBar N) :=
  Finsupp.single (cuspZeroBar N) 1 - Finsupp.single (cuspInftyBar N) 1

theorem cuspidalDivisor_def :
    cuspidalDivisor N = Finsupp.single (cuspZeroBar N) 1 - Finsupp.single (cuspInftyBar N) 1 :=
  rfl

theorem degree_cuspidalDivisor : Divisor.degree (cuspidalDivisor N) = 0 := by
  rw [cuspidalDivisor_def, map_sub, Divisor.degree_single, Divisor.degree_single, cuspZeroBar_def,
    Place.deg_smul, sub_self]

def cuspidalDivisor₀ :
    Divisor.degZero (K := AlgebraicClosure ℚ) (F := modularFunctionFieldBar N) :=
  ⟨cuspidalDivisor N, Divisor.mem_degZero.mpr (degree_cuspidalDivisor N)⟩

@[simp]
theorem coe_cuspidalDivisor₀ :
    (cuspidalDivisor₀ N : Divisor (AlgebraicClosure ℚ) (modularFunctionFieldBar N)) =
      cuspidalDivisor N :=
  rfl

def cuspidalClass : JZero N := Pic0.mk (cuspidalDivisor₀ N)

theorem cuspidalClass_def : cuspidalClass N = Pic0.mk (cuspidalDivisor₀ N) := rfl

end ModularCurve

end

Statements phrased using this module (180)

… and 30 more statements (search for the module name to find them).