Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_FibreModelCuspChart.lean

definition module

Cusp chart condition on a characteristic- fibre model

Fix N \ge 1, a valuation subring A of \overline{\mathbb{Q}}, a prime \ell, a field k of characteristic \ell and a ring homomorphism \mathrm{red} : A \to k. For a fibre model fm : FibreModel N A ℓ k red the proposition FibreModel.CuspChart fm is a predicate on that model — a structure valued in Prop, carrying two assertions and no data — about the single element \bar t \;=\; \overline{j_N}\cdot(\bar j^{\,-1})^N, formed inside the ambient characteristic-zero field laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N), the \overline{\mathbb{Q}}-subfield of \overline{\mathbb{Q}}-Laurent series generated by the coefficientwise images of the q-expansions j(q^d) for d \mid N. Here jBar N is the image of j(q)=q^{-1}+\dots and jNBar N the image of j(q^N), so \bar t is j(q^N)\,j(q)^{-N}.

The first field tBar_mem asserts that \bar t lies in the subring fm.BInf, the model ring of fm at the pole chart (the one containing the constants from A and \bar j^{-1} and integral over the closure of A[\bar j^{-1}]). The second field piInf_t asserts that the specialisation homomorphism fm.piInf : fm.BInf → modularFunctionFieldC k N carries \bar t, viewed as an element of fm.BInf via the first field, to \widetilde{j_N}\cdot(\widetilde{j}^{\,-1})^N = \mathtt{jqNModC }k\,N \cdot (\mathtt{jqModC }k)^{-N}, where jqModC k is the q-expansion of j with coefficients reduced into k and jqNModC k N its q \mapsto q^N substitution, both inside the k-subfield of k-Laurent series they generate. Thus the predicate pins down both the integrality of j(q^N)/j(q)^N on the pole chart and the value of its reduction.

Relation to Mathlib

Mathlib has no notion of a fibre model of a modular curve or of these q-expansion function fields; the predicate is the project's own, stated in terms of Mathlib's ValuationSubring, LaurentSeries and IntermediateField.

Where it is used

The bare fibre-model interface only makes the pole chart's ring contain A[\bar j^{-1}], whose elements are congruent to constants at every cusp; adjoining the condition on j(q^N)/j(q)^N gives an element of the model ring whose reduction is recorded exactly, and so lets statements about the reduction of X_0(N) modulo \ell follow the cusps through specialisation.

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
  3. S. Lang, Elliptic Functions, 2nd edition, Graduate Texts in Mathematics 112, Springer, 1987

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

Imports

Imported by

  • no other definition module

Declarations

Source

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

set_option autoImplicit false

noncomputable section

namespace ModularCurve
namespace CharPModel

open AlgebraicCurve

variable (N : ℕ) [NeZero N] (A : ValuationSubring (AlgebraicClosure ℚ))
variable (ℓ : ℕ) [Fact ℓ.Prime] (k : Type*) [Field k] [CharP k ℓ] (red : A →+* k)

structure FibreModel.CuspChart (fm : FibreModel N A ℓ k red) : Prop where

  tBar_mem : jNBar N * ((jBar N)⁻¹) ^ N ∈ fm.BInf

  piInf_t :
    fm.piInf ⟨jNBar N * ((jBar N)⁻¹) ^ N, tBar_mem⟩ =
      (⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N) *
        ((⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N))⁻¹ ^ N

end CharPModel
end ModularCurve

Statements phrased using this module (81)