Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_ComplexPlaceDictionaryOf.lean

definition module

Realisation of Laurent series and places dictionary for general level

Two things are defined, for an arbitrary subgroup \Gamma\le\mathrm{SL}_2(\mathbb{Z}) and an arbitrary intermediate field F_0 of \mathbb{Q}((q))/\mathbb{Q}.

First, realizeOf Γ x τ, for x\in\mathbb{C}((q)) and \tau\in\mathfrak H: if there exists a triple consisting of a weight k\in\mathbb{Z} and a pair (g,h) of modular forms of weight k on \Gamma with h(\tau)\neq0 and x\cdot \tilde h=\tilde g in \mathbb{C}((q)), where \tilde f denotes the period-one q-expansion qExpansion 1 of f viewed as a Laurent series, then the value is g(\tau)/h(\tau) for one such triple, picked by choice from the existence statement; otherwise the value is 0. Thus the definition does not assert independence of the choice, and realizeOf_of_not records the value 0 in the degenerate case. For \Gamma=\Gamma_0(N) this agrees with the fixed-level function realize N.

Second, the structure ComplexPlaceDictionaryOf Γ F₀, whose carrier field is \mathbb{C}F_0= laurentBaseChange ℂ F₀, the subfield of \mathbb{C}((q)) generated over \mathbb{C} by the coefficientwise image of F_0. A member consists of maps \mathrm{pt}:\mathfrak H\to places of \mathbb{C}F_0 over \mathbb{C} (valuation subrings containing \mathbb{C}, proper, and principal, hence discrete) and e:\mathfrak H\to\mathbb{N}, together with the following as fields: e_\tau>0; \mathrm{pt}(\gamma\tau)=\mathrm{pt}(\tau) for \gamma\in\Gamma; for every \tau and x\in\mathbb{C}F_0, membership x\in\mathcal O_{\mathrm{pt}(\tau)} holds precisely when z\mapsto\lVert\mathrm{realizeOf}\,\Gamma\,x\,z\rVert is bounded along the punctured neighbourhood filter of \tau in \mathfrak H; and for x\neq0 the meromorphic order at \tau\in\mathbb{C} of z\mapsto \mathrm{realizeOf}\,\Gamma\,x\,(\mathrm{ofComplex}\,z) equals e_\tau\cdot\mathrm{ord}_{\mathrm{pt}(\tau)}(x) in \mathbb{Z}\cup\{\infty\}. Auxiliary declarations restate invariance for an element of \mathrm{SL}_2(\mathbb{Z}) lying in \Gamma and e_\tau\neq0, and translate back and forth between this structure and ComplexPlaceDictionary N in the case \Gamma=\Gamma_0(N), F_0= modularFunctionFieldFull N, field by field.

Relation to Mathlib

Mathlib supplies ModularForm, qExpansion, meromorphicOrderAt and UpperHalfPlane.ofComplex; the notion of a place of a function field used here (AlgebraicCurve.Place) and the dictionary relating points of the upper half plane to such places are the project's own. ComplexPlaceDictionaryOf is the level-\Gamma, general-presentation form of the project's ComplexPlaceDictionary N, which it reduces to for \Gamma_0(N) and the field modularFunctionFieldFull N.

Where it is used

The dictionary is the interface through which complex-analytic information about modular curves — orders of vanishing, ramification at elliptic points, boundedness near a point — is transferred to valuation-theoretic statements about the function field presented by q-expansions at the cusp \infty, as needed for the algebraic geometry of modular curves in the modularity route to Fermat's Last Theorem. Keeping the subgroup \Gamma and the rational subfield F_0 as parameters allows one dictionary notion to serve the several presentations of these function fields used later.

References

  1. G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Publications of the Mathematical Society of Japan 11, Princeton University Press, 1971, Chapter 1
  2. F. Diamond and J. Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005, Chapters 2–3

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_LaurentCoeff
import Definitions.Def_AlgebraicCurve_DivisorClassGroup
import Definitions.Def_ModularCurve_ComplexPlaceDictionary

set_option autoImplicit false

noncomputable section

open UpperHalfPlane
open scoped MatrixGroups Topology

namespace ModularCurve

def realizeOf (Γ : Subgroup SL(2, ℤ)) (x : LaurentSeries ℂ) (τ : ℍ) : ℂ := by
  classical
  exact
    if H : ∃ p : (k : ℤ) × (ModularForm Γ k × ModularForm Γ k),
        (p.2.2 : ℍ → ℂ) τ ≠ 0 ∧
          x * ((qExpansion 1 (p.2.2 : ℍ → ℂ) : PowerSeries ℂ) : LaurentSeries ℂ) =
            ((qExpansion 1 (p.2.1 : ℍ → ℂ) : PowerSeries ℂ) : LaurentSeries ℂ)
    then (H.choose.2.1 : ℍ → ℂ) τ / (H.choose.2.2 : ℍ → ℂ) τ
    else 0

theorem realizeOf_def (Γ : Subgroup SL(2, ℤ)) (x : LaurentSeries ℂ) (τ : ℍ) :
    realizeOf Γ x τ = by
      classical
      exact
        if H : ∃ p : (k : ℤ) × (ModularForm Γ k × ModularForm Γ k),
            (p.2.2 : ℍ → ℂ) τ ≠ 0 ∧
              x * ((qExpansion 1 (p.2.2 : ℍ → ℂ) : PowerSeries ℂ) : LaurentSeries ℂ) =
                ((qExpansion 1 (p.2.1 : ℍ → ℂ) : PowerSeries ℂ) : LaurentSeries ℂ)
        then (H.choose.2.1 : ℍ → ℂ) τ / (H.choose.2.2 : ℍ → ℂ) τ
        else 0 :=
  rfl

theorem realizeOf_of_not (Γ : Subgroup SL(2, ℤ)) (x : LaurentSeries ℂ) (τ : ℍ)
    (h : ¬ ∃ p : (k : ℤ) × (ModularForm Γ k × ModularForm Γ k),
        (p.2.2 : ℍ → ℂ) τ ≠ 0 ∧
          x * ((qExpansion 1 (p.2.2 : ℍ → ℂ) : PowerSeries ℂ) : LaurentSeries ℂ) =
            ((qExpansion 1 (p.2.1 : ℍ → ℂ) : PowerSeries ℂ) : LaurentSeries ℂ)) :
    realizeOf Γ x τ = 0 := by
  classical
  rw [realizeOf_def]
  exact dif_neg h

structure ComplexPlaceDictionaryOf (Γ : Subgroup SL(2, ℤ))
    (F₀ : IntermediateField ℚ (LaurentSeries ℚ)) where

  pt : ℍ → AlgebraicCurve.Place ℂ (laurentBaseChange ℂ F₀)

  ramification : ℍ → ℕ

  ramification_pos : ∀ τ : ℍ, 0 < ramification τ

  pt_smul : ∀ (γ : Γ) (τ : ℍ), pt ((γ : SL(2, ℤ)) • τ) = pt τ

  mem_pt_iff : ∀ (τ : ℍ) (x : laurentBaseChange ℂ F₀),
    x ∈ (pt τ).toValuationSubring ↔
      Filter.IsBoundedUnder (· ≤ ·) (𝓝[≠] τ)
        (fun z : ℍ => ‖realizeOf Γ (x : LaurentSeries ℂ) z‖)

  meromorphicOrderAt_realizeOf : ∀ (τ : ℍ) (x : laurentBaseChange ℂ F₀), x ≠ 0 →
    meromorphicOrderAt (fun z : ℂ => realizeOf Γ (x : LaurentSeries ℂ) (ofComplex z)) (τ : ℂ) =
      (((ramification τ : ℤ) * (pt τ).ord x : ℤ) : WithTop ℤ)

namespace ComplexPlaceDictionaryOf

variable {Γ : Subgroup SL(2, ℤ)} {F₀ : IntermediateField ℚ (LaurentSeries ℚ)}

theorem pt_smul_of_mem (D : ComplexPlaceDictionaryOf Γ F₀) {γ : SL(2, ℤ)} (hγ : γ ∈ Γ) (τ : ℍ) :
    D.pt (γ • τ) = D.pt τ :=
  D.pt_smul ⟨γ, hγ⟩ τ

theorem ramification_ne_zero (D : ComplexPlaceDictionaryOf Γ F₀) (τ : ℍ) : D.ramification τ ≠ 0 :=
  (D.ramification_pos τ).ne'

end ComplexPlaceDictionaryOf

theorem realizeOf_gamma0 (N : ℕ) (x : LaurentSeries ℂ) (τ : ℍ) :
    realizeOf (CongruenceSubgroup.Gamma0 N) x τ = realize N x τ :=
  rfl

def ComplexPlaceDictionaryOf.ofGamma0 {N : ℕ} [NeZero N] (D : ComplexPlaceDictionary N) :
    ComplexPlaceDictionaryOf (CongruenceSubgroup.Gamma0 N) (modularFunctionFieldFull N) where
  pt := D.pt
  ramification := D.ramification
  ramification_pos := D.ramification_pos
  pt_smul := D.pt_smul
  mem_pt_iff := D.mem_pt_iff
  meromorphicOrderAt_realizeOf := D.meromorphicOrderAt_realize

def ComplexPlaceDictionaryOf.toGamma0 {N : ℕ} [NeZero N]
    (D : ComplexPlaceDictionaryOf (CongruenceSubgroup.Gamma0 N) (modularFunctionFieldFull N)) :
    ComplexPlaceDictionary N where
  pt := D.pt
  ramification := D.ramification
  ramification_pos := D.ramification_pos
  pt_smul := D.pt_smul
  mem_pt_iff := D.mem_pt_iff
  meromorphicOrderAt_realize := D.meromorphicOrderAt_realizeOf

@[simp]
theorem ComplexPlaceDictionaryOf.pt_ofGamma0 {N : ℕ} [NeZero N] (D : ComplexPlaceDictionary N) :
    (ComplexPlaceDictionaryOf.ofGamma0 D).pt = D.pt :=
  rfl

@[simp]
theorem ComplexPlaceDictionaryOf.pt_toGamma0 {N : ℕ} [NeZero N]
    (D : ComplexPlaceDictionaryOf (CongruenceSubgroup.Gamma0 N) (modularFunctionFieldFull N)) :
    D.toGamma0.pt = D.pt :=
  rfl

end ModularCurve

end

Statements phrased using this module (36)