Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_ModuliPoint.lean

definition module

Naive moduli set of Γ₀(N)-structures and its base change

Fix a natural number N and a field L. A Gamma0Pair N L is a structure carrying a Weierstrass curve toCurve over L — a tuple of coefficients a_1,a_2,a_3,a_4,a_6, i.e. a chosen Weierstrass model, not an isomorphism class — together with a field asserting that this model is elliptic (registered as an instance), a point gen of the associated affine curve, and a field asserting addOrderOf gen = N; thus for N\ge 1 the point is of exact additive order N, while N=0 records that gen has no finite order. The relation Gamma0Pair.Step P Q asserts the existence of an admissible change of variables \gamma=(u,r,s,t) over L with \gamma\bullet P.\mathtt{toCurve}=Q.\mathtt{toCurve}, and of a natural number k coprime to N, such that Q.\mathtt{gen} equals k\cdot\big(\text{transport of }P.\mathtt{gen}\big), where the transport is the project's map Point.vcInvFun, sending (x,y)\mapsto(u^{-2}(x-r),\,u^{-3}(y-t-s(x-r))) and 0\mapsto 0; the equality of points is stated as a heterogeneous equality across the identification of curves given by \gamma. ModuliPoint N L is the quotient Quot of Gamma0Pair N L by this one-step relation, so identifications are by the equivalence relation generated by Step. Since the j-invariant is invariant under variable change, it descends to ModuliPoint.j : ModuliPoint N L → L.

The second half provides base change along a ring homomorphism \sigma : L \to L' of fields: gamma0PairMap applies \sigma to the coefficients and transports the point by the coordinatewise map ratPointMap, the order being preserved because that map is an injective group homomorphism; gamma0PairStep_map shows Step is preserved, yielding moduliPointMapRingHom : ModuliPoint N L → ModuliPoint N L' (a map of sets, despite the name) with j(\sigma_* x)=\sigma(j(x)). Auxiliary lemmas record that \sigma commutes with the formulas vcXInv, vcYInv for the variable change \gamma mapped by \sigma, that point transport and base change commute up to heterogeneous equality, that ratPointMap commutes with n\bullet and preserves additive orders, and three heterogeneous-equality lemmas for points across an equality of Weierstrass models.

Relation to Mathlib

Mathlib supplies WeierstrassCurve, its VariableChange action, affine points and the j-invariant; the naive moduli set of \Gamma_0(N)-structures, the relation identifying pairs, and its base-change functoriality are the project's own, built on the project's transport of affine points along a variable change and along a homomorphism of fields.

Where it is used

These definitions give a concrete, model-based presentation of the L-points of the open modular curve Y_0(N) as classes of pairs (elliptic curve with a point of order N), with the j-invariant and base change along field homomorphisms available; they are imported by many later statement modules of the tree.

References

  1. J. H. Silverman, The Arithmetic of Elliptic Curves, Graduate Texts in Mathematics 106, Springer, 1986, Ch. III
  2. F. Diamond and J. Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005, Ch. 1 and 8

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_WeierstrassCurve_VariableChangePointEquiv
import Definitions.Def_WeierstrassCurve_RatPointHom

noncomputable section

namespace ModularCurve

open WeierstrassCurve WeierstrassCurve.Affine

section Pairs

variable (N : ℕ) (L : Type*) [Field L] [DecidableEq L]

structure Gamma0Pair where

  toCurve : WeierstrassCurve L

  isElliptic : toCurve.IsElliptic

  gen : toCurve.toAffine.Point

  addOrderOf_gen : addOrderOf gen = N

attribute [instance] Gamma0Pair.isElliptic

variable {N L}

def Gamma0Pair.Step (P Q : Gamma0Pair N L) : Prop :=
  ∃ γ : VariableChange L, ∃ _ : γ • P.toCurve = Q.toCurve, ∃ k : ℕ, k.Coprime N ∧
    HEq Q.gen (k • Point.vcInvFun γ P.toCurve.toAffine P.gen)

variable (N L) in

def ModuliPoint : Type _ := Quot (Gamma0Pair.Step (N := N) (L := L))

noncomputable def ModuliPoint.j : ModuliPoint N L → L :=
  Quot.lift (fun P => P.toCurve.j) fun P Q h => by
    obtain ⟨γ, hγ, -⟩ := h
    show P.toCurve.j = Q.toCurve.j
    simp_rw [← hγ, variableChange_j]

@[simp] lemma ModuliPoint.j_mk (P : Gamma0Pair N L) :
    ModuliPoint.j (Quot.mk _ P : ModuliPoint N L) = P.toCurve.j := rfl

end Pairs

section HEqToolbox

variable {K : Type*} [Field K]

theorem Point.heq_zero {V V' : WeierstrassCurve.Affine K} (hV : V' = V) :
    HEq (0 : V'.Point) (0 : V.Point) := by
  subst hV
  rfl

theorem Point.heq_some {V V' : WeierstrassCurve.Affine K} (hV : V' = V) {x y x' y' : K}
    {h : V.Nonsingular x y} {h' : V'.Nonsingular x' y'} (hx : x' = x) (hy : y' = y) :
    HEq (Point.some x' y' h' : V'.Point) (Point.some x y h : V.Point) := by
  subst hV
  subst hx
  subst hy
  rfl

theorem Point.heq_nsmul [DecidableEq K] {V V' : WeierstrassCurve.Affine K} (hV : V' = V)
    (n : ℕ) {S : V'.Point} {T : V.Point} (h : HEq S T) : HEq (n • S) (n • T) := by
  subst hV
  rw [eq_of_heq h]

end HEqToolbox

section Map

variable {L L' : Type} [Field L] [Field L']
variable [DecidableEq L] [DecidableEq L']

theorem addOrderOf_ratPointMap (σ : L →+* L') (V : WeierstrassCurve L) (P : V.toAffine.Point) :
    addOrderOf (WeierstrassCurve.ratPointMap σ (W₀ := V) P) = addOrderOf P :=
  addOrderOf_injective (WeierstrassCurve.ratPointHom σ (W₀ := V))
    (WeierstrassCurve.ratPointMap_injective σ (W₀ := V)) P

theorem ratPointMap_nsmul (σ : L →+* L') (V : WeierstrassCurve L) (k : ℕ) (P : V.toAffine.Point) :
    WeierstrassCurve.ratPointMap σ (W₀ := V) (k • P) = k • WeierstrassCurve.ratPointMap σ (W₀ := V) P :=
  map_nsmul (WeierstrassCurve.ratPointHom σ (W₀ := V)) k P

omit [DecidableEq L] [DecidableEq L'] in

theorem map_vcXInv (σ : L →+* L') (γ : VariableChange L) (x : L) :
    σ (vcXInv γ x) = vcXInv (γ.map σ) (σ x) := by
  simp [vcXInv, map_mul, map_pow, map_sub]

omit [DecidableEq L] [DecidableEq L'] in

theorem map_vcYInv (σ : L →+* L') (γ : VariableChange L) (x y : L) :
    σ (vcYInv γ x y) = vcYInv (γ.map σ) (σ x) (σ y) := by
  simp [vcYInv, map_mul, map_pow, map_sub]

omit [DecidableEq L] [DecidableEq L'] in

theorem ratPointMap_vcInvFun_heq (σ : L →+* L') (γ : VariableChange L) (V : WeierstrassCurve L)
    (P : V.toAffine.Point) :
    HEq (WeierstrassCurve.ratPointMap σ (W₀ := γ • V) (Point.vcInvFun γ V.toAffine P))
        (Point.vcInvFun (γ.map σ) (V.map σ).toAffine (WeierstrassCurve.ratPointMap σ (W₀ := V) P)) := by
  have hc : (γ • V).map σ = (γ.map σ) • (V.map σ) :=
    (WeierstrassCurve.map_variableChange V γ σ).symm
  cases P with
  | zero => exact Point.heq_zero hc
  | some x y h => exact Point.heq_some hc (map_vcXInv σ γ x) (map_vcYInv σ γ x y)

variable {N : ℕ}

def gamma0PairMap (σ : L →+* L') (P : Gamma0Pair N L) : Gamma0Pair N L' where
  toCurve := P.toCurve.map σ
  isElliptic := inferInstance
  gen := WeierstrassCurve.ratPointMap σ (W₀ := P.toCurve) P.gen
  addOrderOf_gen := (addOrderOf_ratPointMap σ P.toCurve P.gen).trans P.addOrderOf_gen

@[simp] theorem gamma0PairMap_toCurve (σ : L →+* L') (P : Gamma0Pair N L) :
    (gamma0PairMap σ P).toCurve = P.toCurve.map σ := rfl

@[simp] theorem gamma0PairMap_gen (σ : L →+* L') (P : Gamma0Pair N L) :
    (gamma0PairMap σ P).gen = WeierstrassCurve.ratPointMap σ (W₀ := P.toCurve) P.gen := rfl

theorem gamma0PairStep_map (σ : L →+* L') {P Q : Gamma0Pair N L}
    (h : Gamma0Pair.Step P Q) :
    Gamma0Pair.Step (gamma0PairMap σ P) (gamma0PairMap σ Q) := by
  obtain ⟨γ, hγ, k, hk, hgen⟩ := h
  obtain ⟨WP, hEP, gP, hgP⟩ := P
  obtain ⟨WQ, hEQ, gQ, hgQ⟩ := Q
  change γ • WP = WQ at hγ
  subst hγ
  change HEq gQ (k • Point.vcInvFun γ WP.toAffine gP) at hgen
  have hgen' : gQ = k • Point.vcInvFun γ WP.toAffine gP := eq_of_heq hgen
  refine ⟨γ.map σ, ?_, k, hk, ?_⟩
  · show γ.map σ • WP.map σ = (γ • WP).map σ
    exact WeierstrassCurve.map_variableChange WP γ σ
  · show HEq (WeierstrassCurve.ratPointMap σ (W₀ := γ • WP) gQ)
      (k • Point.vcInvFun (γ.map σ) (WP.map σ).toAffine (WeierstrassCurve.ratPointMap σ (W₀ := WP) gP))
    rw [hgen']
    refine HEq.trans (heq_of_eq (ratPointMap_nsmul σ (γ • WP) k
      (Point.vcInvFun γ WP.toAffine gP))) ?_
    exact Point.heq_nsmul (WeierstrassCurve.map_variableChange WP γ σ).symm k
      (ratPointMap_vcInvFun_heq σ γ WP gP)

def moduliPointMapRingHom (σ : L →+* L') : ModuliPoint N L → ModuliPoint N L' :=
  Quot.lift (fun P => (Quot.mk _ (gamma0PairMap σ P) : ModuliPoint N L'))
    fun _ _ h => Quot.sound (gamma0PairStep_map σ h)

@[simp] theorem moduliPointMapRingHom_mk (σ : L →+* L') (P : Gamma0Pair N L) :
    moduliPointMapRingHom σ (Quot.mk _ P : ModuliPoint N L) =
      (Quot.mk _ (gamma0PairMap σ P) : ModuliPoint N L') := rfl

theorem j_moduliPointMapRingHom (σ : L →+* L') (x : ModuliPoint N L) :
    (moduliPointMapRingHom σ x).j = σ x.j := by
  induction x using Quot.ind with
  | _ P => exact (P.toCurve.map_j σ)

end Map

end ModularCurve

end

Statements phrased using this module (16)