Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_FibreModel.lean

definition module

Abstract fibre models of in characteristic

Throughout, N is a nonzero natural number, \overline{\mathbb{Q}} is the algebraic closure of \mathbb{Q}, and the ambient characteristic-zero field is laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N), the subfield of \overline{\mathbb{Q}}((q)) generated over \overline{\mathbb{Q}} by the coefficientwise images of modularFunctionFieldFull N, i.e. of the \mathbb{Q}-subfield of \mathbb{Q}((q)) generated by the series j(q^{d}) for all nonzero d \mid N. Inside it, jBar is the image of the q-expansion j(q) and jNBar the image of j(q^{N}). For a valuation subring A \subseteq \overline{\mathbb{Q}}, constantsHom is the inclusion A \hookrightarrow \overline{\mathbb{Q}} followed by the structure map into that field, and affineBaseFin, affineBaseInf are the subrings generated by the constants A together with jBar, respectively with jBar^{-1} — the two affine coordinate rings A[j] and A[1/j] of the j-line.

FibreModel N A ℓ k red, for a prime \ell, a field k of characteristic \ell and a ring homomorphism \mathrm{red} : A \to k, is a structure bundling: two subrings B_{\mathrm{fin}}, B_{\infty} of the characteristic-zero function field; the requirements that each contains all constants \mathrm{const}(a), that B_{\mathrm{fin}} contains jBar and jNBar and B_{\infty} contains jBar^{-1}; integrality of every element of B_{\mathrm{fin}} over A[j] and of every element of B_{\infty} over A[1/j] (a monic polynomial vanishing at it); reduction homomorphisms \pi_{\mathrm{fin}}, \pi_{\infty} into modularFunctionFieldC k N, the subfield of k((q)) generated over k by jqModC k and jqNModC k N; compatibility of each \pi with \mathrm{red} on constants and with the generators (j \mapsto jqModC k, j_N \mapsto jqNModC k N, 1/j \mapsto jqModC k^{-1}); the demand that each kernel be the ideal generated by the image of the maximal ideal of A; integral closedness of each image in the target; and the demand that every element of the target be a quotient \pi(b)/\pi(c) with \pi(c) \neq 0.

Thus the structure carries its defining properties as fields and asserts nothing about existence; consumers take a term of it as a hypothesis.

Relation to Mathlib

Mathlib has no notion of a modular curve or of its reduction; both the ambient function fields and this structure are the project's own, formulated with Mathlib's ValuationSubring, Subring.closure, RingHom.ker, IsLocalRing.maximalIdeal and Laurent series.

Where it is used

These definitions provide the interface on which the statements about specialisation of X_0(N) at a place of residue characteristic \ell are phrased in the tree: a fibre model is bound as a hypothesis, so that any construction of models from the integral closure of A[j] in the function field can be substituted. The resulting arithmetic of X_0(N) in characteristic \ell feeds the level-lowering part of the route to Fermat's Last Theorem.

References

  1. J. Igusa, Kroneckerian model of fields of elliptic modular functions, American Journal of Mathematics 81 (1959), 561–577
  2. P. Deligne and M. Rapoport, Les schémas de modules de courbes elliptiques, in: Modular Functions of One Variable II, Lecture Notes in Mathematics 349, Springer, 1973, 143–316

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

Imports

Imported by

Declarations

Source

import Definitions.Def_ModularCurve_JqCoeff
import Definitions.Def_ModularCurve_LaurentCoeff
import Definitions.Def_ModularCurve_PhiGen
import Definitions.Def_AlgebraicCurve_DivisorClassGroup
import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure ↗

set_option autoImplicit false

noncomputable section

namespace ModularCurve
namespace CharPModel

open AlgebraicCurve

variable (N : ℕ) [NeZero N]

def jBar : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N) :=
  ⟨coeffEmb (AlgebraicClosure ℚ) jq,
    coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionField_le_full N (jq_mem N))⟩

def jNBar : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N) :=
  ⟨coeffEmb (AlgebraicClosure ℚ) (qExpand ℚ N jq),
    coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) (jqd_mem_full N (dvd_refl N))⟩

variable (A : ValuationSubring (AlgebraicClosure ℚ))

def constantsHom : A →+* laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N) :=
  (algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N))).comp A.subtype

def affineBaseFin : Subring (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) :=
  Subring.closure (Set.range (constantsHom N A) ∪ {jBar N})

def affineBaseInf : Subring (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) :=
  Subring.closure (Set.range (constantsHom N A) ∪ {(jBar N)⁻¹})

structure FibreModel (ℓ : ℕ) [Fact ℓ.Prime] (k : Type*) [Field k] [CharP k ℓ]
    (red : A →+* k) : Type _ where

  BFin : Subring (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))

  BInf : Subring (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))

  constFin_mem : ∀ a : A, constantsHom N A a ∈ BFin

  constInf_mem : ∀ a : A, constantsHom N A a ∈ BInf

  jBar_mem : jBar N ∈ BFin

  jNBar_mem : (jNBar N : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ BFin

  jInvBar_mem : (jBar N)⁻¹ ∈ BInf

  integralFin : ∀ b : BFin, ∃ p : Polynomial (affineBaseFin N A),
    p.Monic ∧ Polynomial.eval₂ (affineBaseFin N A).subtype (b : laurentBaseChange (AlgebraicClosure
        ℚ) (modularFunctionFieldFull N)) p = 0

  integralInf : ∀ b : BInf, ∃ p : Polynomial (affineBaseInf N A),
    p.Monic ∧ Polynomial.eval₂ (affineBaseInf N A).subtype (b : laurentBaseChange (AlgebraicClosure
        ℚ) (modularFunctionFieldFull N)) p = 0

  piFin : BFin →+* modularFunctionFieldC k N

  piInf : BInf →+* modularFunctionFieldC k N

  piFin_const : ∀ a : A,
    piFin ⟨constantsHom N A a, constFin_mem a⟩ = algebraMap k (modularFunctionFieldC k N) (red a)

  piInf_const : ∀ a : A,
    piInf ⟨constantsHom N A a, constInf_mem a⟩ = algebraMap k (modularFunctionFieldC k N) (red a)

  piFin_j : piFin ⟨jBar N, jBar_mem⟩ = ⟨jqModC k, jqModC_mem k N⟩

  piFin_jN : piFin ⟨jNBar N, jNBar_mem⟩ = ⟨jqNModC k N, jqNModC_mem k N⟩

  piInf_jInv : piInf ⟨(jBar N)⁻¹, jInvBar_mem⟩ =
    (⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N)⁻¹

  ker_piFin : RingHom.ker piFin =
    Ideal.span ((fun a : A => (⟨constantsHom N A a, constFin_mem a⟩ : BFin)) ''
      (IsLocalRing.maximalIdeal A : Set A))

  ker_piInf : RingHom.ker piInf =
    Ideal.span ((fun a : A => (⟨constantsHom N A a, constInf_mem a⟩ : BInf)) ''
      (IsLocalRing.maximalIdeal A : Set A))

  intClosed_piFin : ∀ x : modularFunctionFieldC k N,
    (∃ p : Polynomial piFin.range, p.Monic ∧ Polynomial.eval₂ piFin.range.subtype x p = 0) →
    x ∈ piFin.range

  intClosed_piInf : ∀ x : modularFunctionFieldC k N,
    (∃ p : Polynomial piInf.range, p.Monic ∧ Polynomial.eval₂ piInf.range.subtype x p = 0) →
    x ∈ piInf.range

  frac_piFin : ∀ x : modularFunctionFieldC k N,
    ∃ b c : BFin, piFin c ≠ 0 ∧ x * piFin c = piFin b

  frac_piInf : ∀ x : modularFunctionFieldC k N,
    ∃ b c : BInf, piInf c ≠ 0 ∧ x * piInf c = piInf b

end CharPModel
end ModularCurve

Statements phrased using this module (64)