Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_EMD.lean

definition module

Embedding–moduli dictionary for the modular function field

Over a field L with decidable equality, pairStabCard attaches to a \Gamma_0(N)-pair P (a Weierstrass curve P.toCurve over L that is elliptic, together with a point P.gen of exact additive order N) the cardinality, as a natural number, of the set of variable changes \gamma that fix the Weierstrass model, \gamma \bullet P.\mathrm{toCurve} = P.\mathrm{toCurve}, and for which P.gen is heterogeneously equal to k \bullet (the image of P.gen under the point substitution attached to the inverse of \gamma) for some k coprime to N; this is the stabiliser of P for the relation Gamma0Pair.Step generating the moduli-point quotient, not the stabiliser of the curve alone. The remaining definitions set up a dictionary between series expansions and cyclic subgroups. For N \neq 0 and j_0 \in \overline{\mathbb{Q}}, Emb N j₀ is the type of \overline{\mathbb{Q}}-algebra homomorphisms \psi from modularFunctionFieldBar N to the Hahn series field \overline{\mathbb{Q}} with rational exponents, normalised by \psi(\bar{j}) = j_0 + t, where \bar{j} is jBar N. Induces ψ w says that there is a rational g > 0 with g \cdot \mathrm{ord}_w(x) = \mathrm{order}(\psi(x)) for every x in the field, i.e. the leading exponent of the series expansion is proportional to the valuation at the place w; SamePlace ψ ψ' asserts that one and the same place is induced by both. On the geometric side, CycSub E₀ N is the type of additive subgroups of the affine points of E_0 that are of the form \langle g \rangle for some point g of exact order N, and SameOrbit E₀ H H' says that H = \langle g \rangle and H' = \langle g' \rangle for points g, g' with g' heterogeneously equal to the image of g under the point substitution attached to the inverse of some variable change \gamma preserving E_0. Finally, EMD N j₀ is the proposition that there exist a Weierstrass curve E_0 over \overline{\mathbb{Q}}, elliptic, with j(E_0) = j_0, and a bijection \Phi from Emb N j₀ to CycSub E₀ N transporting SamePlace into SameOrbit: \psi and \psi' induce a common place exactly when \Phi(\psi) and \Phi(\psi') lie in one orbit of the automorphisms of the model.

Relation to Mathlib

Mathlib supplies the Weierstrass curves, variable changes and Hahn series (with their order) used here; the pair stabiliser count, the normalised embeddings, the induced-place and same-orbit relations and the dictionary statement EMD are the project's own notions, formulated for the project's places of a function field and its substitution maps on Weierstrass points.

Where it is used

These notions express the moduli interpretation of the points of X_0(N) over \overline{\mathbb{Q}} in the shape needed in the Mazur part of the argument: places of modularFunctionFieldBar N lying over a given j-value correspond to cyclic subgroups of order N on a curve with that invariant, up to automorphisms. This is what allows a pair consisting of an elliptic curve and a point of order p to be converted into a place of the modular function field with prescribed behaviour, the input to the Eisenstein-quotient specialisation argument.

References

  1. B. Mazur, Modular curves and the Eisenstein ideal, Publications Mathématiques de l'IHÉS 47 (1977), 33–186
  2. G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Publications of the Mathematical Society of Japan 11, Princeton University Press, 1971, Chapter 6
  3. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154

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

Imports

Imported by

Declarations

Source

import Definitions.Def_ModularCurve_ModuliPoint
import Definitions.Def_ModularCurve_MazurStepThreeInputs

set_option autoImplicit false

noncomputable section

namespace ModularCurve

open AlgebraicCurve WeierstrassCurve WeierstrassCurve.Affine

section PairStab

variable {N : ℕ} {L : Type*} [Field L] [DecidableEq L]

noncomputable def pairStabCard (P : Gamma0Pair N L) : ℕ :=
  Nat.card {γ : VariableChange L // γ • P.toCurve = P.toCurve ∧
    ∃ k : ℕ, k.Coprime N ∧ HEq P.gen (k • Point.vcInvFun γ P.toCurve.toAffine P.gen)}

end PairStab

def Emb (N : ℕ) [NeZero N] (j₀ : AlgebraicClosure ℚ) : Type :=
  {ψ : ↥(modularFunctionFieldBar N) →ₐ[AlgebraicClosure ℚ] HahnSeries ℚ (AlgebraicClosure ℚ) //
    ψ (jBar N) = HahnSeries.C j₀ + HahnSeries.single (1 : ℚ) (1 : AlgebraicClosure ℚ)}

def Induces {N : ℕ} [NeZero N]
    (ψ : ↥(modularFunctionFieldBar N) →ₐ[AlgebraicClosure ℚ] HahnSeries ℚ (AlgebraicClosure ℚ))
    (w : Place (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar N)) : Prop :=
  ∃ g : ℚ, 0 < g ∧ ∀ x : ↥(modularFunctionFieldBar N), (w.ord x : ℚ) * g = (ψ x).order

def SamePlace {N : ℕ} [NeZero N]
    (ψ ψ' : ↥(modularFunctionFieldBar N) →ₐ[AlgebraicClosure ℚ] HahnSeries ℚ (AlgebraicClosure ℚ)) :
    Prop :=
  ∃ w : Place (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar N), Induces ψ w ∧ Induces ψ' w

def CycSub (E₀ : WeierstrassCurve (AlgebraicClosure ℚ)) (N : ℕ) : Type :=
  {H : AddSubgroup E₀.toAffine.Point //
    ∃ g : E₀.toAffine.Point, addOrderOf g = N ∧ H = AddSubgroup.zmultiples g}

def SameOrbit (E₀ : WeierstrassCurve (AlgebraicClosure ℚ)) (H H' : AddSubgroup E₀.toAffine.Point) :
    Prop :=
  ∃ γ : VariableChange (AlgebraicClosure ℚ), ∃ _ : γ • E₀ = E₀, ∃ g g' : E₀.toAffine.Point,
    H = AddSubgroup.zmultiples g ∧ H' = AddSubgroup.zmultiples g' ∧
      HEq g' (Point.vcInvFun γ E₀.toAffine g)

def EMD (N : ℕ) [NeZero N] (j₀ : AlgebraicClosure ℚ) : Prop :=
  ∃ (E₀ : WeierstrassCurve (AlgebraicClosure ℚ)) (_ : E₀.IsElliptic), E₀.j = j₀ ∧
    ∃ Φ : Emb N j₀ ≃ CycSub E₀ N, ∀ ψ ψ' : Emb N j₀,
      SamePlace ψ.1 ψ'.1 ↔ SameOrbit E₀ (Φ ψ).1 (Φ ψ').1

end ModularCurve

end

Statements phrased using this module (16)