Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_HeckeAlgebraHom.lean

definition module

Integral Hecke algebra on characters of

Throughout, additive characters of a congruence group are modelled as additive monoid homomorphisms \mathrm{Additive}\,\Gamma \to \mathbb{Z}, i.e. as elements of \mathrm{Hom}(\Gamma,\mathbb{Z}). The module first records that \mathrm{SL}_2(\mathbb{Z}) is finitely generated, by exhibiting \{S,T\} as a generating set, and deduces the same for \Gamma_0(N) with N \neq 0. For an arbitrary group G and a subset S \subseteq G, evalGen S is the \mathbb{Z}-linear map \mathrm{Hom}(\mathrm{Additive}\,G,\mathbb{Z}) \to (S \to \mathbb{Z}) sending \varphi to its family of values \varphi(s), s \in S; evalGen_injective says it is injective whenever S generates G, and addHom_int_moduleFinite concludes that for finitely generated G the module \mathrm{Hom}(\mathrm{Additive}\,G,\mathbb{Z}) is a finite \mathbb{Z}-module, hence (for G = \Gamma_0(N)) Noetherian; moduleEnd_addHom_int_moduleFinite upgrades this to finiteness of \mathrm{End}_{\mathbb{Z}}\bigl(\mathrm{Hom}(\mathrm{Additive}\,G,\mathbb{Z})\bigr), by evaluating an endomorphism on a finite generating set of the module.

The Hecke vocabulary is then set up inside this endomorphism ring. For \ell \neq 0, heckeOperatorEndHom N ℓ is the \mathbb{Z}-linear endomorphism of \mathrm{Hom}(\mathrm{Additive}\,\Gamma_0(N),\mathbb{Z}) underlying HeckeEis.heckeOperatorHom N ℓ ℤ, that is: restrict a character along the finite-index subgroup of \gamma \in \Gamma_0(N) with \ell \mid \gamma_{01}, pull back along the conjugation \gamma \mapsto \alpha_\ell^{-1}\gamma\alpha_\ell by \alpha_\ell = \mathrm{diag}(1,\ell), and then corestrict back to \Gamma_0(N) by the transfer (a sum over the coset space). For N \neq 0 and a set S \subseteq \mathbb{N}, heckeAlgebraHom N S is the \mathbb{Z}-subalgebra of \mathrm{End}_{\mathbb{Z}}\bigl(\mathrm{Hom}(\mathrm{Additive}\,\Gamma_0(N),\mathbb{Z})\bigr) generated by the operators heckeOperatorEndHom N ℓ for all primes \ell \notin S; thus S = \varnothing gives the full algebra and excluding the primes dividing N gives an anemic variant. Finally, the submodule parabolicHoms ℤ (Gamma0 N) ℤ of characters vanishing on every \gamma with (\operatorname{tr}\gamma)^2 = 4 is recorded to be a finite \mathbb{Z}-module.

Relation to Mathlib

Mathlib supplies the group-theoretic input (generators of \mathrm{SL}_2(\mathbb{Z}), Group.FG, Schreier's lemma for finite-index subgroups) and the module-finiteness machinery; the Hecke operators on \mathrm{Hom}(\Gamma_0(N),\mathbb{Z}) and the subalgebra they generate are the project's own notions, with no Mathlib counterpart.

Where it is used

These operators and the algebra they generate provide the integral, group-theoretic model of the Hecke action used alongside the analytic Hecke algebra on cusp forms: finiteness over \mathbb{Z} of the algebra and of the parabolic submodule is what makes eigenvalues integral and allows an eigenvector to be reduced modulo a prime, which is the starting point for attaching mod-\ell representations to eigenforms.

References

  1. G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, 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 8

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Definitions.Def_Gamma0HeckeOperatorHom
import Definitions.Def_ModularCurve_PeriodMap
import Mathlib.RingTheory.Finiteness.Subalgebra ↗
import Mathlib.GroupTheory.Schreier ↗
import Mathlib.LinearAlgebra.Matrix.FixedDetMatrices ↗
import Mathlib.GroupTheory.Finiteness ↗

set_option autoImplicit false

open CongruenceSubgroup
open scoped MatrixGroups

namespace ModularCurve.Period

section FGInfrastructure

instance instGroupFG_SL2Z : Group.FG SL(2, ℤ) :=
  ⟨⟨{ModularGroup.S, ModularGroup.T}, by
    simp only [Finset.coe_insert, Finset.coe_singleton]
    exact SpecialLinearGroup.SL2Z_generators⟩⟩

instance instGroupFG_Gamma0 (N : ℕ) [NeZero N] : Group.FG (Gamma0 N) := inferInstance

variable {G : Type*} [Group G]

noncomputable def evalGen (S : Set G) : (Additive G →+ ℤ) →ₗ[ℤ] (S → ℤ) where
  toFun φ s := φ (Additive.ofMul (s : G))
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

theorem evalGen_injective {S : Set G} (hS : Subgroup.closure S = ⊤) :
    Function.Injective (evalGen S) := by
  intro φ ψ h
  refine AddMonoidHom.ext fun γ => ?_
  have hmem : Additive.toMul γ ∈ Subgroup.closure S := hS ▸ Subgroup.mem_top _
  suffices hkey : φ (Additive.ofMul (Additive.toMul γ)) = ψ (Additive.ofMul (Additive.toMul γ)) by
    simpa using hkey
  set g := Additive.toMul γ
  clear_value g; clear γ
  induction hmem using Subgroup.closure_induction with
  | mem s hs => exact congrFun h ⟨s, hs⟩
  | one => simp
  | mul a b _ _ iha ihb =>
      have hmul : (Additive.ofMul (a * b) : Additive G) = Additive.ofMul a + Additive.ofMul b := rfl
      rw [hmul, map_add, map_add, iha, ihb]
  | inv a _ iha =>
      have hinv : (Additive.ofMul a⁻¹ : Additive G) = -Additive.ofMul a := rfl
      rw [hinv, map_neg, map_neg, iha]

theorem addHom_int_moduleFinite [Group.FG G] : Module.Finite ℤ (Additive G →+ ℤ) := by
  obtain ⟨S, hS, hSfin⟩ := Group.fg_iff.mp ‹Group.FG G›
  haveI : Finite S := hSfin
  exact Module.Finite.of_injective (evalGen S) (evalGen_injective hS)

instance instIsNoetherian_addHom_int (N : ℕ) [NeZero N] :
    IsNoetherian ℤ (Additive (Gamma0 N) →+ ℤ) :=
  have := addHom_int_moduleFinite (G := (Gamma0 N))
  inferInstance

theorem moduleEnd_addHom_int_moduleFinite [Group.FG G] :
    Module.Finite ℤ (Module.End ℤ (Additive G →+ ℤ)) := by
  haveI := addHom_int_moduleFinite (G := G)
  set M := Additive G →+ ℤ
  obtain ⟨s, hs⟩ := Module.Finite.fg_top (R := ℤ) (M := M)
  let ev : Module.End ℤ M →ₗ[ℤ] (s → M) :=
    { toFun := fun f i => f (i : M)
      map_add' := fun _ _ => rfl
      map_smul' := fun _ _ => rfl }
  refine Module.Finite.of_injective ev ?_
  rw [← LinearMap.ker_eq_bot, eq_bot_iff]
  intro f hf
  simp only [Submodule.mem_bot, LinearMap.mem_ker] at hf ⊢
  refine LinearMap.ext fun m => ?_
  have hm : m ∈ (⊤ : Submodule ℤ M) := Submodule.mem_top
  rw [← hs] at hm
  refine Submodule.span_induction ?_ ?_ ?_ ?_ hm
  · intro x hx
    exact congrFun hf ⟨x, hx⟩
  · simp
  · intro x y _ _ ihx ihy
    simp [map_add, ihx, ihy]
  · intro c x _ ihx
    simp [map_smul, ihx]

end FGInfrastructure

section Vocabulary

variable (N ℓ : ℕ) [NeZero ℓ]

noncomputable def heckeOperatorEndHom : Module.End ℤ (Additive (Gamma0 N) →+ ℤ) :=
  AddMonoidHom.toIntLinearMap (HeckeEis.heckeOperatorHom N ℓ ℤ)

variable [NeZero N] (S : Set ℕ)

noncomputable def heckeAlgebraHom :
    Subalgebra ℤ (Module.End ℤ (Additive (Gamma0 N) →+ ℤ)) :=
  Algebra.adjoin ℤ
    {T | ∃ (ℓ : ℕ) (_ : NeZero ℓ), ℓ.Prime ∧ ℓ ∉ S ∧ T = heckeOperatorEndHom N ℓ}

end Vocabulary

section ParabolicFiniteness

variable (N : ℕ) [NeZero N]

instance parabolicHoms_int_moduleFinite :
    Module.Finite ℤ (parabolicHoms ℤ (Gamma0 N) ℤ) :=
  Module.Finite.of_injective (parabolicHoms ℤ (Gamma0 N) ℤ).subtype
    (parabolicHoms ℤ (Gamma0 N) ℤ).injective_subtype

end ParabolicFiniteness

end ModularCurve.Period

Statements phrased using this module (0)

No statement module imports it directly (it is used through other definition modules or by proofs).