Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_AtkinLehnerPartial.lean

definition module

Partial Atkin–Lehner automorphisms of the full modular function field

Fix natural numbers N and \ell with \ell \neq 0. The ambient field is modularFunctionFieldFull (N * ℓ), the intermediate field of \mathbb{Q} \subseteq \mathrm{LaurentSeries}\,\mathbb{Q} generated by the set of all series qExpand\ \mathbb{Q}\ e\ jq for nonzero e \mid N\ell; here jq is the formal Laurent series q^{-1}E_4^3\eta^{-24} over \mathbb{Q} (the q-expansion of the j-invariant) and qExpand ℚ e is the ring homomorphism substituting q \mapsto q^e, i.e. re-indexing coefficients by k \mapsto ek. Thus the field is the one classically written \mathbb{Q}(j(q^e) : e \mid N\ell).

The predicate IsAtkinLehnerAutFull N ℓ σ, for a \mathbb{Q}-algebra automorphism \sigma of that field, asserts: for every nonzero d dividing N, \sigma sends the element j(q^{d}) to j(q^{d\ell}) and sends j(q^{d\ell}) to j(q^{d}), each written as the subtype element given by the relevant membership witness. So it is the clause set expressing that \sigma interchanges the two q-expansions attached to each divisor d of N; nothing further is required of \sigma (in particular it is not required to be prime to N, nor is \ell required to be prime, nor is \sigma^2 = \mathrm{id} imposed), and no existence or uniqueness statement is made.

The definition atkinLehnerInvolutionFull N ℓ is a total, guarded name for such an automorphism: it is a choice of \sigma satisfying IsAtkinLehnerAutFull N ℓ when one exists, and the identity automorphism otherwise. Two lemmas record exactly this: under the existence hypothesis the named map satisfies the predicate, and under its negation the named map is AlgEquiv.refl.

Relation to Mathlib

Mathlib has no modular function fields or Atkin–Lehner operators; both the predicate and the guarded automorphism are the project's own, built on Mathlib's IntermediateField, AlgEquiv and Hahn/Laurent series.

Where it is used

The partial Atkin–Lehner automorphism at \ell is the symmetry used to relate the two degeneracy embeddings of the level-N function field into the level-N\ell one, and hence a Hecke correspondence at \ell with its transpose, in the level-structure bookkeeping underlying level lowering.

References

  1. A. O. L. Atkin and J. Lehner, Hecke operators on \Gamma_0(m), Mathematische Annalen 185 (1970), 134–160
  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_AtkinLehnerPartial.lean

Imports

Imported by

Declarations

Source

import Definitions.Def_ModularCurve_X0

set_option autoImplicit false

namespace ModularCurve

section Partial

variable (N ℓ : ℕ) [NeZero ℓ]

def IsAtkinLehnerAutFull
    (σ : modularFunctionFieldFull (N * ℓ) ≃ₐ[ℚ] modularFunctionFieldFull (N * ℓ)) : Prop :=
  ∀ (d : ℕ) (_ : NeZero d) (hd : d ∣ N),
    σ ⟨qExpand ℚ d jq, jqd_mem_full (N * ℓ) (Dvd.dvd.mul_right hd ℓ)⟩
        = ⟨qExpand ℚ (d * ℓ) jq, jqd_mem_full (N * ℓ) (Nat.mul_dvd_mul_right hd ℓ)⟩
      ∧ σ ⟨qExpand ℚ (d * ℓ) jq, jqd_mem_full (N * ℓ) (Nat.mul_dvd_mul_right hd ℓ)⟩
        = ⟨qExpand ℚ d jq, jqd_mem_full (N * ℓ) (Dvd.dvd.mul_right hd ℓ)⟩

open Classical in

noncomputable def atkinLehnerInvolutionFull :
    modularFunctionFieldFull (N * ℓ) ≃ₐ[ℚ] modularFunctionFieldFull (N * ℓ) :=
  if h : ∃ σ : modularFunctionFieldFull (N * ℓ) ≃ₐ[ℚ] modularFunctionFieldFull (N * ℓ),
      IsAtkinLehnerAutFull N ℓ σ
  then h.choose else AlgEquiv.refl

theorem isAtkinLehnerAutFull_atkinLehnerInvolutionFull
    (h : ∃ σ : modularFunctionFieldFull (N * ℓ) ≃ₐ[ℚ] modularFunctionFieldFull (N * ℓ),
      IsAtkinLehnerAutFull N ℓ σ) :
    IsAtkinLehnerAutFull N ℓ (atkinLehnerInvolutionFull N ℓ) := by
  rw [atkinLehnerInvolutionFull, dif_pos h]
  exact h.choose_spec

theorem atkinLehnerInvolutionFull_eq_refl
    (h : ¬ ∃ σ : modularFunctionFieldFull (N * ℓ) ≃ₐ[ℚ] modularFunctionFieldFull (N * ℓ),
      IsAtkinLehnerAutFull N ℓ σ) :
    atkinLehnerInvolutionFull N ℓ = AlgEquiv.refl := by
  rw [atkinLehnerInvolutionFull, dif_neg h]

end Partial

end ModularCurve

Statements phrased using this module (64)