Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularForm_AtkinLehnerDatum.lean

definition module

Atkin–Lehner data and the bare Atkin–Lehner slash operator

For natural numbers M and q, the structure ModularForm.AtkinLehnerDatum M q packages, as data, a cofactor R : ℕ together with a proof that M = qR, and a pair of integers a, b together with a proof of the Bézout relation qa - Rb = 1 (such a datum exists exactly when q divides M exactly, i.e. \gcd(q,R)=1). Under a NeZero M assumption both q and R are positive. Attached to a datum W is the integral matrix W.\mathrm{mat} = \begin{pmatrix} qa & b \\ qR & q\end{pmatrix}, whose determinant is q (det_mat) and whose lower-left entry is M (mat_lowerLeft). The square of this matrix is computed exactly: mat_sq states W.\mathrm{mat}^2 = q \cdot W.\mathrm{sqUnit}, where sqUnit is the explicit integral matrix \begin{pmatrix} qa^2 + Rb & b(a+1) \\ qR(a+1) & Rb + q\end{pmatrix}; its determinant is 1 (det_sqUnit), so it defines an element sqUnitSL of \mathrm{SL}_2(\mathbb{Z}), and its lower-left entry is M(a+1), whence sqUnitSL_mem places it in Mathlib's Gamma0 M.

The same matrix is then transported to the real and rational general linear groups: alGL : GL (Fin 2) ℝ and alGLQ : GL (Fin 2) ℚ are the entrywise images of W.\mathrm{mat}, invertible because the determinant q is nonzero; val_det_alGL records that the determinant of alGL is q as a real number, det_alGL_pos that it is positive, and consequently σ_alGL_apply that the twist \sigma of Mathlib's slash action acts as the identity on \mathbb{C} for this matrix. alGLQ_map_castHom identifies the image of alGLQ under \mathbb{Q} \hookrightarrow \mathbb{R} with alGL. Finally, for a weight k \in \mathbb{Z} and an arbitrary function f : \mathbb{H} \to \mathbb{C}, ModularForm.alSlash W k f is defined to be the weight-k slash f \mid[k] W.\mathrm{alGL}; this is additive in f and, because \sigma is trivial here, genuinely \mathbb{C}-linear: alSlash_smul gives w(c \cdot f) = c \cdot w(f) with no conjugation.

Relation to Mathlib

Mathlib supplies the ambient notions used here — the weight-k slash action of GL (Fin 2) ℝ on functions on the upper half plane together with its conjugation twist σ, and the congruence subgroup Gamma0 — but has no notion of Atkin–Lehner datum or Atkin–Lehner operator; the structure and the operator alSlash are the project's own.

Where it is used

These definitions are the basis for the Atkin–Lehner operators on M_k(\Gamma_0(M)) and S_k(\Gamma_0(M)) used in the level-lowering part of the argument: the relation W.\mathrm{mat}^2 = q\,\cdot (element of \Gamma_0(M)) yields w_q^2 = q^{k-2}, and together with the trace map from level M to level R this leads to the statement that a newform of level exactly divisible by q has a_q^2 = 1. Note that the operator here is the slash by one specific chosen matrix, so it depends on the datum as data; independence of the choice is a statement about modular forms rather than about arbitrary functions.

References

  1. A. O. L. Atkin and J. Lehner, Hecke operators on \Gamma_0(m), Mathematische Annalen 185 (1970), 134–160
  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_ModularForm_AtkinLehnerDatum.lean

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib

set_option autoImplicit false

open Matrix UpperHalfPlane CongruenceSubgroup
open scoped MatrixGroups ModularForm

noncomputable section

namespace ModularForm

variable (M q : ℕ)

structure AtkinLehnerDatum : Type where

  R : ℕ

  hM : M = q * R

  a : ℤ

  b : ℤ

  bezout : (q : ℤ) * a - (R : ℤ) * b = 1

namespace AtkinLehnerDatum

variable {M q : ℕ} (W : AtkinLehnerDatum M q)

lemma hM_int : (M : ℤ) = (q : ℤ) * (W.R : ℤ) := by exact_mod_cast W.hM

include W in

lemma q_pos [NeZero M] : 0 < q := by
  rcases Nat.eq_zero_or_pos q with h | h
  · exact absurd (W.hM.trans (Nat.mul_eq_zero.mpr (Or.inl h))) (NeZero.ne M)
  · exact h

include W in

lemma R_pos [NeZero M] : 0 < W.R := by
  rcases Nat.eq_zero_or_pos W.R with h | h
  · exact absurd (W.hM.trans (Nat.mul_eq_zero.mpr (Or.inr h))) (NeZero.ne M)
  · exact h

def mat : Matrix (Fin 2) (Fin 2) ℤ := !![(q : ℤ) * W.a, W.b; (q : ℤ) * (W.R : ℤ), (q : ℤ)]

@[simp] lemma det_mat : W.mat.det = (q : ℤ) := by
  rw [mat, Matrix.det_fin_two_of]
  linear_combination (q : ℤ) * W.bezout

lemma mat_lowerLeft : W.mat 1 0 = (M : ℤ) := by
  rw [mat, W.hM_int]
  simp

def sqUnit : Matrix (Fin 2) (Fin 2) ℤ :=
  !![(q : ℤ) * W.a ^ 2 + (W.R : ℤ) * W.b, W.b * (W.a + 1);
     (q : ℤ) * (W.R : ℤ) * (W.a + 1), (W.R : ℤ) * W.b + (q : ℤ)]

theorem mat_sq : W.mat * W.mat = (q : ℤ) • W.sqUnit := by
  rw [mat, sqUnit, Matrix.mul_fin_two]
  refine Matrix.ext fun i j => ?_
  fin_cases i <;> fin_cases j
  · show (q : ℤ) * W.a * ((q : ℤ) * W.a) + W.b * ((q : ℤ) * (W.R : ℤ))
      = (q : ℤ) * ((q : ℤ) * W.a ^ 2 + (W.R : ℤ) * W.b)
    ring
  · show (q : ℤ) * W.a * W.b + W.b * (q : ℤ) = (q : ℤ) * (W.b * (W.a + 1))
    ring
  · show (q : ℤ) * (W.R : ℤ) * ((q : ℤ) * W.a) + (q : ℤ) * ((q : ℤ) * (W.R : ℤ))
      = (q : ℤ) * ((q : ℤ) * (W.R : ℤ) * (W.a + 1))
    ring
  · show (q : ℤ) * (W.R : ℤ) * W.b + (q : ℤ) * (q : ℤ)
      = (q : ℤ) * ((W.R : ℤ) * W.b + (q : ℤ))
    ring

@[simp] lemma det_sqUnit : W.sqUnit.det = 1 := by
  rw [sqUnit, Matrix.det_fin_two_of]
  linear_combination ((q : ℤ) * W.a - (W.R : ℤ) * W.b + 1) * W.bezout

def sqUnitSL : SL(2, ℤ) := ⟨W.sqUnit, W.det_sqUnit⟩

@[simp] lemma sqUnitSL_coe : (W.sqUnitSL : Matrix (Fin 2) (Fin 2) ℤ) = W.sqUnit := rfl

lemma sqUnitSL_mem : W.sqUnitSL ∈ Gamma0 M := by
  rw [Gamma0_mem]
  show (((W.sqUnit 1 0 : ℤ) : ZMod M) = 0)
  have h : W.sqUnit 1 0 = (M : ℤ) * (W.a + 1) := by
    rw [sqUnit, W.hM_int]; simp
  rw [h]
  push_cast
  simp

def alGL [NeZero M] : GL (Fin 2) ℝ :=
  Matrix.GeneralLinearGroup.mkOfDetNeZero (W.mat.map (algebraMap ℤ ℝ)) (by
    have h : ((W.mat).map (algebraMap ℤ ℝ)).det = (algebraMap ℤ ℝ) W.mat.det := by
      rw [← RingHom.mapMatrix_apply, ← RingHom.map_det]
    rw [h, W.det_mat]
    simpa using W.q_pos.ne')

@[simp] lemma alGL_coe [NeZero M] :
    (W.alGL : Matrix (Fin 2) (Fin 2) ℝ) = (W.mat).map (algebraMap ℤ ℝ) := rfl

lemma alGL_entry [NeZero M] (i j : Fin 2) :
    W.alGL i j = algebraMap ℤ ℝ (W.mat i j) := by
  show ((W.alGL : Matrix (Fin 2) (Fin 2) ℝ)) i j = _
  rw [alGL_coe, Matrix.map_apply]

lemma val_det_alGL [NeZero M] : ((W.alGL).det : ℝ) = (q : ℝ) := by
  rw [Matrix.GeneralLinearGroup.val_det_apply, alGL_coe]
  have h : ((W.mat).map (algebraMap ℤ ℝ)).det = (algebraMap ℤ ℝ) W.mat.det := by
    rw [← RingHom.mapMatrix_apply, ← RingHom.map_det]
  rw [h, W.det_mat]
  simp

lemma det_alGL_pos [NeZero M] : 0 < ((W.alGL).det : ℝ) := by
  rw [val_det_alGL]
  exact_mod_cast W.q_pos

lemma σ_alGL_apply [NeZero M] (z : ℂ) : σ W.alGL z = z := by
  rw [UpperHalfPlane.σ, if_pos W.det_alGL_pos]
  simp

def alGLQ [NeZero M] : GL (Fin 2) ℚ :=
  Matrix.GeneralLinearGroup.mkOfDetNeZero (W.mat.map (algebraMap ℤ ℚ)) (by
    have h : ((W.mat).map (algebraMap ℤ ℚ)).det = (algebraMap ℤ ℚ) W.mat.det := by
      rw [← RingHom.mapMatrix_apply, ← RingHom.map_det]
    rw [h, W.det_mat]
    simpa using W.q_pos.ne')

lemma alGLQ_map_castHom [NeZero M] : (W.alGLQ).map (Rat.castHom ℝ) = W.alGL := by
  apply Units.ext
  show (Rat.castHom ℝ).mapMatrix ((W.alGLQ : Matrix (Fin 2) (Fin 2) ℚ))
      = (W.alGL : Matrix (Fin 2) (Fin 2) ℝ)
  show (Rat.castHom ℝ).mapMatrix ((W.mat).map (algebraMap ℤ ℚ))
      = (W.mat).map (algebraMap ℤ ℝ)
  rw [RingHom.mapMatrix_apply, Matrix.map_map]
  congr 1

end AtkinLehnerDatum

def alSlash {M q : ℕ} (W : AtkinLehnerDatum M q) (k : ℤ) [NeZero M] (f : ℍ → ℂ) : ℍ → ℂ :=
  f ∣[k] W.alGL

lemma alSlash_def {M q : ℕ} (W : AtkinLehnerDatum M q) (k : ℤ) [NeZero M] (f : ℍ → ℂ) :
    alSlash W k f = f ∣[k] W.alGL := rfl

lemma alSlash_add {M q : ℕ} (W : AtkinLehnerDatum M q) (k : ℤ) [NeZero M] (f g : ℍ → ℂ) :
    alSlash W k (f + g) = alSlash W k f + alSlash W k g := by
  simp only [alSlash, SlashAction.add_slash]

lemma alSlash_smul {M q : ℕ} (W : AtkinLehnerDatum M q) (k : ℤ) [NeZero M] (c : ℂ) (f : ℍ → ℂ) :
    alSlash W k (c • f) = c • alSlash W k f := by
  simp only [alSlash, ModularForm.smul_slash, AtkinLehnerDatum.σ_alGL_apply]

end ModularForm

end

Statements phrased using this module (44)