Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_DegeneracyTower.lean

definition module

Degeneracy maps at arbitrary level and Hecke exchange identity

Throughout, L is a field of characteristic zero containing \mathbb{Q}, and for a positive integer N the field L\cdot F_N denotes laurentBaseChange L (modularFunctionFieldFull N), the intermediate field of L((q)) generated over L by the coefficientwise image of modularFunctionFieldFull N, which is itself the subfield of \mathbb{Q}((q)) generated over \mathbb{Q} by the series \mathrm{qExpand}\,d\,(j) for all nonzero divisors d \mid N (substitution q \mapsto q^{d} in the q-expansion of j). Two families of L-algebra maps are defined for an arbitrary target level, constrained only by a divisibility hypothesis, so that composites of Hecke maps become single maps between fixed types: towerInclBar L (h : N ∣ M), the inclusion L\cdot F_N \hookrightarrow L\cdot F_M which is the identity on underlying Laurent series; and towerSubstBar L N ℓ (h : N*ℓ ∣ M), the composite of heckeBetaBar L N ℓ with such an inclusion, acting on underlying series as \mathrm{qExpand}\,\ell, i.e. q \mapsto q^{\ell}. Accompanying lemmas record the values on underlying series, invariance under replacing \ell by an equal natural number, transitivity and reflexivity of the inclusions, the identifications of heckeAlphaBar and heckeBetaBar as instances of the two families at target level N\ell, the four composition rules with heckeAlphaBar and heckeBetaBar (including \mathrm{subst}_{\ell}\circ\beta_{\ell'} = \mathrm{subst}_{\ell\ell'}), and the resulting commuting square heckeSquareBar_commutes.

For M = N\ell\ell', dvd_of_eq_roof supplies the divisibilities N\ell \mid M and N\ell'\ell \mid M. The predicate HeckeExchangeAt L N ℓ ℓ' M hM is a named input: assuming HasPrincipalDivisors at levels N\ell and M and integrality of the four maps \beta_{\ell}, \alpha_{\ell'}, u = towerInclBar into level M and u' = towerSubstBar L (N*ℓ') ℓ, it asserts that for every divisor D on L\cdot F_{N\ell'} one has \beta_{\ell}^{*}\big((\alpha_{\ell'})_{*}D\big) = u_{*}\big(u'^{*}D\big) in the divisor group of L\cdot F_{N\ell}, the pullbacks and pushforwards being those along algebra maps from the correspondence module.

Relation to Mathlib

Modular function fields, their degeneracy maps and the divisor-level exchange identity are the project's own notions; only the underlying machinery (IntermediateField.inclusion, Laurent series, integrality of ring maps) is Mathlib's.

Where it is used

These maps are the two degeneracy embeddings underlying the Hecke correspondences on the Jacobian J_0(N), realised here as the degree-zero divisor class group of the base-changed modular function field; stating them with an arbitrary target level lets composites such as T_{\ell}T_{\ell'} be formed inside one fixed field at the roof level N\ell\ell'. The exchange identity HeckeExchangeAt is the divisor-level input from which commutativity of the Hecke operators, and hence the Hecke module structure on the Jacobian used in the modularity argument, is derived.

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 3
  2. F. Diamond and J. Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005, Chapters 5 and 7

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

Imports

Imported by

Declarations

Source

import Definitions.Def_ModularCurve_HeckeOperator

set_option autoImplicit false

noncomputable section

namespace ModularCurve

open AlgebraicCurve

section PrivateSupply

variable (L : Type*) [Field L] [Algebra ℚ L]

private theorem laurentBaseChange_mono'' {F₀ F₁ : IntermediateField ℚ (LaurentSeries ℚ)}
    (h : F₀ ≤ F₁) : laurentBaseChange L F₀ ≤ laurentBaseChange L F₁ := by
  rw [laurentBaseChange, IntermediateField.adjoin_le_iff]
  rintro _ ⟨y, hy, rfl⟩
  exact coeffEmb_mem_laurentBaseChange L (h hy)

end PrivateSupply

section TowerMaps

variable (L : Type*) [Field L] [Algebra ℚ L] {N M : ℕ} [NeZero N] [NeZero M]

def towerInclBar (h : N ∣ M) :
    laurentBaseChange L (modularFunctionFieldFull N) →ₐ[L]
      laurentBaseChange L (modularFunctionFieldFull M) :=
  IntermediateField.inclusion (laurentBaseChange_mono'' L (full_degeneracy_le h))

@[simp]
theorem coe_towerInclBar (h : N ∣ M) (x : laurentBaseChange L (modularFunctionFieldFull N)) :
    (towerInclBar L h x : LaurentSeries L) = (x : LaurentSeries L) :=
  IntermediateField.coe_inclusion _ x

theorem towerInclBar_eq_inclusion (h : N ∣ M)
    (h' : laurentBaseChange L (modularFunctionFieldFull N) ≤
      laurentBaseChange L (modularFunctionFieldFull M)) :
    towerInclBar L h = IntermediateField.inclusion h' :=
  rfl

theorem towerInclBar_comp_towerInclBar {M' : ℕ} [NeZero M'] (h₁ : N ∣ M') (h₂ : M' ∣ M)
    (h : N ∣ M) : (towerInclBar L h₂).comp (towerInclBar L h₁) = towerInclBar L h := by
  refine AlgHom.ext fun x => Subtype.ext ?_
  rw [AlgHom.comp_apply, coe_towerInclBar, coe_towerInclBar, coe_towerInclBar]

theorem towerInclBar_self (h : N ∣ N) (x : laurentBaseChange L (modularFunctionFieldFull N)) :
    towerInclBar L h x = x :=
  Subtype.ext (coe_towerInclBar L h x)

variable (N) in

def towerSubstBar (ℓ : ℕ) [NeZero ℓ] (h : N * ℓ ∣ M) :
    laurentBaseChange L (modularFunctionFieldFull N) →ₐ[L]
      laurentBaseChange L (modularFunctionFieldFull M) :=
  (towerInclBar L h).comp (heckeBetaBar L N ℓ)

@[simp]
theorem coe_towerSubstBar (ℓ : ℕ) [NeZero ℓ] (h : N * ℓ ∣ M)
    (x : laurentBaseChange L (modularFunctionFieldFull N)) :
    (towerSubstBar L N ℓ h x : LaurentSeries L) = qExpand L ℓ (x : LaurentSeries L) :=
  rfl

theorem towerSubstBar_congr {ℓ ℓ' : ℕ} [NeZero ℓ] [NeZero ℓ'] (hℓ : ℓ = ℓ') (h : N * ℓ ∣ M)
    (h' : N * ℓ' ∣ M) : towerSubstBar L N ℓ h = towerSubstBar L N ℓ' h' := by
  subst hℓ
  rfl

end TowerMaps

section Composites

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

theorem heckeAlphaBar_eq_towerInclBar : heckeAlphaBar L N ℓ = towerInclBar L (dvd_mul_right N ℓ) :=
  rfl

theorem heckeBetaBar_eq_towerSubstBar : heckeBetaBar L N ℓ = towerSubstBar L N ℓ dvd_rfl := by
  refine AlgHom.ext fun x => Subtype.ext ?_
  rw [coe_towerSubstBar, coe_heckeBetaBar]

theorem towerInclBar_comp_heckeAlphaBar (h : N * ℓ ∣ M) (h' : N ∣ M) :
    (towerInclBar L h).comp (heckeAlphaBar L N ℓ) = towerInclBar L h' := by
  refine AlgHom.ext fun x => Subtype.ext ?_
  rw [AlgHom.comp_apply, coe_towerInclBar, coe_heckeAlphaBar, coe_towerInclBar]

theorem towerInclBar_comp_heckeBetaBar (h : N * ℓ ∣ M) :
    (towerInclBar L h).comp (heckeBetaBar L N ℓ) = towerSubstBar L N ℓ h :=
  rfl

theorem towerSubstBar_comp_heckeAlphaBar (h : N * ℓ' * ℓ ∣ M) (h' : N * ℓ ∣ M) :
    (towerSubstBar L (N * ℓ') ℓ h).comp (heckeAlphaBar L N ℓ') = towerSubstBar L N ℓ h' := by
  refine AlgHom.ext fun x => Subtype.ext ?_
  rw [AlgHom.comp_apply, coe_towerSubstBar, coe_heckeAlphaBar, coe_towerSubstBar]

theorem towerSubstBar_comp_heckeBetaBar (h : N * ℓ' * ℓ ∣ M) (h' : N * (ℓ * ℓ') ∣ M) :
    (towerSubstBar L (N * ℓ') ℓ h).comp (heckeBetaBar L N ℓ') = towerSubstBar L N (ℓ * ℓ') h' := by
  refine AlgHom.ext fun x => Subtype.ext ?_
  rw [AlgHom.comp_apply, coe_towerSubstBar, coe_heckeBetaBar, coe_towerSubstBar]
  exact qExpand_qExpand ℓ' ℓ _

theorem heckeSquareBar_commutes (h₁ : N * ℓ ∣ M) (h₂ : N * ℓ' * ℓ ∣ M) :
    (towerInclBar L h₁).comp (heckeBetaBar L N ℓ) =
      (towerSubstBar L (N * ℓ') ℓ h₂).comp (heckeAlphaBar L N ℓ') := by
  rw [towerInclBar_comp_heckeBetaBar, towerSubstBar_comp_heckeAlphaBar]

end Composites

section Exchange

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

omit [NeZero N] [NeZero ℓ] [NeZero ℓ'] [NeZero M] in

theorem dvd_of_eq_roof (hM : M = N * ℓ * ℓ') : N * ℓ ∣ M ∧ N * ℓ' * ℓ ∣ M :=
  ⟨⟨ℓ', hM⟩, ⟨1, by rw [hM]; ring⟩⟩

def HeckeExchangeAt (hM : M = N * ℓ * ℓ') : Prop :=
  ∀ [HasPrincipalDivisors L (laurentBaseChange L (modularFunctionFieldFull (N * ℓ)))]
    [HasPrincipalDivisors L (laurentBaseChange L (modularFunctionFieldFull M))]
    (hβ : (heckeBetaBar L N ℓ).toRingHom.IsIntegral)
    (hα' : (heckeAlphaBar L N ℓ').toRingHom.IsIntegral)
    (hu : (towerInclBar L (dvd_of_eq_roof N ℓ ℓ' M hM).1).toRingHom.IsIntegral)
    (hu' : (towerSubstBar L (N * ℓ') ℓ (dvd_of_eq_roof N ℓ ℓ' M hM).2).toRingHom.IsIntegral)
    (D : Divisor L (laurentBaseChange L (modularFunctionFieldFull (N * ℓ')))),
    Divisor.pullbackAlong (heckeBetaBar L N ℓ) hβ
        (Divisor.pushforwardAlong (heckeAlphaBar L N ℓ') hα' D)
      = Divisor.pushforwardAlong (towerInclBar L (dvd_of_eq_roof N ℓ ℓ' M hM).1) hu
          (Divisor.pullbackAlong (towerSubstBar L (N * ℓ') ℓ (dvd_of_eq_roof N ℓ ℓ' M hM).2) hu' D)

end Exchange

end ModularCurve

end

Statements phrased using this module (25)