Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_OmegaOf.lean

definition module

The differential attached to a q-expansion

For a level N, a function f : \mathbb{H} \to \mathbb{C} and a ring homomorphism \sigma : \overline{\mathbb{Q}} \to \mathbb{C} (with \overline{\mathbb{Q}} = AlgebraicClosure ℚ), ModularCurve.omegaOf N f σ is an element of \Omega_{\bar F_N/\overline{\mathbb{Q}}}, where \bar F_N = modularFunctionFieldBar N is the subfield of \overline{\mathbb{Q}}((q)) generated over \overline{\mathbb{Q}} by the coefficientwise images of the q-expansions \mathrm{qExpand}_d\, j for d \mid N, and \Omega is Mathlib's module of Kähler differentials. The definition is by cases on the existence of a witness: if some x \in \bar F_N satisfies \mathrm{coeffMap}\,\sigma\bigl(x \cdot \theta(\tilde j)\bigr) = \mathrm{qExpansion}\,1\,f as Laurent series over \mathbb{C} — here \tilde j is the q-series jq of the j-function pushed into \overline{\mathbb{Q}}((q)) coefficientwise, \theta is the operator g \mapsto q\,dg/dq of thetaL, and \mathrm{coeffMap}\,\sigma applies \sigma to each coefficient — then omegaOf N f σ is x \cdot D_{\overline{\mathbb{Q}}}(\tilde j), the scalar multiple by x of the universal derivation applied to \tilde j \in \bar F_N; otherwise it is 0. Thus no \sigma-rationality hypothesis on f appears among the binders: data for which no witness exists receives the value 0, and only \mathrm{qExpansion}\,1\,f enters the body.

Three theorems give the interface. omegaOf_witness_unique states that a witness x is unique, since \mathrm{coeffMap}\,\sigma is injective for injective \sigma and \theta(\tilde j) \neq 0. omegaOf_eq_smul_D_of_coeffMap_eq states that any witness x computes the value, \mathrm{omegaOf}\,N\,f\,\sigma = x \cdot D(\tilde j), and omegaOf_eq_zero_of_not_exists records the second branch. Two auxiliary facts supply the nonvanishing: the coefficient of q^{-1} in \theta(\tilde j) equals -1, whence \theta(\tilde j) \neq 0.

Relation to Mathlib

Mathlib provides the module of Kähler differentials (KaehlerDifferential) and the q-expansion of a modular form (qExpansion); the function fields of modular curves as subfields of Laurent series, the coefficientwise maps coeffMap/coeffEmb, the operator thetaL, and the differential attached to a q-expansion are the project's own notions.

Where it is used

The element omegaOf N f σ realises a weight-2 form on \Gamma_0(N) as a differential on the modular curve over \overline{\mathbb{Q}}, the bridge between modular forms and the Jacobian of X_0(N) whose torsion supplies the Galois representations used in the Frey curve argument.

References

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

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

Imports

Theorems imported by this definition module

Imported by

  • no other definition module

Declarations

Source

import Definitions.Def_ModularCurve_QAdicPlace
import Definitions.Def_ModularCurve_ArithmeticGalois
import Definitions.Def_ModularCurve_QExpansionDiff
import Theorems.Thm_ModularCurve_theta_coeff
import Theorems.Thm_ModularCurve_coeffMap_injective
import Mathlib.NumberTheory.ModularForms.QExpansion ↗

set_option autoImplicit false

noncomputable section

open UpperHalfPlane

namespace ModularCurve

variable (N : ℕ) [NeZero N]

open scoped Classical in

def omegaOf (f : ℍ → ℂ) (σ : AlgebraicClosure ℚ →+* ℂ) :
    Ω[modularFunctionFieldBar N⁄AlgebraicClosure ℚ] :=
  if h : ∃ x : modularFunctionFieldBar N,
      coeffMap σ ((x : LaurentSeries (AlgebraicClosure ℚ)) *
          thetaL (AlgebraicClosure ℚ) (coeffEmb (AlgebraicClosure ℚ) jq)) =
        ((qExpansion 1 f : PowerSeries ℂ) : LaurentSeries ℂ)
  then
    h.choose •
      KaehlerDifferential.D (AlgebraicClosure ℚ) (modularFunctionFieldBar N)
        (⟨coeffEmb (AlgebraicClosure ℚ) jq,
          coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) (jq_mem_full N)⟩ :
          modularFunctionFieldBar N)
  else 0

private theorem theta_coeffEmb_jq_coeff_neg_one :
    (thetaL (AlgebraicClosure ℚ) (coeffEmb (AlgebraicClosure ℚ) jq)).coeff (-1 : ℤ) = -1 := by
  rw [thetaL_apply, theta_coeff, coeffEmb_coeff, coeff_jq_neg_one, map_one]
  norm_num

private theorem thetaL_coeffEmb_jq_ne_zero :
    thetaL (AlgebraicClosure ℚ) (coeffEmb (AlgebraicClosure ℚ) jq) ≠ 0 := by
  intro h0
  have h := theta_coeffEmb_jq_coeff_neg_one
  rw [h0] at h
  simp at h

omit [NeZero N] in

theorem omegaOf_witness_unique (f : ℍ → ℂ)
    (σ : AlgebraicClosure ℚ →+* ℂ) {x y : modularFunctionFieldBar N}
    (hx : coeffMap σ ((x : LaurentSeries (AlgebraicClosure ℚ)) *
        thetaL (AlgebraicClosure ℚ) (coeffEmb (AlgebraicClosure ℚ) jq)) =
      ((qExpansion 1 f : PowerSeries ℂ) : LaurentSeries ℂ))
    (hy : coeffMap σ ((y : LaurentSeries (AlgebraicClosure ℚ)) *
        thetaL (AlgebraicClosure ℚ) (coeffEmb (AlgebraicClosure ℚ) jq)) =
      ((qExpansion 1 f : PowerSeries ℂ) : LaurentSeries ℂ)) : x = y := by
  have h1 : (x : LaurentSeries (AlgebraicClosure ℚ)) *
        thetaL (AlgebraicClosure ℚ) (coeffEmb (AlgebraicClosure ℚ) jq)
      = (y : LaurentSeries (AlgebraicClosure ℚ)) *
        thetaL (AlgebraicClosure ℚ) (coeffEmb (AlgebraicClosure ℚ) jq) :=
    coeffMap_injective σ.injective (hx.trans hy.symm)
  have h2 : (x : LaurentSeries (AlgebraicClosure ℚ)) = y :=
    mul_right_cancel₀ thetaL_coeffEmb_jq_ne_zero h1
  exact_mod_cast h2

theorem omegaOf_eq_smul_D_of_coeffMap_eq (f : ℍ → ℂ)
    (σ : AlgebraicClosure ℚ →+* ℂ) {x : modularFunctionFieldBar N}
    (hx : coeffMap σ ((x : LaurentSeries (AlgebraicClosure ℚ)) *
        thetaL (AlgebraicClosure ℚ) (coeffEmb (AlgebraicClosure ℚ) jq)) =
      ((qExpansion 1 f : PowerSeries ℂ) : LaurentSeries ℂ)) :
    omegaOf N f σ =
      x • KaehlerDifferential.D (AlgebraicClosure ℚ) (modularFunctionFieldBar N)
        (⟨coeffEmb (AlgebraicClosure ℚ) jq,
          coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) (jq_mem_full N)⟩ :
          modularFunctionFieldBar N) := by
  have h : ∃ z : modularFunctionFieldBar N,
      coeffMap σ ((z : LaurentSeries (AlgebraicClosure ℚ)) *
          thetaL (AlgebraicClosure ℚ) (coeffEmb (AlgebraicClosure ℚ) jq)) =
        ((qExpansion 1 f : PowerSeries ℂ) : LaurentSeries ℂ) := ⟨x, hx⟩
  unfold omegaOf
  rw [dif_pos h, omegaOf_witness_unique N f σ h.choose_spec hx]

theorem omegaOf_eq_zero_of_not_exists (f : ℍ → ℂ)
    (σ : AlgebraicClosure ℚ →+* ℂ)
    (h : ¬ ∃ x : modularFunctionFieldBar N,
        coeffMap σ ((x : LaurentSeries (AlgebraicClosure ℚ)) *
            thetaL (AlgebraicClosure ℚ) (coeffEmb (AlgebraicClosure ℚ) jq)) =
          ((qExpansion 1 f : PowerSeries ℂ) : LaurentSeries ℂ)) :
    omegaOf N f σ = 0 := by
  unfold omegaOf
  rw [dif_neg h]

end ModularCurve

end

Statements phrased using this module (1)