Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_PrimCosetReps.lean

definition module

Primitive coset representatives and the coset product polynomial

For a natural number N, primCosetReps N is the finite set of triples (a,b,d) of natural numbers, carved out of \{0,\dots,N\}^3, satisfying ad = N, b < d and \gcd(a,\gcd(b,d)) = 1; these are the usual representatives \begin{pmatrix} a & b \\ 0 & d\end{pmatrix} of the primitive integral matrices of determinant N modulo \mathrm{SL}_2(\mathbb{Z}). The companion lemma mem_primCosetReps states, for N \neq 0, that (a,b,d) lies in primCosetReps N precisely when ad = N, b < d and \gcd(a,\gcd(b,d)) = 1: the ambient bounds a,b,d \le N used to make the set finite are automatic consequences of ad = N and b < d.

Over a field K, for a unit \zeta \in K^\times, a formal Laurent series J over K and a triple t = (a,b,d), cosetConj ζ J t is defined to be 0 when a = 0, and otherwise to be cosetSubst ζ a b J, that is the image of J under the composite of the coefficientwise twist c_k \mapsto (\zeta^{ab})^k c_k with the exponent rescaling k \mapsto a^2 k — formally the substitution J(t) \mapsto J(\zeta^{ab} t^{a^2}). The third entry d of the triple does not enter the formula. The lemma cosetConj_eq records the case a \neq 0 of this definition. Finally, cosetTwoVarPoly ζ N J is the polynomial \prod_{t \in \mathrm{primCosetReps}\ N} \bigl(X - C(\mathrm{cosetConj}\ \zeta\ J\ t)\bigr) in one variable over the field of formal Laurent series over K: a monic polynomial whose degree is the cardinality of primCosetReps N, and whose roots are the coset conjugates of J. When J is the q-expansion of j and \zeta a primitive N-th root of unity, this is the right-hand side of the coset factorisation of the modular polynomial \Phi_N.

Relation to Mathlib

Mathlib has no modular polynomial, nor coset representatives for primitive integral matrices of a given determinant; these are the project's own notions, built on Mathlib's LaurentSeries/HahnSeries and Polynomial API.

Where it is used

These definitions supply the factorised side of the modular equation: the coset conjugates of the q-expansion of j and their product polynomial are the input to the construction of a modular polynomial \Phi_N and hence of the function field of X_0(N), which underlies the modular-curve material used in the Frey–Serre–Ribet–Wiles–Taylor–Wiles argument.

References

  1. S. Lang, Elliptic Functions, 2nd edition, Graduate Texts in Mathematics 112, Springer, 1987, Chapter 5
  2. D. A. Cox, Primes of the Form x^2+ny^2: Fermat, Class Field Theory, and Complex Multiplication, Wiley, 1989, §11

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_PhiGen

set_option autoImplicit false

namespace ModularCurve

def primCosetReps (N : ℕ) : Finset (ℕ × ℕ × ℕ) :=
  Finset.filter
    (fun t => t.1 * t.2.2 = N ∧ t.2.1 < t.2.2 ∧ Nat.gcd t.1 (Nat.gcd t.2.1 t.2.2) = 1)
    (Finset.range (N + 1) ×ˢ Finset.range (N + 1) ×ˢ Finset.range (N + 1))

theorem mem_primCosetReps {N a b d : ℕ} (hN : N ≠ 0) :
    (a, b, d) ∈ primCosetReps N ↔ a * d = N ∧ b < d ∧ Nat.gcd a (Nat.gcd b d) = 1 := by
  simp only [primCosetReps, Finset.mem_filter, Finset.mem_product, Finset.mem_range]
  constructor
  · rintro ⟨_, had, hbd, hgcd⟩
    exact ⟨had, hbd, hgcd⟩
  · rintro ⟨had, hbd, hgcd⟩
    have hd0 : d ≠ 0 := by
      rintro rfl
      exact hN (by simpa using had.symm)
    have ha0 : a ≠ 0 := by
      rintro rfl
      exact hN (by simpa using had.symm)
    have haN : a ≤ N := had ▸ Nat.le_mul_of_pos_right a (Nat.pos_of_ne_zero hd0)
    have hdN : d ≤ N := had ▸ Nat.le_mul_of_pos_left d (Nat.pos_of_ne_zero ha0)
    exact ⟨⟨by omega, by omega, by omega⟩, had, hbd, hgcd⟩

section Conjugates

variable {K : Type*} [Field K]

noncomputable def cosetConj (ζ : Kˣ) (J : LaurentSeries K) (t : ℕ × ℕ × ℕ) : LaurentSeries K :=
  if h : t.1 = 0 then 0 else
    haveI : NeZero t.1 := ⟨h⟩
    cosetSubst ζ t.1 t.2.1 J

theorem cosetConj_eq (ζ : Kˣ) (J : LaurentSeries K) (a b d : ℕ) [NeZero a] :
    cosetConj ζ J (a, b, d) = cosetSubst ζ a b J := by
  unfold cosetConj
  rw [dif_neg (NeZero.ne a)]

noncomputable def cosetTwoVarPoly (ζ : Kˣ) (N : ℕ) (J : LaurentSeries K) : Polynomial (LaurentSeries K) :=
  (primCosetReps N).prod fun t => Polynomial.X - Polynomial.C (cosetConj ζ J t)

end Conjugates

end ModularCurve

Statements phrased using this module (13)