Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_JZeroNeronIdentityComponentGood.lean

definition module

Good-reduction data for the Néron identity component of

Fix a prime p. The first structure, ModularCurve.JZeroNeronIdentityComponent.GoodPrimeData p g L pts ℓ, is parametrised by a scheme G with a morphism g\colon G\to\operatorname{Spec}\mathbf Z, a relative group law L for g (a functorial group structure on the sets SchemeHomOver t g of morphisms over a base morphism t, natural in t), a bijection pts between JZero p — the degree-zero divisor class group of the level-p modular function field over \overline{\mathbf Q} — and the \overline{\mathbf Q}-points of g, and a prime \ell. Writing R_\ell= GaloisRep.ratLocalizedAt ℓ for the subring of rationals whose denominator is coprime to \ell, and f for the second projection of G\times_{\operatorname{Spec}\mathbf Z}\operatorname{Spec}R_\ell, the structure carries: a relative group law L' for f; a bijection pts' from JZero p onto the \overline{\mathbf Q}-points of f; compatibility of L' and pts' with L and pts under the first projection; an AbelianSchemePropertyBundle for f (smoothness, properness, connected fibres over every point of \operatorname{Spec}R_\ell, and existence of a relative group law); commutativity of L'; additivity of pts'; equivariance of pts' for \operatorname{Gal}(\overline{\mathbf Q}/\mathbf Q), expressed by composition with the induced morphism of spectra; a field pointsDict asserting that for every valuation subring A' of \overline{\mathbf Q} with \ell a nonunit there are an R_\ell-structure \sigma_{A'} on \operatorname{Spec}A', a bijection of JZero p with the points of f over \operatorname{Spec}\overline{\mathbf Q}\to\operatorname{Spec}A'\to\operatorname{Spec}R_\ell agreeing with pts', and an additive bijection of the residue-field class group JZeroC (ResidueField A') p with the points over the residue point, such that, whenever ReductionInputsModL A' p holds (a degree-preserving place-reduction map exists and principal divisors are generated by integral ones), ReductionOfPointsAgreesModL holds: each class extends to an A'-point restricting to pts' generically and to the image of reductionModL A' p on the special fibre; and a field hecke asserting that, for the HeckeAlg-module structure heckeModuleBar p on JZero p, every Hecke element is realised by an endomorphism of f over R_\ell which is additive for L' on T-points and induces the action on \overline{\mathbf Q}-points.

The second structure, ModularCurve.JZeroNeronIdentityComponentGood p, extends ModularCurve.JZeroNeronIdentityComponent p by one field: for every prime \ell not dividing p, such good-prime data for the tuple (g,L,\text{pts}) of the underlying component. Since GoodPrimeData takes g, L and pts as explicit arguments, it can be stated for a raw tuple before a full identity component is assembled.

Relation to Mathlib

Mathlib supplies the ambient scheme theory used here (pullbacks, Smooth, IsProper, spectra of commutative rings), but has no notion of relative group law or abelian scheme; RelativeGroupLaw, AbelianSchemePropertyBundle, the divisor class groups JZero/JZeroC, the Hecke algebra action heckeModuleBar and the reduction map reductionModL are the project's own.

Where it is used

These data package the statement that the base change of the Néron identity component of J_0(p) to \mathbf Z_{(\ell)} is an abelian scheme with explicit dictionaries of generic, integral and special-fibre points, for every prime \ell\neq p. They are the input used by the modules that analyse p-primary torsion in J_0(p) and the Eisenstein ideal, where reduction at good primes and the Hecke action must be compared on one and the same model.

References

  1. S. Bosch, W. Lütkebohmert and M. Raynaud, Néron Models, Ergebnisse der Mathematik und ihrer Grenzgebiete 21, Springer, 1990
  2. J. Igusa, Kroneckerian model of fields of elliptic modular functions, American Journal of Mathematics 81 (1959), 561–577
  3. B. Mazur, Modular curves and the Eisenstein ideal, Publications Mathématiques de l'IHÉS 47 (1977), 33–186

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_JZeroNeronIdentityComponent
import Definitions.Def_ModularCurve_ReductionModL
import Definitions.Def_JacJ1Iface
import Definitions.Def_AlgebraicGeometry_RelativeGroupLaw
import Definitions.Def_AlgebraicGeometry_NeronModelEndomorphismExtension
import Definitions.Def_ModularCurve_ReductionOfPointsAgreesModL
import Definitions.Def_ModularCurve_ArithmeticGalois
import Definitions.Def_ModularCurve_HeckeModule
import Definitions.Def_FLTPrelim_Ramification
import Definitions.Def_GaloisRep_Flat

set_option autoImplicit false

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.Scheme NeronModelInfra GoodReductionJacobian
  AlgebraicCurve IsLocalRing

noncomputable section

namespace ModularCurve

structure JZeroNeronIdentityComponent.GoodPrimeData (p : ℕ) [Fact p.Prime]
    {G : Scheme.{0}} (g : G ⟶ Spec (CommRingCat.of ℤ)) (L : RelativeGroupLaw ℤ g)
    (pts : JZero p ≃ SchemeHomOver (Spec.map (CommRingCat.ofHom (algebraMap ℤ (AlgebraicClosure ℚ)))) g)
    (ℓ : ℕ) [Fact ℓ.Prime] where

  L' : RelativeGroupLaw ↥(GaloisRep.ratLocalizedAt ℓ) (pullback.snd g (Spec.map (CommRingCat.ofHom (algebraMap ℤ ↥(GaloisRep.ratLocalizedAt ℓ)))))

  pts' : JZero p ≃ SchemeHomOver (Spec.map (CommRingCat.ofHom
    (algebraMap ↥(GaloisRep.ratLocalizedAt ℓ) (AlgebraicClosure ℚ)))) (pullback.snd g (Spec.map (CommRingCat.ofHom (algebraMap ℤ ↥(GaloisRep.ratLocalizedAt ℓ)))))

  law_compat : ∀ {T : Scheme.{0}} (t : T ⟶ Spec (CommRingCat.of ↥(GaloisRep.ratLocalizedAt ℓ)))
    (x y : SchemeHomOver t (pullback.snd g (Spec.map (CommRingCat.ofHom (algebraMap ℤ ↥(GaloisRep.ratLocalizedAt ℓ))))))
    (X Y : SchemeHomOver (t ≫ Spec.map (CommRingCat.ofHom (algebraMap ℤ ↥(GaloisRep.ratLocalizedAt ℓ)))) g),
    X.1 = x.1 ≫ pullback.fst _ _ → Y.1 = y.1 ≫ pullback.fst _ _ →
    (L'.mul t x y).1 ≫ pullback.fst _ _ = (L.mul _ X Y).1

  pts_compat : ∀ x : JZero p, (pts' x).1 ≫ pullback.fst _ _ = (pts x).1

  bundle : AbelianSchemePropertyBundle ↥(GaloisRep.ratLocalizedAt ℓ) (pullback.snd g (Spec.map (CommRingCat.ofHom (algebraMap ℤ ↥(GaloisRep.ratLocalizedAt ℓ)))))

  comm : ∀ {T : Scheme.{0}} (t : T ⟶ Spec (CommRingCat.of ↥(GaloisRep.ratLocalizedAt ℓ)))
    (x y : SchemeHomOver t (pullback.snd g (Spec.map (CommRingCat.ofHom (algebraMap ℤ ↥(GaloisRep.ratLocalizedAt ℓ)))))), L'.mul t x y = L'.mul t y x

  pts_add : ∀ x y : JZero p, pts' (x + y) = L'.mul _ (pts' x) (pts' y)

  pts_galois : ∀ (σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) (x : JZero p),
    (pts' (σ • x)).1 =
      Spec.map (CommRingCat.ofHom (σ : AlgebraicClosure ℚ →+* AlgebraicClosure ℚ)) ≫ (pts' x).1

  pointsDict : ∀ (A' : ValuationSubring (AlgebraicClosure ℚ)), A'.LiesOverPrime ℓ →
    ∃ (σA : Spec (CommRingCat.of ↥A') ⟶ Spec (CommRingCat.of ↥(GaloisRep.ratLocalizedAt ℓ)))
      (ptsA : JZero p ≃ SchemeHomOver (Spec.map (CommRingCat.ofHom A'.subtype) ≫ σA) (pullback.snd g (Spec.map (CommRingCat.ofHom (algebraMap ℤ ↥(GaloisRep.ratLocalizedAt ℓ))))))
      (ptsSp : JZeroC (ResidueField ↥A') p ≃
        SchemeHomOver (Spec.map (CommRingCat.ofHom (residue ↥A')) ≫ σA) (pullback.snd g (Spec.map (CommRingCat.ofHom (algebraMap ℤ ↥(GaloisRep.ratLocalizedAt ℓ)))))),
      (∀ x : JZero p, (ptsA x).1 = (pts' x).1) ∧
      (∀ u v : JZeroC (ResidueField ↥A') p, ptsSp (u + v) = L'.mul _ (ptsSp u) (ptsSp v)) ∧
      (ReductionInputsModL A' p → ReductionOfPointsAgreesModL p A' (pullback.snd g (Spec.map (CommRingCat.ofHom (algebraMap ℤ ↥(GaloisRep.ratLocalizedAt ℓ))))) σA ptsA ptsSp)

  hecke : letI := heckeModuleBar p
    ∀ t : HeckeAlg, ∃ φ : SchemeHomOver (pullback.snd g (Spec.map (CommRingCat.ofHom (algebraMap ℤ ↥(GaloisRep.ratLocalizedAt ℓ))))) (pullback.snd g (Spec.map (CommRingCat.ofHom (algebraMap ℤ ↥(GaloisRep.ratLocalizedAt ℓ))))),
      (∀ {T : Scheme.{0}} (s : T ⟶ Spec (CommRingCat.of ↥(GaloisRep.ratLocalizedAt ℓ))) (x y : SchemeHomOver s (pullback.snd g (Spec.map (CommRingCat.ofHom (algebraMap ℤ ↥(GaloisRep.ratLocalizedAt ℓ)))))),
        NeronModelInfra.schemeHomOverComp (L'.mul s x y) φ =
          L'.mul s (NeronModelInfra.schemeHomOverComp x φ)
            (NeronModelInfra.schemeHomOverComp y φ)) ∧
      ∀ x : JZero p, (pts' (t • x)).1 = (pts' x).1 ≫ φ.1

structure JZeroNeronIdentityComponentGood (p : ℕ) [Fact p.Prime] extends JZeroNeronIdentityComponent p where

  goodPrime : ∀ (ℓ : ℕ) [Fact ℓ.Prime], ¬ ℓ ∣ p →
    JZeroNeronIdentityComponent.GoodPrimeData p g L pts ℓ

end ModularCurve

end

Statements phrased using this module (5)