Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_TatePoint.lean

definition module

Near curves over Hahn series, Tate-point Vélu slots, moduli dictionary

Two families of objects are fixed. Over the field H of Hahn series with rational exponents and coefficients in \bar{\mathbb Q} (written Qbar), jNear j₀ is the element j_0 + s (constant term j_0 plus the monomial of exponent 1 with coefficient 1) and nearCurve j₀ is Mathlib's ofJ at that value, an elliptic curve over H; nearCurve_j records that its j-invariant is j_0+s and nearCurve_j_transcendental that this is transcendental over \bar{\mathbb Q}, since an element of H algebraic over an algebraically closed coefficient field would be a constant. For a Weierstrass curve E over H, CycSubH E N is the type of additive subgroups of the affine point group E(H) of the form \mathbb Z g with g of additive order exactly N, and RootsAt data jv is the type of roots y \in H of the one-variable polynomial obtained from the bivariate \Phi of data by substituting jv for the inner variable. ModuliDictionary p data asserts: for every elliptic E/H with j(E) transcendental over \bar{\mathbb Q} there is a bijection e from RootsAt data E.j to CycSubH E p such that each root r admits a finite set S of pairs which is an odd Vélu set for E (points on the affine equation, \mathrm{gy}\neq 0, injective x-coordinates), whose members lie in the subgroup e(r), and whose Vélu quotient is elliptic with j-invariant r.

At the Tate point, over a field K that is a \mathbb Q-algebra, with p prime and \zeta \in K^\times: basePoint K p is the formal Tate curve over K((q)) with q replaced by q^p, and for a family veluSlotSet of p+1 finite sets of pairs indexed by Fin (p+1), slotQuotient is the corresponding Vélu quotient of basePoint. Under the hypothesis that each slot quotient is elliptic, W4Conclusions data is a Prop-valued structure whose fields assert: each slot set is an odd Vélu set; for b : \mathrm{Fin}\,p the \zeta^b-twist of the Tate curve has j-invariant PhiGen.conj p ζ b.succ; the q \mapsto q^{p^2} specialisation has j-invariant PhiGen.conj p ζ 0; the b-th successor slot quotient equals that twisted Tate curve; the image of \Phi under the composite of evalAtJ, q\mapsto q^p and the coefficient embedding into K((q)) factors as \prod_i (X - j(\mathrm{slotQuotient}\,i)); and the p+1 slot j-invariants are pairwise distinct. W3Proper asserts that each slot set has exactly (p-1)/2 elements and consists of positive multiples k\cdot g of a single point g of additive order p on basePoint K p.

Relation to Mathlib

HahnSeries, AlgebraicClosure, Transcendental, WeierstrassCurve.ofJ and the affine point group law are Mathlib's; the Vélu notions used here (veluQuotient, veluGy, IsOddVeluSet) and the modular-polynomial data type are the project's own.

Where it is used

These declarations fix the common vocabulary in which the level-p moduli correspondence is both produced and consumed: the theorems supplying the p+1 cyclic subgroups of order p on the formal Tate curve, and the theorems deducing the dictionary between roots of the modular polynomial at a j-value and cyclic p-subgroups, used in the modular-curve input to the argument.

References

  1. J. Vélu, Isogénies entre courbes elliptiques, C. R. Acad. Sci. Paris Sér. A 273 (1971), 238–241
  2. J. H. Silverman, Advanced Topics in the Arithmetic of Elliptic Curves, Graduate Texts in Mathematics 151, Springer, 1994, Chapter V
  3. S. Lang, Elliptic Functions, 2nd edition, Graduate Texts in Mathematics 112, Springer, 1987, Chapter 5

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

Imports

Imported by

Declarations

Source

import Definitions.Def_ModularCurve_TateFormal
import Definitions.Def_ModularCurve_PhiGen
import Definitions.Def_WeierstrassCurve_VeluQuotientMap

set_option autoImplicit false

noncomputable section

open ModularCurve WeierstrassCurve Polynomial

namespace ModularCurve.TatePoint

abbrev Qbar : Type := AlgebraicClosure ℚ

abbrev H : Type := HahnSeries ℚ Qbar

def jNear (j₀ : Qbar) : H := HahnSeries.C j₀ + HahnSeries.single (1 : ℚ) (1 : Qbar)

open scoped Classical in

def nearCurve (j₀ : Qbar) : WeierstrassCurve H := WeierstrassCurve.ofJ (jNear j₀)

open scoped Classical in
instance instIsElliptic_nearCurve (j₀ : Qbar) : (nearCurve j₀).IsElliptic := by
  unfold nearCurve; infer_instance

open scoped Classical in

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

def RootsAt {p : ℕ} [NeZero p] (data : ModularPolynomialData p) (jv : H) : Type :=
  {y : H // (data.Φ.map (Polynomial.eval₂RingHom (Int.castRingHom H) jv)).IsRoot y}

open scoped Classical in

theorem nearCurve_j (j₀ : Qbar) : (nearCurve j₀).j = jNear j₀ :=
  WeierstrassCurve.ofJ_j (jNear j₀)

theorem nearCurve_j_transcendental (j₀ : Qbar) : Transcendental Qbar (nearCurve j₀).j := by
  rw [nearCurve_j]
  intro halg
  have hdeg := IsAlgClosed.degree_eq_one_of_irreducible Qbar (minpoly.irreducible halg.isIntegral)
  obtain ⟨c, hc⟩ := minpoly.mem_range_of_degree_eq_one Qbar _ hdeg
  have hC : algebraMap Qbar H c = HahnSeries.C c := by
    rw [HahnSeries.algebraMap_apply', PowerSeries.algebraMap_eq, HahnSeries.ofPowerSeries_C]
  rw [hC] at hc
  have h1 := congrArg (fun x : H => x.coeff (1 : ℚ)) hc
  simp only [jNear, HahnSeries.C_apply, HahnSeries.coeff_add, HahnSeries.coeff_single_same,
    HahnSeries.coeff_single_of_ne (one_ne_zero : (1 : ℚ) ≠ 0), zero_add] at h1
  exact zero_ne_one h1

section TatePoint

variable (K : Type) [Field K] [Algebra ℚ K]
variable (p : ℕ) [Fact (Nat.Prime p)] [NeZero p] (ζ : Kˣ)

def basePoint : WeierstrassCurve (LaurentSeries K) := (tateLaurent K).map (qExpand K p)

variable (veluSlotSet : Fin (p + 1) → Finset (LaurentSeries K × LaurentSeries K))

def slotQuotient (i : Fin (p + 1)) : WeierstrassCurve (LaurentSeries K) :=
  (basePoint K p).veluQuotient (veluSlotSet i)

variable (instQ : ∀ i, (slotQuotient K p veluSlotSet i).IsElliptic)

structure W4Conclusions (data : ModularPolynomialData p) : Prop where

  oddVeluSet : ∀ i, (basePoint K p).IsOddVeluSet (veluSlotSet i)

  slotCurve_succ : ∀ b : Fin p,
    ((tateLaurent K).map (qTwist (ζ ^ (b : ℕ)))).j = PhiGen.conj p ζ b.succ

  slotCurve_zero : ((tateLaurent K).map (qExpand K (p * p))).j = PhiGen.conj p ζ 0

  nonToric : ∀ b : Fin p,
    slotQuotient K p veluSlotSet b.succ = (tateLaurent K).map (qTwist (ζ ^ (b : ℕ)))

  dictionary : data.Φ.map (((coeffEmb K).comp (qExpand ℚ p)).comp evalAtJ) =
    ∏ i : Fin (p + 1),
      (X - C (@WeierstrassCurve.j _ _ (slotQuotient K p veluSlotSet i) (instQ i)))

  distinct : Function.Injective fun i : Fin (p + 1) =>
    @WeierstrassCurve.j _ _ (slotQuotient K p veluSlotSet i) (instQ i)

open scoped Classical in

def W3Proper : Prop :=
  ∀ i, (veluSlotSet i).card = (p - 1) / 2 ∧
    ∃ g : (basePoint K p).toAffine.Point, addOrderOf g = p ∧
      ∀ P ∈ veluSlotSet i, ∃ (k : ℕ) (h : (basePoint K p).toAffine.Nonsingular P.1 P.2),
        0 < k ∧ (k • g : (basePoint K p).toAffine.Point) = WeierstrassCurve.Affine.Point.some P.1 P.2 h

end TatePoint

open scoped Classical in

def ModuliDictionary (p : ℕ) [NeZero p] (data : ModularPolynomialData p) : Prop :=
  ∀ (E : WeierstrassCurve H) [E.IsElliptic], Transcendental Qbar E.j →
    Nonempty {e : RootsAt data E.j ≃ CycSubH E p //
      ∀ r : RootsAt data E.j, ∃ S : Finset (H × H),
        E.IsOddVeluSet S ∧
        (∀ P ∈ S, ∃ h : E.toAffine.Nonsingular P.1 P.2,
          WeierstrassCurve.Affine.Point.some P.1 P.2 h ∈ (e r).1) ∧
        ∃ hQ : (E.veluQuotient S).IsElliptic,
          @WeierstrassCurve.j H _ (E.veluQuotient S) hQ = r.1}

end ModularCurve.TatePoint

end

Statements phrased using this module (7)