Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_XH.lean

definition module

Function fields and Jacobians of the modular curves

Fix a natural number M and a subgroup H \leq (\mathbb{Z}/M)^\times. The underlying congruence subgroup is CohCarrier.GammaH M H, the set of A \in \mathrm{SL}_2(\mathbb{Z}) with A_{10} \equiv 0 \pmod M whose lower-right entry A_{11}, viewed as a unit of \mathbb{Z}/M (its inverse being A_{00}), lies in H. The group-theoretic lemmas record that the translation T = \begin{pmatrix}1&1\\0&1\end{pmatrix} belongs to it, that \Gamma_1(M) \leq \Gamma_H(M) with equality when H is trivial, and that H \mapsto \Gamma_H(M) is monotone.

For a field K, xHFunctionFieldC K M H is the intermediate field of K((q)) over K generated by the ratios \bar p_f/\bar p_g, where f,g are modular forms of one common weight on the image of \Gamma_H(M) in \mathrm{GL}_2(\mathbb{R}) admitting integral q-expansions p_f,p_g \in \mathbb{Z}[[q]] at \infty (i.e. p maps to qExpansion 1 f over \mathbb{C}), reduced coefficientwise into K, with \bar p_g \neq 0; xHFunctionField M H is the case K = \mathbb{Q}. Alongside it, xHTopFunctionFieldC K M H t is the same construction for \Gamma_H(M) \cap \Gamma_0(t). The inclusions proved are: F_H \leq F_{H \cap \Gamma_0(t)} with equality for t = 1; F_H \leq F_{\Gamma_1(M)}; F_{\Gamma_0(M)} \leq F_H; antitonicity in H; and the two extreme cases H = \top giving the \Gamma_0(M) field and H = \bot giving the X_1(M) field.

On the Jacobian side, xHFunctionFieldBar M H is the compositum of \overline{\mathbb{Q}} with the rational field inside \overline{\mathbb{Q}}((q)), obtained by adjoining to \overline{\mathbb{Q}} the coefficientwise image of xHFunctionField M H, and JH M H is the group Pic0 of the resulting extension, carrying an action of \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) through the coefficients and an action of its own additive endomorphisms. JH.torsionGaloisRep n is the resulting representation of \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) on the n-torsion Pic0.torsion by \mathbb{Z}/n-linear endomorphisms, obtained from arithmeticGalois followed by SemilinearAut.torsionRep, with two lemmas identifying its values with the semilinear action. For a prime p, JH.tateGaloisRep and JH.tateEnd are the \mathbb{Z}_p-linear representations of the Galois group and of AddMonoid.End (JH M H) on TateModule p (JH M H), both given by TateModule.rep, acting levelwise on the defining sequences of torsion points. Finally JHC M H K is Pic0 K (xHFunctionFieldC K M H), the class group of the field over an arbitrary base field K.

Relation to Mathlib

Mathlib supplies \Gamma_0(M), \Gamma_1(M), the modular forms ModularForm for a subgroup of \mathrm{GL}_2(\mathbb{R}) and the q-expansion qExpansion; the intermediate groups \Gamma_H(M), the presentation of the function field of a modular curve by integral q-expansion ratios, and the associated divisor class groups and Tate modules are the project's own.

Where it is used

These function fields serve as the carriers of the modular curves X_H(M) in the formalisation, and the groups JH M H with their mod-n and p-adic representations provide the Galois modules on which the Hecke correspondences and diamond operators act, as needed for the construction of the Galois representations attached to modular forms in the modularity-lifting and level-lowering steps.

References

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

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_X1
import Definitions.Def_CohCarrier_Level
import Definitions.Def_EllipticCurve_TateModule

set_option autoImplicit false

noncomputable section

open IntermediateField HahnSeries AlgebraicCurve CongruenceSubgroup

open scoped MatrixGroups

namespace ModularCurve

section Groups

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

theorem translation_mem_GammaH : ModularGroup.T ∈ CohCarrier.GammaH M H := by
  rw [CohCarrier.mem_GammaH_iff]
  have hT0 : ModularGroup.T ∈ Gamma0 M := by
    rw [Gamma0_mem]
    simp [ModularGroup.T]
  refine ⟨hT0, ?_⟩
  have : CohCarrier.gamma0Units M ⟨ModularGroup.T, hT0⟩ = 1 := by
    ext
    simp [CohCarrier.gamma0Units, Gamma0Map, ModularGroup.T]
  rw [this]
  exact one_mem H

theorem Gamma1_le_GammaH : Gamma1 M ≤ CohCarrier.GammaH M H := by
  intro A hA
  rw [Gamma1_mem] at hA
  obtain ⟨_, h11, h10⟩ := hA
  rw [CohCarrier.mem_GammaH_iff]
  have hA0 : A ∈ Gamma0 M := Gamma0_mem.mpr h10
  refine ⟨hA0, ?_⟩
  have : CohCarrier.gamma0Units M ⟨A, hA0⟩ = 1 := by
    ext
    simp only [CohCarrier.gamma0Units, MonoidHom.coe_mk, OneHom.coe_mk, Units.val_one, Gamma0Map]
    exact h11
  rw [this]
  exact one_mem H

theorem GammaH_bot : CohCarrier.GammaH M ⊥ = Gamma1 M := by
  refine le_antisymm ?_ (Gamma1_le_GammaH M ⊥)
  intro A hA
  obtain ⟨hA0, hAH⟩ := CohCarrier.mem_GammaH_iff.mp hA
  rw [Subgroup.mem_bot] at hAH
  have h11 : ((A 1 1 : ℤ) : ZMod M) = 1 := by
    have := congrArg (fun u : (ZMod M)ˣ => (u : ZMod M)) hAH
    simpa [CohCarrier.gamma0Units, Gamma0Map] using this
  have h10 : ((A 1 0 : ℤ) : ZMod M) = 0 := Gamma0_mem.mp hA0
  rw [Gamma1_mem]
  refine ⟨?_, h11, h10⟩
  have hda := CohCarrier.Gamma0_d_mul_a M ⟨A, hA0⟩
  simp only at hda
  rw [h11, one_mul] at hda
  exact hda

variable {M} in

theorem GammaH_mono {H H' : Subgroup (ZMod M)ˣ} (h : H ≤ H') :
    CohCarrier.GammaH M H ≤ CohCarrier.GammaH M H' := by
  intro A hA
  obtain ⟨hA0, hAH⟩ := CohCarrier.mem_GammaH_iff.mp hA
  exact CohCarrier.mem_GammaH_iff.mpr ⟨hA0, h hAH⟩

end Groups

section FunctionField

variable (K : Type*) [Field K] (M : ℕ) (H : Subgroup (ZMod M)ˣ)

def xHFunctionFieldC : IntermediateField K (LaurentSeries K) :=
  qExpFunctionFieldC K (CohCarrier.GammaH M H)

abbrev xHFunctionField : IntermediateField ℚ (LaurentSeries ℚ) :=
  xHFunctionFieldC ℚ M H

theorem xHFunctionFieldC_rat : xHFunctionFieldC ℚ M H = xHFunctionField M H := rfl

def xHTopFunctionFieldC (t : ℕ) : IntermediateField K (LaurentSeries K) :=
  qExpFunctionFieldC K (CohCarrier.GammaH M H ⊓ Gamma0 t)

theorem xHFunctionFieldC_le_top (t : ℕ) : xHFunctionFieldC K M H ≤ xHTopFunctionFieldC K M H t :=
  qExpFunctionFieldC_mono K inf_le_left

theorem xHTopFunctionFieldC_one : xHTopFunctionFieldC K M H 1 = xHFunctionFieldC K M H := by
  have : CohCarrier.GammaH M H ⊓ Gamma0 1 = CohCarrier.GammaH M H := by
    refine le_antisymm inf_le_left (le_inf le_rfl ?_)
    intro A _
    rw [Gamma0_mem]
    exact Subsingleton.elim _ _
  rw [xHTopFunctionFieldC, this, xHFunctionFieldC]

theorem xHFunctionFieldC_le_x1 : xHFunctionFieldC K M H ≤ x1FunctionFieldC K M :=
  qExpFunctionFieldC_mono K (Gamma1_le_GammaH M H)

theorem x0_le_xHFunctionFieldC : qExpFunctionFieldC K (Gamma0 M) ≤ xHFunctionFieldC K M H :=
  qExpFunctionFieldC_mono K (CohCarrier.GammaH_le_Gamma0 H)

variable {H} in

theorem xHFunctionFieldC_antitone {H' : Subgroup (ZMod M)ˣ} (h : H ≤ H') :
    xHFunctionFieldC K M H' ≤ xHFunctionFieldC K M H :=
  qExpFunctionFieldC_mono K (GammaH_mono h)

theorem xHFunctionFieldC_top : xHFunctionFieldC K M ⊤ = qExpFunctionFieldC K (Gamma0 M) := by
  rw [xHFunctionFieldC, CohCarrier.GammaH_top]

theorem xHFunctionFieldC_bot : xHFunctionFieldC K M ⊥ = x1FunctionFieldC K M := by
  rw [xHFunctionFieldC, GammaH_bot]
  rfl

end FunctionField

section Jacobian

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

abbrev xHFunctionFieldBar :
    IntermediateField (AlgebraicClosure ℚ) (LaurentSeries (AlgebraicClosure ℚ)) :=
  laurentBaseChange (AlgebraicClosure ℚ) (xHFunctionField M H)

abbrev JH : Type _ :=
  Pic0 (AlgebraicClosure ℚ) (xHFunctionFieldBar M H)

example : DistribMulAction (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) (JH M H) :=
  inferInstance

example : DistribMulAction (AddMonoid.End (JH M H)) (JH M H) := inferInstance

def JH.torsionGaloisRep (n : ℕ) :
    (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) →*
      Module.End (ZMod n) (Pic0.torsion (AlgebraicClosure ℚ) (xHFunctionFieldBar M H) n) :=
  (SemilinearAut.torsionRep _ _ n).comp (arithmeticGalois (xHFunctionField M H))

@[simp]
theorem JH.torsionGaloisRep_apply {n : ℕ} (σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ)
    (x : Pic0.torsion (AlgebraicClosure ℚ) (xHFunctionFieldBar M H) n) :
    JH.torsionGaloisRep M H n σ x = arithmeticGalois (xHFunctionField M H) σ • x :=
  rfl

theorem JH.coe_torsionGaloisRep_apply {n : ℕ} (σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ)
    (x : Pic0.torsion (AlgebraicClosure ℚ) (xHFunctionFieldBar M H) n) :
    ((JH.torsionGaloisRep M H n σ x : Pic0.torsion (AlgebraicClosure ℚ) (xHFunctionFieldBar M H) n) :
        JH M H) = σ • (x : JH M H) :=
  rfl

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

abbrev JH.tateGaloisRep :
    (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) →* Module.End ℤ_[p] (TateModule p (JH M H)) :=
  TateModule.rep p (JH M H) (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ)

abbrev JH.tateEnd : AddMonoid.End (JH M H) →* Module.End ℤ_[p] (TateModule p (JH M H)) :=
  TateModule.rep p (JH M H) (AddMonoid.End (JH M H))

theorem JH.tateGaloisRep_apply_coe (σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ)
    (x : TateModule p (JH M H)) (n : ℕ) :
    ((JH.tateGaloisRep M H p σ x : TateModule p (JH M H)) : ℕ → JH M H) n = σ • (x : ℕ → JH M H) n :=
  rfl

theorem JH.tateEnd_apply_coe (f : AddMonoid.End (JH M H)) (x : TateModule p (JH M H)) (n : ℕ) :
    ((JH.tateEnd M H p f x : TateModule p (JH M H)) : ℕ → JH M H) n = f ((x : ℕ → JH M H) n) :=
  rfl

abbrev JHC (K : Type*) [Field K] : Type _ :=
  Pic0 K (xHFunctionFieldC K M H)

example (K : Type*) [Field K] : AddCommGroup (JHC M H K) := inferInstance

end Jacobian

end ModularCurve

end

Statements phrased using this module (375)

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