Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_JOnePGeom.lean

definition module

Abstract points-level Néron special fibre of

For a natural number p, the module introduces a single structure, ModularCurve.JOneP.NeronSpecialFibreGeom p, living in Type 1 because it quantifies over carrier types. An inhabitant of it is exactly the following data: a type J0s with an additive commutative group structure; an additive subgroup torus of J0s; two further types JI and JE, each with an additive commutative group structure; an additive group homomorphism proj : J0s →+ JI × JE; a proof that proj is surjective; and a proof that the kernel of proj is precisely the subgroup torus. The group structures on the three carriers are registered as instances, so the carriers may be used as abelian groups wherever an inhabitant of the structure is fixed. Mathematically, therefore, an element of this structure is nothing more and nothing less than a short exact sequence of abelian groups 0 \longrightarrow T \longrightarrow J \longrightarrow J_I \times J_E \longrightarrow 0, with T given as a subgroup of J and the surjection and the identification of the kernel carried as fields rather than proved. The names record the intended reading: J is the group of geometric points of the identity component of the special fibre at p of the Néron model of the Jacobian of the relevant modular curve of level divisible by p, T is its toric part, and J_I, J_E are the Jacobians of the two Igusa components of the special fibre, proj being restriction (pull-back of line bundles) to those two components. The parameter p records the prime at which the fibre is taken and indexes the structure; no modular curve, Néron model, Jacobian or scheme is constructed, and all of the geometry is abstracted into the above group-theoretic data, so downstream statements are conditional on being given such a package.

Relation to Mathlib

Mathlib has no notion of Néron models, special fibres of Jacobians, or Igusa curves; this structure is the project's own abstraction, and it is assembled purely from Mathlib's AddCommGroup, AddSubgroup and AddMonoidHom (kernel and surjectivity).

Where it is used

This package is the geometric input for the level-lowering step at p: statements about the component group and the toric part of the special fibre of J_1(p;M), and the comparison of that fibre with the Igusa curves, are formulated relative to a given inhabitant of it, with the Hecke, diamond and inertia operators supplied by a companion operator-level structure defined over such an inhabitant.

References

  1. 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
  2. S. Bosch, W. Lütkebohmert and M. Raynaud, Néron Models, Ergebnisse der Mathematik und ihrer Grenzgebiete 21, Springer, 1990
  3. K. A. Ribet, On modular representations of \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) arising from modular forms, Inventiones Mathematicae 100 (1990), 431–476

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

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib

set_option autoImplicit false

namespace ModularCurve

namespace JOneP

structure NeronSpecialFibreGeom (p : ℕ) : Type 1 where

  J0s : Type
  [instJ0s : AddCommGroup J0s]

  torus : AddSubgroup J0s

  JI : Type
  [instJI : AddCommGroup JI]
  JE : Type
  [instJE : AddCommGroup JE]

  proj : J0s →+ JI × JE
  proj_surjective : Function.Surjective proj
  ker_proj : proj.ker = torus

attribute [instance] NeronSpecialFibreGeom.instJ0s NeronSpecialFibreGeom.instJI NeronSpecialFibreGeom.instJE

end JOneP

end ModularCurve

Statements phrased using this module (162)

… and 12 more statements (search for the module name to find them).