Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_CohCarrier_HeckeDiamondRing.lean

definition module

Hecke–diamond ring on degree-one cohomology of

Fix a natural number M, subgroups H, H' \le (\mathbb{Z}/M)^\times, a set S \subseteq \mathbb{N} and a commutative ring A. The carrier is H1 M H A, the A-module \operatorname{Hom}(\Gamma_H(M), A) of additive characters of \Gamma_H(M), written as additive homomorphisms out of Additive ↥(GammaH M H), where \Gamma_H(M) consists of those \gamma \in \mathrm{SL}_2(\mathbb{Z}) lying in \Gamma_0(M) whose lower-right entry, viewed as a unit of \mathbb{Z}/M, belongs to H. The operators adjoined are those already defined on this module: heckeTL M H A ℓ sends \varphi to the transfer (corestriction) from \Gamma_H(M) \cap \Gamma^0(\ell) to \Gamma_H(M) of \varphi composed with the map \begin{pmatrix} a & b \\ c & d\end{pmatrix} \mapsto \begin{pmatrix} a & b/\ell \\ c\ell & d\end{pmatrix}, and diamondL M H A u, for u \in (\mathbb{Z}/M)^\times, is precomposition with conjugation by a chosen \sigma \in \Gamma_0(M) whose lower-right entry reduces to u.

GoodPrime M S is the subtype of \ell with \ell prime, \ell \notin S and \ell \nmid M; heckeTFamily is the resulting family \ell \mapsto T_\ell of A-linear endomorphisms, and heckeTFamily_apply identifies its value with the underlying additive operator heckeT. Under the standing assumption M \neq 0, heckeDiamondGens is the union of the image of this family with \{\langle u\rangle : u \in H'\}, and heckeDiamondRing is the \mathbb{Z}-subalgebra \mathbb{T} = \mathbb{Z}[T_\ell, \langle u\rangle] of \operatorname{End}_A(\operatorname{Hom}(\Gamma_H(M),A)) generated by it. Two membership lemmas record that each generator lies in the generating set, and heckeDiamondRing.T and heckeDiamondRing.diamond, with their coercion lemmas, name the corresponding elements of the subalgebra. No commutativity of the generators is asserted, no operator U_q at primes q \mid M is adjoined, and diamond operators are taken only for u \in H'.

Relation to Mathlib

Mathlib supplies Algebra.adjoin, Module.End and the congruence subgroups \Gamma_0(M), \Gamma(M); the group \Gamma_H(M), the cohomology carrier \operatorname{Hom}(\Gamma_H(M),A), the transfer-defined Hecke operators and the Hecke–diamond subalgebra are the project's own, Mathlib having no Hecke algebra acting on this module.

Where it is used

This ring is the integral Hecke algebra \mathbb{T} acting on the degree-one cohomology of \Gamma_H(M), the source of the Galois representations and of the localisation at a system of Hecke eigenvalues used in the deformation-theoretic part of the argument; the accompanying HeckeData structure packages a commuting family of such operators together with a reduction \bar\theta of eigenvalues into a field.

References

  1. F. Diamond and J. Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005, §5.2 and §6.5
  2. G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Princeton University Press, 1971, §3.5
  3. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154, §1.6

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Definitions.Def_CohCarrier_Inst

set_option autoImplicit false

noncomputable section

namespace CohCarrier

variable (M : ℕ) (H : Subgroup (ZMod M)ˣ) (S : Set ℕ) (H' : Subgroup (ZMod M)ˣ)
  (A : Type) [CommRing A]

abbrev GoodPrime : Type := {ℓ : ℕ // ℓ.Prime ∧ ℓ ∉ S ∧ ¬ ℓ ∣ M}

def heckeTFamily : GoodPrime M S → Module.End A (H1 M H A) :=
  fun ℓ => haveI : NeZero ℓ.1 := ⟨ℓ.2.1.ne_zero⟩; heckeTL M H A ℓ.1

theorem heckeTFamily_apply (ℓ : GoodPrime M S) (φ : H1 M H A) :
    heckeTFamily M H S A ℓ φ = (haveI : NeZero ℓ.1 := ⟨ℓ.2.1.ne_zero⟩; heckeT M H ℓ.1 A φ) := rfl

variable [NeZero M]

def heckeDiamondGens : Set (Module.End A (H1 M H A)) :=
  Set.range (heckeTFamily M H S A) ∪ Set.range (fun u : H' => diamondL M H A (u : (ZMod M)ˣ))

theorem heckeTL_mem_heckeDiamondGens (ℓ : ℕ) (hℓ : ℓ.Prime) (hℓS : ℓ ∉ S) (hℓM : ¬ ℓ ∣ M) :
    (haveI : NeZero ℓ := ⟨hℓ.ne_zero⟩; heckeTL M H A ℓ) ∈ heckeDiamondGens M H S H' A :=
  Or.inl ⟨⟨ℓ, hℓ, hℓS, hℓM⟩, rfl⟩

theorem diamondL_mem_heckeDiamondGens (u : (ZMod M)ˣ) (hu : u ∈ H') :
    diamondL M H A u ∈ heckeDiamondGens M H S H' A :=
  Or.inr ⟨⟨u, hu⟩, rfl⟩

def heckeDiamondRing : Subalgebra ℤ (Module.End A (H1 M H A)) :=
  Algebra.adjoin ℤ (heckeDiamondGens M H S H' A)

namespace heckeDiamondRing

def T (ℓ : ℕ) (hℓ : ℓ.Prime) (hℓS : ℓ ∉ S) (hℓM : ¬ ℓ ∣ M) : ↥(heckeDiamondRing M H S H' A) :=
  ⟨(haveI : NeZero ℓ := ⟨hℓ.ne_zero⟩; heckeTL M H A ℓ),
    Algebra.subset_adjoin (heckeTL_mem_heckeDiamondGens M H S H' A ℓ hℓ hℓS hℓM)⟩

@[simp] theorem coe_T (ℓ : ℕ) (hℓ : ℓ.Prime) (hℓS : ℓ ∉ S) (hℓM : ¬ ℓ ∣ M) :
    ((T M H S H' A ℓ hℓ hℓS hℓM : ↥(heckeDiamondRing M H S H' A)) : Module.End A (H1 M H A)) =
      (haveI : NeZero ℓ := ⟨hℓ.ne_zero⟩; heckeTL M H A ℓ) := rfl

def diamond (u : (ZMod M)ˣ) (hu : u ∈ H') : ↥(heckeDiamondRing M H S H' A) :=
  ⟨diamondL M H A u, Algebra.subset_adjoin (diamondL_mem_heckeDiamondGens M H S H' A u hu)⟩

@[simp] theorem coe_diamond (u : (ZMod M)ˣ) (hu : u ∈ H') :
    ((diamond M H S H' A u hu : ↥(heckeDiamondRing M H S H' A)) : Module.End A (H1 M H A)) =
      diamondL M H A u := rfl

end heckeDiamondRing

end CohCarrier

end

Statements phrased using this module (1)