Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_LevelNFunctionField.lean

definition module

Fricke functions and the level- analytic coordinate ring

Fix a natural number N. For v = (v_0,v_1) \in (\mathbb{Z}/N\mathbb{Z})^2 and \tau in the upper half-plane, ModularCurve.LevelN.wp N v τ is ((2\pi i)^2)^{-1} times the value of the Weierstrass function PeriodPair.weierstrassP of the period pair PeriodPair.ofTau τ — the pair with periods \omega_1 = \tau, \omega_2 = 1, whose lattice is the \mathbb{Z}-span of \{\tau, 1\} — at the argument (v_0\tau + v_1)/N, where the integers v_0, v_1 are the canonical representatives (ZMod.val) of the two coordinates of v. The Fricke function ModularCurve.LevelN.fricke N v is the pointwise product of this with -E_4(\tau)E_6(\tau)/\bigl(2592\,\Delta(\tau)\bigr), where E_4, E_6 and \Delta are Mathlib's level-one Eisenstein series and discriminant; ModularCurve.LevelN.jAnalytic is the function \tau \mapsto E_4(\tau)^3/\Delta(\tau). No holomorphy, modularity or nonvanishing assertion is part of these definitions: each is simply a function \mathbb{H} \to \mathbb{C}, with the usual conventions for division by zero in \mathbb{C}.

The set ModularCurve.LevelN.generators N is obtained by inserting jAnalytic into the set of those functions g : \mathbb{H} \to \mathbb{C} for which there is a nonzero v \in (\mathbb{Z}/N\mathbb{Z})^2 with g = fricke N v; and ModularCurve.LevelN.ring N is the \mathbb{C}-subalgebra of the algebra of all functions \mathbb{H} \to \mathbb{C} (pointwise operations) generated by this set, i.e. \mathbb{C}[j, f_v : v \neq 0]. The accompanying lemmas record that jAnalytic and each fricke N v with v \neq 0 lie in the generating set and hence in the subalgebra, and ModularCurve.LevelN.jGen N packages jAnalytic as an element of that subalgebra, with its underlying function being jAnalytic again.

Relation to Mathlib

The Eisenstein series ModularForm.E₄, ModularForm.E₆ and ModularForm.discriminant and the upper half-plane are Mathlib's; the period-pair Weierstrass function is the project's own, and Mathlib has no Fricke functions or level-N function field, which are introduced here.

Where it is used

These functions provide the concrete analytic model of the modular curve of level N: the subalgebra ring N is the analytic coordinate ring whose fraction field serves as the field of modular functions of level N, and the Fricke functions are the coordinates in which the transformation law f_v(\gamma\tau) = f_{v\gamma}(\tau) and the invariance under \pm\Gamma(N) are stated elsewhere in the development.

References

  1. G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Princeton University Press, 1971, §6.1–§6.2
  2. S. Lang, Elliptic Functions, Graduate Texts in Mathematics 112, Springer, 1987, Ch. 6
  3. F. Diamond and J. Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005, §7.5

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_PeriodPair_Uniformization

set_option autoImplicit false

noncomputable section

open UpperHalfPlane

open scoped MatrixGroups

namespace ModularCurve.LevelN

def wp (N : ℕ) (v : Fin 2 → ZMod N) (τ : ℍ) : ℂ :=
  ((2 * (Real.pi : ℂ) * Complex.I) ^ 2)⁻¹ *
    PeriodPair.weierstrassP (PeriodPair.ofTau τ)
      ((((v 0).val : ℂ) * (τ : ℂ) + ((v 1).val : ℂ)) / (N : ℂ))

def fricke (N : ℕ) (v : Fin 2 → ZMod N) (τ : ℍ) : ℂ :=
  -(ModularForm.E₄ τ * ModularForm.E₆ τ / ModularForm.discriminant τ) / 2592 * wp N v τ

def jAnalytic (τ : ℍ) : ℂ :=
  ModularForm.E₄ τ ^ 3 / ModularForm.discriminant τ

def generators (N : ℕ) : Set (ℍ → ℂ) :=
  insert jAnalytic {g : ℍ → ℂ | ∃ v : Fin 2 → ZMod N, v ≠ 0 ∧ g = fricke N v}

def ring (N : ℕ) : Subalgebra ℂ (ℍ → ℂ) :=
  Algebra.adjoin ℂ (generators N)

theorem jAnalytic_mem_generators (N : ℕ) : jAnalytic ∈ generators N :=
  Set.mem_insert _ _

theorem fricke_mem_generators (N : ℕ) {v : Fin 2 → ZMod N} (hv : v ≠ 0) :
    fricke N v ∈ generators N :=
  Set.mem_insert_of_mem _ ⟨v, hv, rfl⟩

theorem jAnalytic_mem (N : ℕ) : jAnalytic ∈ ring N :=
  Algebra.subset_adjoin (jAnalytic_mem_generators N)

theorem fricke_mem (N : ℕ) {v : Fin 2 → ZMod N} (hv : v ≠ 0) : fricke N v ∈ ring N :=
  Algebra.subset_adjoin (fricke_mem_generators N hv)

def jGen (N : ℕ) : ring N :=
  ⟨jAnalytic, jAnalytic_mem N⟩

@[simp]
theorem coe_jGen (N : ℕ) : ((jGen N : ring N) : ℍ → ℂ) = jAnalytic :=
  rfl

end ModularCurve.LevelN

end

Statements phrased using this module (19)