Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_X1Diamond.lean

definition module

Diamond automorphisms of the function field and

Working with the q-expansion model of modular curves, this module introduces diamond operators. First, for a field L containing \mathbb{Q} and an intermediate field F_0 of \mathbb{Q}((q))/\mathbb{Q}, the predicate IsBaseChangeAutOf L σ₀ σ says of an L-algebra automorphism \sigma of the compositum laurentBaseChange L F₀ (the L-subfield of L((q)) generated by the coefficientwise image of F_0) that it extends the \mathbb{Q}-automorphism \sigma_0 of F_0: for every y \in F_0, the image under \sigma of the coefficientwise embedding of y is the coefficientwise embedding of \sigma_0(y). The total operation baseChangeAut L σ₀ returns such an extension when one exists and the identity otherwise, as recorded by isBaseChangeAutOf_baseChangeAut and baseChangeAut_of_not.

Next, slashQExpC k f γ is the period-one q-expansion of the weight-k slash f\mid_k\gamma, for f : \mathbb{H} \to \mathbb{C} and \gamma \in \mathrm{SL}_2(\mathbb{Z}), viewed in \mathbb{C}((q)). The predicate IsDiamondAut M d σ, for a \mathbb{Q}-algebra automorphism \sigma of x1FunctionField M, asserts that d is coprime to M and that for all weights k, all modular forms f, g of weight k on \Gamma_1(M) with integral q-expansions p_f, p_g (and p_g nonzero over \mathbb{Q}), and all \gamma \in \Gamma_0(M) with upper-left entry congruent to d modulo M, the image in \mathbb{C}((q)) of \sigma(p_f/p_g) multiplied by the q-expansion of g\mid_k\gamma equals that of f\mid_k\gamma; thus \sigma is pinned down on the generating ratios of modular forms by pull-back along \gamma. Again diamondAut M d is total: it picks such a \sigma if one exists and is the identity otherwise, in particular whenever d and M are not coprime. Base changing to \overline{\mathbb{Q}} gives diamondAutBar M d, and diamondOneBar M d is the induced \mathbb{Z}-linear endomorphism of J_1(M) = \mathrm{Pic}^0 of the base-changed function field, acting through the semilinear automorphism that is trivial on the constants.

Relation to Mathlib

Mathlib's modular forms, the slash action f\mid_k\gamma and qExpansion are used as given; the diamond operators on a function-field model of X_1(M) and their action on the degree-zero Picard group are the project's own notions, Mathlib having no modular curves or their Jacobians.

Where it is used

The diamond operators provide the action of (\mathbb{Z}/M)^\times on J_1(M) and hence on its torsion, which is what allows modular forms with nebentypus character and their associated Galois representations to be isolated inside the Jacobian of X_1(M) in the modularity and level-lowering parts of the argument.

References

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

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

Imports

Imported by

Declarations

Source

import Definitions.Def_ModularCurve_X1

set_option autoImplicit false

noncomputable section

open UpperHalfPlane IntermediateField HahnSeries AlgebraicCurve CongruenceSubgroup

open scoped MatrixGroups ModularForm

namespace ModularCurve

section BaseChangeAut

variable (L : Type*) [Field L] [Algebra ℚ L] {F₀ : IntermediateField ℚ (LaurentSeries ℚ)}

def IsBaseChangeAutOf (σ₀ : F₀ ≃ₐ[ℚ] F₀)
    (σ : laurentBaseChange L F₀ ≃ₐ[L] laurentBaseChange L F₀) : Prop :=
  ∀ y : F₀,
    ((σ ⟨coeffEmb L (y : LaurentSeries ℚ), coeffEmb_mem_laurentBaseChange L y.2⟩ :
        laurentBaseChange L F₀) : LaurentSeries L)
      = coeffEmb L ((σ₀ y : F₀) : LaurentSeries ℚ)

def baseChangeAut (σ₀ : F₀ ≃ₐ[ℚ] F₀) :
    laurentBaseChange L F₀ ≃ₐ[L] laurentBaseChange L F₀ :=
  haveI := Classical.dec
    (∃ σ : laurentBaseChange L F₀ ≃ₐ[L] laurentBaseChange L F₀, IsBaseChangeAutOf L σ₀ σ)
  if h : ∃ σ : laurentBaseChange L F₀ ≃ₐ[L] laurentBaseChange L F₀, IsBaseChangeAutOf L σ₀ σ
  then h.choose else AlgEquiv.refl

variable {L}

theorem isBaseChangeAutOf_baseChangeAut {σ₀ : F₀ ≃ₐ[ℚ] F₀}
    (h : ∃ σ : laurentBaseChange L F₀ ≃ₐ[L] laurentBaseChange L F₀, IsBaseChangeAutOf L σ₀ σ) :
    IsBaseChangeAutOf L σ₀ (baseChangeAut L σ₀) := by
  rw [baseChangeAut, dif_pos h]
  exact h.choose_spec

theorem baseChangeAut_of_not {σ₀ : F₀ ≃ₐ[ℚ] F₀}
    (h : ¬ ∃ σ : laurentBaseChange L F₀ ≃ₐ[L] laurentBaseChange L F₀, IsBaseChangeAutOf L σ₀ σ) :
    baseChangeAut L σ₀ = AlgEquiv.refl := by
  rw [baseChangeAut, dif_neg h]

end BaseChangeAut

section Diamond

variable (M : ℕ)

def slashQExpC (k : ℤ) (f : ℍ → ℂ) (γ : SL(2, ℤ)) : LaurentSeries ℂ :=
  HahnSeries.ofPowerSeries ℤ ℂ (qExpansion 1 (f ∣[k] (γ : GL (Fin 2) ℝ)))

def IsDiamondAut (d : ℕ) (σ : x1FunctionField M ≃ₐ[ℚ] x1FunctionField M) : Prop :=
  Nat.Coprime d M ∧
    ∀ (k : ℤ) (f g : ModularForm (Gamma1 M : 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) →
        coeffMap (algebraMap ℚ ℂ)
            ((σ ⟨intSeriesC ℚ pf / intSeriesC ℚ pg, div_mem_qExpFunctionFieldC f g hf hg hg0⟩ :
                x1FunctionField M) : LaurentSeries ℚ)
          * slashQExpC k g γ = slashQExpC k f γ

theorem IsDiamondAut.coprime {d : ℕ} {σ : x1FunctionField M ≃ₐ[ℚ] x1FunctionField M}
    (h : IsDiamondAut M d σ) : Nat.Coprime d M := h.1

def diamondAut (d : ℕ) : x1FunctionField M ≃ₐ[ℚ] x1FunctionField M :=
  haveI := Classical.dec (∃ σ : x1FunctionField M ≃ₐ[ℚ] x1FunctionField M, IsDiamondAut M d σ)
  if h : ∃ σ : x1FunctionField M ≃ₐ[ℚ] x1FunctionField M, IsDiamondAut M d σ
  then h.choose else AlgEquiv.refl

variable {M}

theorem isDiamondAut_diamondAut {d : ℕ}
    (h : ∃ σ : x1FunctionField M ≃ₐ[ℚ] x1FunctionField M, IsDiamondAut M d σ) :
    IsDiamondAut M d (diamondAut M d) := by
  rw [diamondAut, dif_pos h]
  exact h.choose_spec

theorem diamondAut_of_not {d : ℕ}
    (h : ¬ ∃ σ : x1FunctionField M ≃ₐ[ℚ] x1FunctionField M, IsDiamondAut M d σ) :
    diamondAut M d = AlgEquiv.refl := by
  rw [diamondAut, dif_neg h]

theorem diamondAut_of_not_coprime {d : ℕ} (h : ¬ Nat.Coprime d M) :
    diamondAut M d = AlgEquiv.refl :=
  diamondAut_of_not fun ⟨_, hσ⟩ => h hσ.coprime

end Diamond

section DiamondBar

variable (M : ℕ)

def diamondAutBar (d : ℕ) :
    x1FunctionFieldBar M ≃ₐ[AlgebraicClosure ℚ] x1FunctionFieldBar M :=
  baseChangeAut (AlgebraicClosure ℚ) (diamondAut M d)

def diamondOneBar (d : ℕ) : Module.End ℤ (JOne M) :=
  (DistribSMul.toAddMonoidHom (JOne M) (SemilinearAut.ofAlgAut (diamondAutBar M d))).toIntLinearMap

theorem diamondOneBar_apply (d : ℕ) (x : JOne M) :
    diamondOneBar M d x = SemilinearAut.ofAlgAut (diamondAutBar M d) • x :=
  rfl

end DiamondBar

end ModularCurve

end

Statements phrased using this module (59)