Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_XHOperators.lean

definition module

Diamond operators and Hecke generators on the Jacobian

Throughout, M is a natural number, H \le (\mathbb{Z}/M)^\times, xHFunctionField M H is the field of q-expansions attached to the congruence subgroup \Gamma_H(M) inside \mathbb{Q}((q)), xHFunctionFieldBar M H its base change to \overline{\mathbb{Q}} = AlgebraicClosure ℚ, and J_H = JH M H the degree-zero divisor class group \mathrm{Pic}^0 of that base-changed field.

For d \in (\mathbb{Z}/M)^\times, IsDiamondAutHBar M H d σ is a predicate on a \overline{\mathbb{Q}}-algebra automorphism \sigma of xHFunctionFieldBar M H, pinning it down through q-expansions: for every weight k \in \mathbb{Z}, every pair of modular forms f, g of weight k on \Gamma_H(M) whose q-expansions are given by integral power series p_f, p_g with the Laurent series of p_g nonzero, and every \gamma \in \mathrm{SL}_2(\mathbb{Z}) lying in \Gamma_0(M) with upper-left entry congruent to d mod M, the image under \sigma of the element coming from the ratio of the two Laurent series is the image of some y in the rational field xHFunctionField M H, and y, pushed to \mathbb{C}((q)) coefficientwise, satisfies y \cdot q\text{-exp}(g\mid_k\gamma) = q\text{-exp}(f\mid_k\gamma). diamondAutHBar M H d is the total choice: such a \sigma when one exists, and the identity otherwise; two lemmas record these two cases. diamondHBar M H d is the induced additive endomorphism of J_H, obtained from the semilinear automorphism attached to diamondAutHBar M H d, and is the identity when no such \sigma exists.

genOpH M H S assigns an additive endomorphism of J_H to each generator in CohCarrier.Gen M S: to T ℓ (for \ell prime, \ell \notin S, \ell \nmid M) and to U q (for q prime dividing M) the correspondence operator heckeOperatorHAlong over \overline{\mathbb{Q}} at that prime — which is 0 unless its geometric inputs hold — and to dia d the diamond operator above; three lemmas state these values. tateGenOpH M H S p g is the induced \mathbb{Z}_p-linear endomorphism of the p-adic Tate module of J_H, acting levelwise on the defining sequences. Finally HeckeDiamondInputsHAll M H bundles the hypotheses needed for all these operators to be the intended ones: HeckeInputsHAlong at every prime \ell (itself an existential packaging of definedness and integrality of the two degeneracy maps, principal divisors upstairs, finiteness, the fundamental identity and the norm formula), together with the existence, for every d, of an automorphism satisfying IsDiamondAutHBar; its two projections extract the Hecke inputs at a prime and the fact that diamondAutHBar M H d then satisfies the predicate.

Relation to Mathlib

Mathlib supplies modular forms, the slash action, q-expansions and the groups \Gamma_0(N), \Gamma_1(N); the groups \Gamma_H(M), the q-expansion function fields, \mathrm{Pic}^0 of a function field and Hecke and diamond operators on it are the project's own notions.

Where it is used

The operators defined here make the Jacobian of X_H(M), and its p-adic Tate module, into a module over the Hecke algebra generated by T_\ell, U_q and the diamond operators, indexed in the same way as the transfer operators on H^1(\Gamma_H(M), -) so that the two actions can be compared generator by generator. This is the source of the Galois representations with prescribed Frobenius traces used in level lowering and modularity lifting.

References

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

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

Imports

Imported by

Declarations

Source

import Definitions.Def_ModularCurve_XHHeckeOperator
import Definitions.Def_CohCarrier_Inst

set_option autoImplicit false

noncomputable section

open UpperHalfPlane IntermediateField HahnSeries AlgebraicCurve CongruenceSubgroup

open scoped MatrixGroups ModularForm

namespace ModularCurve

section Diamond

variable (M : ℕ) (H : Subgroup (ZMod M)ˣ)

def IsDiamondAutHBar (d : (ZMod M)ˣ)
    (σ : xHFunctionFieldBar M H ≃ₐ[AlgebraicClosure ℚ] xHFunctionFieldBar M H) : Prop :=
  ∀ (k : ℤ) (f g : ModularForm (CohCarrier.GammaH M H : Subgroup (GL (Fin 2) ℝ)) k)
    (pf pg : PowerSeries ℤ) (hf : IsIntegralQExp f pf) (hg : IsIntegralQExp g pg)
    (hg0 : intSeriesC ℚ pg ≠ 0) (γ : SL(2, ℤ)), γ ∈ Gamma0 M → ((γ 0 0 : ℤ) : ZMod M) = (d : ZMod M) →
      ∃ y : LaurentSeries ℚ, y ∈ xHFunctionField M H ∧
        ((σ ⟨coeffEmb (AlgebraicClosure ℚ) (intSeriesC ℚ pf / intSeriesC ℚ pg),
              coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ)
                (div_mem_qExpFunctionFieldC f g hf hg hg0)⟩ : xHFunctionFieldBar M H) :
            LaurentSeries (AlgebraicClosure ℚ)) = coeffEmb (AlgebraicClosure ℚ) y ∧
        coeffMap (algebraMap ℚ ℂ) y *
            HahnSeries.ofPowerSeries ℤ ℂ (qExpansion 1 (⇑g ∣[k] (γ : GL (Fin 2) ℝ))) =
          HahnSeries.ofPowerSeries ℤ ℂ (qExpansion 1 (⇑f ∣[k] (γ : GL (Fin 2) ℝ)))

def diamondAutHBar (d : (ZMod M)ˣ) :
    xHFunctionFieldBar M H ≃ₐ[AlgebraicClosure ℚ] xHFunctionFieldBar M H :=
  haveI := Classical.dec (∃ σ : xHFunctionFieldBar M H ≃ₐ[AlgebraicClosure ℚ] xHFunctionFieldBar M H,
    IsDiamondAutHBar M H d σ)
  if h : ∃ σ : xHFunctionFieldBar M H ≃ₐ[AlgebraicClosure ℚ] xHFunctionFieldBar M H,
      IsDiamondAutHBar M H d σ
  then h.choose else AlgEquiv.refl

variable {M H}

theorem isDiamondAutHBar_diamondAutHBar {d : (ZMod M)ˣ}
    (h : ∃ σ : xHFunctionFieldBar M H ≃ₐ[AlgebraicClosure ℚ] xHFunctionFieldBar M H,
      IsDiamondAutHBar M H d σ) :
    IsDiamondAutHBar M H d (diamondAutHBar M H d) := by
  rw [diamondAutHBar, dif_pos h]
  exact h.choose_spec

theorem diamondAutHBar_of_not {d : (ZMod M)ˣ}
    (h : ¬ ∃ σ : xHFunctionFieldBar M H ≃ₐ[AlgebraicClosure ℚ] xHFunctionFieldBar M H,
      IsDiamondAutHBar M H d σ) :
    diamondAutHBar M H d = AlgEquiv.refl := by
  rw [diamondAutHBar, dif_neg h]

variable (M H)

def diamondHBar (d : (ZMod M)ˣ) : JH M H →+ JH M H :=
  DistribSMul.toAddMonoidHom (JH M H) (SemilinearAut.ofAlgAut (diamondAutHBar M H d))

theorem diamondHBar_apply (d : (ZMod M)ˣ) (x : JH M H) :
    diamondHBar M H d x = SemilinearAut.ofAlgAut (diamondAutHBar M H d) • x :=
  rfl

theorem diamondHBar_of_not {d : (ZMod M)ˣ}
    (h : ¬ ∃ σ : xHFunctionFieldBar M H ≃ₐ[AlgebraicClosure ℚ] xHFunctionFieldBar M H,
      IsDiamondAutHBar M H d σ) (x : JH M H) :
    diamondHBar M H d x = x := by
  rw [diamondHBar_apply, diamondAutHBar_of_not h]
  have : SemilinearAut.ofAlgAut
      (AlgEquiv.refl : xHFunctionFieldBar M H ≃ₐ[AlgebraicClosure ℚ] xHFunctionFieldBar M H) = 1 :=
    map_one _
  rw [this, one_smul]

end Diamond

section GenOp

variable (M : ℕ) (H : Subgroup (ZMod M)ˣ) (S : Set ℕ)

def genOpH : CohCarrier.Gen M S → (JH M H →+ JH M H)
  | .T ℓ hℓ _ _ => haveI : NeZero ℓ := ⟨hℓ.ne_zero⟩; heckeOperatorHAlong (AlgebraicClosure ℚ) M H ℓ
  | .U q hq _ => haveI : NeZero q := ⟨hq.ne_zero⟩; heckeOperatorHAlong (AlgebraicClosure ℚ) M H q
  | .dia d => diamondHBar M H d

theorem genOpH_T (ℓ : ℕ) (hℓ : ℓ.Prime) (hℓS : ℓ ∉ S) (hℓM : ¬ ℓ ∣ M) :
    genOpH M H S (.T ℓ hℓ hℓS hℓM) =
      (haveI : NeZero ℓ := ⟨hℓ.ne_zero⟩; heckeOperatorHAlong (AlgebraicClosure ℚ) M H ℓ) :=
  rfl

theorem genOpH_U (q : ℕ) (hq : q.Prime) (hqM : q ∣ M) :
    genOpH M H S (.U q hq hqM) =
      (haveI : NeZero q := ⟨hq.ne_zero⟩; heckeOperatorHAlong (AlgebraicClosure ℚ) M H q) :=
  rfl

theorem genOpH_dia (d : (ZMod M)ˣ) : genOpH M H S (.dia d) = diamondHBar M H d := rfl

variable (p : ℕ) [Fact p.Prime]

def tateGenOpH (g : CohCarrier.Gen M S) : Module.End ℤ_[p] (TateModule p (JH M H)) :=
  JH.tateEnd M H p (genOpH M H S g)

theorem tateGenOpH_apply_coe (g : CohCarrier.Gen M S) (x : TateModule p (JH M H)) (n : ℕ) :
    ((tateGenOpH M H S p g x : TateModule p (JH M H)) : ℕ → JH M H) n =
      genOpH M H S g ((x : ℕ → JH M H) n) :=
  rfl

end GenOp

section Inputs

variable (M : ℕ) (H : Subgroup (ZMod M)ˣ)

def HeckeDiamondInputsHAll : Prop :=
  (∀ ℓ : ℕ, ∀ hℓ : ℓ.Prime, haveI : NeZero ℓ := ⟨hℓ.ne_zero⟩;
      HeckeInputsHAlong (AlgebraicClosure ℚ) M H ℓ) ∧
    ∀ d : (ZMod M)ˣ, ∃ σ : xHFunctionFieldBar M H ≃ₐ[AlgebraicClosure ℚ] xHFunctionFieldBar M H,
      IsDiamondAutHBar M H d σ

variable {M H}

theorem HeckeDiamondInputsHAll.heckeInputsHAlong (h : HeckeDiamondInputsHAll M H) (ℓ : ℕ)
    (hℓ : ℓ.Prime) : haveI : NeZero ℓ := ⟨hℓ.ne_zero⟩; HeckeInputsHAlong (AlgebraicClosure ℚ) M H ℓ :=
  h.1 ℓ hℓ

theorem HeckeDiamondInputsHAll.isDiamondAutHBar (h : HeckeDiamondInputsHAll M H) (d : (ZMod M)ˣ) :
    IsDiamondAutHBar M H d (diamondAutHBar M H d) :=
  isDiamondAutHBar_diamondAutHBar (h.2 d)

end Inputs

end ModularCurve

end

Statements phrased using this module (246)

… and 96 more statements (search for the module name to find them).