Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_HeckeDifferential.lean

definition module

Euler derivation, q-expansion of differentials, Hecke action

Over a commutative ring R, ModularCurve.qEulerFun sends a Laurent series x\in R((q)) to the series with coefficients n\,x_n, and ModularCurve.qEuler packages this as a derivation of R((q)) over R, namely \vartheta = q\,d/dq; the Leibniz rule is verified coefficientwise, and qEuler_single records \vartheta(rq^n) = n r q^n. Auxiliary lemmas give the support inclusion \operatorname{supp}(\vartheta x)\subseteq\operatorname{supp}(x) and the identity \operatorname{algebraMap}(c)=\mathrm{single}\,0\,c.

For a field L and an intermediate field F of L\subseteq L((q)), ModularCurve.qEulerOn is the restriction of \vartheta to F, viewed as an L-derivation F\to L((q)), and ModularCurve.diffQExp is its universal factorisation through the module of Kähler differentials: the F-linear map \Omega_{F/L}\to L((q)) with d x\mapsto \vartheta x, hence f\,dx\mapsto f\cdot\vartheta x. Thus a differential written as h\,dq/q is sent to h. Instance declarations supply the L-algebra structure on F, the L-module structure and scalar tower on \Omega_{F/L}, and the scalar tower L–F–L((q)).

In the modular setting, for a field L containing \mathbb{Q} and positive integers N,\ell, ModularCurve.heckeDiffAlong is the endomorphism of \Omega_{L\cdot F_N/L} given by Differential.correspondence applied to the pair (\beta,\alpha), i.e. the pullback along \alpha (the inclusion of the base-changed full modular function field of level N into that of level N\ell) followed by the trace along \beta (the substitution q\mapsto q^{\ell}); the trace leg is defined via the formally étale base-change equivalence when the extension along \beta is separable, and is 0 otherwise. ModularCurve.heckeDiffBar specialises this to L=\overline{\mathbb{Q}} and a prime \ell, an \overline{\mathbb{Q}}-linear endomorphism of \Omega_{\overline{\mathbb{Q}}F_N/\overline{\mathbb{Q}}}. Finally ModularCurve.diffQExpBar and ModularCurve.regularDifferentialsBar abbreviate, at L=\overline{\mathbb{Q}}, the q-expansion map and the submodule of differentials \omega such that at every place v one has \omega = f\cdot d\pi_v with f in the valuation ring of v and \pi_v the chosen uniformiser.

Relation to Mathlib

Mathlib supplies LaurentSeries, Derivation and KaehlerDifferential; the derivation q\,d/dq on R((q)), the induced q-expansion map on Kähler differentials, and the pullback/trace correspondence on differentials along an algebra map (from the project's AlgebraicCurve.Differential) are the project's own notions.

Where it is used

The q-expansion map on differentials is what converts regular differentials on the modular curve into power series, giving the dictionary between H^0(\Omega^1) and weight-two cusp forms; heckeDiffBar is the Hecke correspondence acting on differentials, the cotangent counterpart of the Hecke action on \mathrm{Pic}^0 of the modular curve used throughout the modularity and level-lowering arguments.

References

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

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_HeckeOperator
import Definitions.Def_AlgebraicCurve_DifferentialPushPull
import Definitions.Def_AlgebraicCurve_RegularDifferentials

set_option autoImplicit false

noncomputable section

open HahnSeries KaehlerDifferential AlgebraicCurve

namespace ModularCurve

section Euler

variable (R : Type*) [CommRing R]

def qEulerFun (x : LaurentSeries R) : LaurentSeries R where
  coeff n := (n : R) * x.coeff n
  isPWO_support' := x.isPWO_support.mono fun n hn => by
    simp only [Function.mem_support, ne_eq] at hn ⊢
    intro h
    exact hn (by rw [h, mul_zero])

@[simp] theorem qEulerFun_coeff (x : LaurentSeries R) (n : ℤ) :
    (qEulerFun R x).coeff n = (n : R) * x.coeff n := rfl

theorem support_qEulerFun_subset (x : LaurentSeries R) :
    (qEulerFun R x).support ⊆ x.support := fun n hn => by
  contrapose! hn
  simp only [mem_support, ne_eq, not_not] at hn ⊢
  rw [qEulerFun_coeff, hn, mul_zero]

theorem algebraMap_laurentSeries_apply_alt (c : R) :
    algebraMap R (LaurentSeries R) c = single 0 c := by
  have h1 : algebraMap R (PowerSeries R) c = PowerSeries.C c := by simp
  rw [HahnSeries.algebraMap_apply', h1, HahnSeries.ofPowerSeries_C]
  rfl

def qEuler : Derivation R (LaurentSeries R) (LaurentSeries R) where
  toFun := qEulerFun R
  map_add' x y := by
    ext n
    simp only [qEulerFun_coeff, coeff_add, mul_add]
  map_smul' r x := by
    ext n
    simp only [RingHom.id_apply, qEulerFun_coeff]
    rw [Algebra.smul_def, algebraMap_laurentSeries_apply_alt, coeff_single_zero_mul, HahnSeries.coeff_smul,
      qEulerFun_coeff, smul_eq_mul]
    ring
  map_one_eq_zero' := by
    ext n
    simp only [LinearMap.coe_mk, AddHom.coe_mk, qEulerFun_coeff, coeff_zero]
    by_cases hn : n = 0
    · subst hn; simp
    · rw [coeff_one, if_neg hn, mul_zero]
  leibniz' x y := by
    ext a
    simp only [LinearMap.coe_mk, AddHom.coe_mk, qEulerFun_coeff, coeff_add', Pi.add_apply,
      smul_eq_mul]
    rw [coeff_mul,
      coeff_mul_right' (x := x) (y := qEulerFun R y) y.isPWO_support (support_qEulerFun_subset R y),
      coeff_mul_right' (x := y) (y := qEulerFun R x) x.isPWO_support (support_qEulerFun_subset R x),
      Finset.mul_sum]
    have hswap : ∑ ij ∈ Finset.antidiagonal y.isPWO_support x.isPWO_support a,
        y.coeff ij.1 * (qEulerFun R x).coeff ij.2
        = ∑ ij ∈ Finset.antidiagonal x.isPWO_support y.isPWO_support a,
            (ij.1 : R) * x.coeff ij.1 * y.coeff ij.2 := by
      refine Finset.sum_nbij' Prod.swap Prod.swap ?_ ?_ ?_ ?_ ?_
      · intro ij hij
        exact Finset.swap_mem_antidiagonal.mpr hij
      · intro ij hij
        exact Finset.swap_mem_antidiagonal.mpr hij
      · intro ij _; rfl
      · intro ij _; rfl
      · intro ij _
        simp only [Prod.fst_swap, Prod.snd_swap, qEulerFun_coeff]
        ring
    rw [hswap, ← Finset.sum_add_distrib]
    refine Finset.sum_congr rfl fun ij hij => ?_
    rw [Finset.mem_antidiagonal] at hij
    rw [qEulerFun_coeff, ← hij.2.2, Int.cast_add]
    ring

@[simp] theorem qEuler_coeff (x : LaurentSeries R) (n : ℤ) :
    (qEuler R x).coeff n = (n : R) * x.coeff n := rfl

theorem qEuler_single (n : ℤ) (r : R) :
    qEuler R (single n r) = single n ((n : R) * r) := by
  ext m
  by_cases h : m = n
  · subst h; simp
  · simp [coeff_single_of_ne h]

end Euler

section Shortcuts

variable {L : Type*} [Field L] (F : IntermediateField L (LaurentSeries L))

set_option synthInstance.maxHeartbeats 400000 in
instance instAlgebraIntermediateFieldLaurent : Algebra L F := inferInstance

set_option synthInstance.maxHeartbeats 400000 in
instance instModuleKaehlerIntermediateFieldLaurent : Module L Ω[F⁄L] := inferInstance

set_option synthInstance.maxHeartbeats 400000 in
instance instIsScalarTowerKaehlerIntermediateFieldLaurent : IsScalarTower L F Ω[F⁄L] :=
  inferInstance

instance instIsScalarTowerIntermediateFieldLaurent : IsScalarTower L F (LaurentSeries L) :=
  ⟨fun c f x => by
    show ((c • f : F) : LaurentSeries L) * x = c • ((f : LaurentSeries L) * x)
    rw [IntermediateField.coe_smul, Algebra.smul_def, algebraMap_laurentSeries_eq_single,
      ← C_apply, mul_assoc, C_mul_eq_smul]⟩

end Shortcuts

section QExpansion

variable {L : Type*} [Field L] (F : IntermediateField L (LaurentSeries L))

def qEulerOn : Derivation L F (LaurentSeries L) :=
  (qEuler L).compAlgebraMap F

@[simp] theorem qEulerOn_apply (x : F) : qEulerOn F x = qEuler L (x : LaurentSeries L) := rfl

def diffQExp : Ω[F⁄L] →ₗ[F] LaurentSeries L :=
  (qEulerOn F).liftKaehlerDifferential

@[simp] theorem diffQExp_D (x : F) : diffQExp F (D L F x) = qEuler L (x : LaurentSeries L) :=
  (qEulerOn F).liftKaehlerDifferential_comp_D x

theorem diffQExp_smul_D (f x : F) :
    diffQExp F (f • D L F x) = (f : LaurentSeries L) * qEuler L (x : LaurentSeries L) := by
  rw [map_smul, diffQExp_D]
  rfl

end QExpansion

section Hecke

variable (L : Type*) [Field L] [Algebra ℚ L] (N ℓ : ℕ) [NeZero N] [NeZero ℓ]

def heckeDiffAlong :
    Ω[laurentBaseChange L (modularFunctionFieldFull N)⁄L] →ₗ[L]
      Ω[laurentBaseChange L (modularFunctionFieldFull N)⁄L] :=
  Differential.correspondence (heckeBetaBar L N ℓ) (heckeAlphaBar L N ℓ)

theorem heckeDiffAlong_apply (ω : Ω[laurentBaseChange L (modularFunctionFieldFull N)⁄L]) :
    heckeDiffAlong L N ℓ ω =
      Differential.traceAlong (heckeBetaBar L N ℓ) (Differential.pullbackAlong (heckeAlphaBar L N ℓ) ω) :=
  rfl

end Hecke

section Bar

variable (N : ℕ)

variable [NeZero N]

def heckeDiffBar (ℓ : Nat.Primes) :
    Module.End (AlgebraicClosure ℚ) Ω[modularFunctionFieldBar N⁄AlgebraicClosure ℚ] :=
  haveI : NeZero (ℓ : ℕ) := ⟨ℓ.2.ne_zero⟩
  heckeDiffAlong (AlgebraicClosure ℚ) N ℓ

theorem heckeDiffBar_eq (ℓ : Nat.Primes) :
    heckeDiffBar N ℓ = (haveI : NeZero (ℓ : ℕ) := ⟨ℓ.2.ne_zero⟩;
      Differential.correspondence (heckeBetaBar (AlgebraicClosure ℚ) N ℓ)
        (heckeAlphaBar (AlgebraicClosure ℚ) N ℓ)) :=
  rfl

abbrev diffQExpBar : Ω[modularFunctionFieldBar N⁄AlgebraicClosure ℚ] →ₗ[modularFunctionFieldBar N]
    LaurentSeries (AlgebraicClosure ℚ) :=
  diffQExp (modularFunctionFieldBar N)

abbrev regularDifferentialsBar : Submodule (AlgebraicClosure ℚ)
    Ω[modularFunctionFieldBar N⁄AlgebraicClosure ℚ] :=
  regularDifferentials (AlgebraicClosure ℚ) (modularFunctionFieldBar N)

end Bar

end ModularCurve

end

Statements phrased using this module (63)