Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_JZeroNeronTorsionSheafV4.lean

definition module

Fppf torsion-sheaf datum for Eisenstein torsion of

Two abelian subgroups of J_0(p) are introduced first. For a prime p and natural numbers q,m, eisensteinTorsionBar p q m is the subgroup of elements of JZero p annihilated by every element of the m-th power of eisensteinMaximalIdeal p q, the ideal of the Hecke algebra HeckeAlg consisting of those operators whose value under the Eisenstein character \mathrm{HeckeAlg}\to\mathbb Z at level p lies in (q); the action used is the Hecke module structure heckeModuleBar p. For a valuation subring A of \overline{\mathbb Q} lying over p, toricEisensteinPart p q A hA m is the intersection of that subgroup with jZeroToricTorsion p A (q ^ m), i.e. with the set of q^m-torsion points of the form e\cdot y with y invariant under the inertia subgroup of A, e being eisensteinNumerator p.

The structure JZeroNeronTorsionSheaf p q A hA, for primes p,q and such an A, packages: a family \mathcal J_m of abelian sheaves on the small fppf site of \operatorname{Spec}\mathbb Z, together with flat finite-type Hopf \mathbb Z-algebras H_m and additive identifications, natural in U, of the sections of \mathcal J_m over an fppf \operatorname{Spec}\mathbb Z-scheme U with the convolution group of \mathbb Z-algebra maps H_m\to\Gamma(U,\mathcal O); bijections of the \overline{\mathbb Q}-points of H_m with eisensteinTorsionBar p q m and of its A-points with toricEisensteinPart p q A hA m, each additive for convolution, Galois-equivariant respectively compatible with A\hookrightarrow\overline{\mathbb Q}; for each prime \ell\neq p a finite flat cocommutative Hopf algebra H^{\mathrm{ff}}_{m,\ell} over GaloisRep.ratLocalizedAt ℓ whose \overline{\mathbb Q}-points are again identified, additively and Galois-equivariantly, with eisensteinTorsionBar p q m, with H_m finite after base change there; morphisms \mathcal J_m\to\mathcal J_{m+1}\to Q_m whose composite vanishes, carrying as a field the assertion that the resulting short complex is short exact; a record \mathrm{inv}(m) of AdmissibleInvariants q whose components are pinned by equalities \#H^0_{\mathrm{fppf}}(\operatorname{Spec}\mathbb Z,\mathcal J_m)=q^{h^0}, \#H^1=q^{h^1}, \#\,eisensteinTorsionBar\,=q^{\delta}\cdot\#\,toricEisensteinPart, and, when q\neq p, \# of the convolution group of \mathbb F_q-algebra maps \overline{H}_m\to\overline{\mathbb F_q} equal to q^{\alpha}, where \overline{H}_m is a finite cocommutative Hopf \mathbb F_q-algebra presented as the quotient of H^{\mathrm{ff}}_{m,q} by the ideal generated by q; and a term of JKummerRow q m over the subgroup generated by eisensteinQuotientRational p (heckeModuleBar p), whose group H1Jtors is identified additively with H^1_{\mathrm{fppf}}(\operatorname{Spec}\mathbb Z,\mathcal J_m). Thus the sheaves are not constructed as Néron-model torsion but characterised by these pinnings. Finally HasJZeroNeronTorsionSheaf p q asserts that for every valuation subring of \overline{\mathbb Q} lying over p such a structure exists.

Relation to Mathlib

The ambient framework — sheaves on the small fppf site of a scheme, short exactness of short complexes in an abelian category, HopfAlgebra, Submodule.torsionBySet, flatness and finite type — is Mathlib's; JZero, HeckeAlg, the Eisenstein ideal and Eisenstein quotient, AdmissibleInvariants, JKummerRow, WithConv and the fppf cohomology groups used here are the project's own notions.

Where it is used

The structure is the interface on which the counting argument for the \mathfrak P^m-torsion of J_0(p) in the style of Mazur's Eisenstein-ideal paper is run: consumers combine the short exact sequences with the four numerical pinnings to obtain an Euler-characteristic inequality between h^0,h^1,\delta,\alpha, and use the Kummer row to compare H^1_{\mathrm{fppf}} with rational points of the Eisenstein quotient. The resulting bounds feed the project's treatment of rational p-torsion on elliptic curves over \mathbb Q, used in the Fermat deduction.

References

  1. B. Mazur, Modular curves and the Eisenstein ideal, Publications Mathématiques de l'IHÉS 47 (1977), 33–186
  2. J. S. Milne, Arithmetic Duality Theorems, Academic Press, 1986
  3. M. Raynaud, Schémas en groupes de type (p,\dots,p), Bulletin de la Société Mathématique de France 102 (1974), 241–280

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_JZeroNeronDataPrime
import Definitions.Def_ModularCurve_EisensteinIdeal
import Definitions.Def_ModularCurve_FppfKummerInterface
import Definitions.Def_ModularCurve_MazurStepThreeInputs
import Definitions.Def_AlgebraicGeometry_FppfSiteCohomology
import Definitions.Def_AlgebraicGeometry_FppfCohomologyLES
import Definitions.Def_AlgebraicGeometry_FppfKummerProp17
import Definitions.Def_ModularCurve_JZeroToricTorsion

set_option autoImplicit false

noncomputable section

namespace ModularCurve

open CategoryTheory AlgebraicGeometry AlgebraicGeometry.Scheme ValuationSubring Opposite

abbrev eisensteinTorsionBar (p q m : ℕ) [NeZero p] : AddSubgroup (JZero p) :=
  letI := heckeModuleBar p
  (Submodule.torsionBySet HeckeAlg (JZero p)
    (↑((eisensteinMaximalIdeal p q) ^ m) : Set HeckeAlg)).toAddSubgroup

abbrev toricEisensteinPart (p q : ℕ) [Fact p.Prime]
    (A : ValuationSubring (AlgebraicClosure ℚ)) (_hA : A.LiesOverPrime p) (m : ℕ) :
    AddSubgroup (JZero p) :=
  jZeroToricTorsion p A (q ^ m) ⊓ eisensteinTorsionBar p q m

structure JZeroNeronTorsionSheaf (p q : ℕ) [Fact p.Prime] [Fact q.Prime]
    (A : ValuationSubring (AlgebraicClosure ℚ)) (hA : A.LiesOverPrime p) where

  𝒥 : ℕ → Sheaf (smallFppfTopology specInt) Ab.{1}

  H : ℕ → Type
  [instCommRing_H : ∀ m, CommRing (H m)]
  [instHopfAlgebra_H : ∀ m, HopfAlgebra ℤ (H m)]
  [instFiniteType_H : ∀ m, Algebra.FiniteType ℤ (H m)]
  [instFlat_H : ∀ m, Module.Flat ℤ (H m)]

  ff_finite : ∀ (m ℓ : ℕ), ℓ.Prime → ℓ ≠ p →
    Module.Finite (GaloisRep.ratLocalizedAt ℓ) (TensorProduct ℤ (GaloisRep.ratLocalizedAt ℓ) (H m))

  sectionsEquiv : ∀ (m : ℕ) (U : specInt.Fppf),
    (𝒥 m).1.obj (op U) ≃+ Additive (WithConv (H m →ₐ[ℤ] Γ(U.left, ⊤)))

  sectionsNat : ∀ (m : ℕ) {U V : specInt.Fppf} (f : U ⟶ V) (s : (𝒥 m).1.obj (op V)),
    ∀ h : H m,
      (Additive.toMul (sectionsEquiv m U ((𝒥 m).1.map f.op s))) h
        = (Scheme.Γ.map f.left.op) ((Additive.toMul (sectionsEquiv m V s)) h)

  genericPoints : ∀ m, WithConv (H m →ₐ[ℤ] AlgebraicClosure ℚ) ≃ ↥(eisensteinTorsionBar p q m)

  genericConv : ∀ m, ∀ f g : WithConv (H m →ₐ[ℤ] AlgebraicClosure ℚ),
    genericPoints m (f * g) = genericPoints m f + genericPoints m g

  genericGalois : ∀ m, ∀ σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ,
    ∀ f g : WithConv (H m →ₐ[ℤ] AlgebraicClosure ℚ),
    (∀ h : H m, g h = σ (f h)) →
    ((genericPoints m g : ↥(eisensteinTorsionBar p q m)) : JZero p)
      = σ • ((genericPoints m f : ↥(eisensteinTorsionBar p q m)) : JZero p)

  pFibrePoints : ∀ m, WithConv (H m →ₐ[ℤ] ↥A) ≃ ↥(toricEisensteinPart p q A hA m)

  pFibreConv : ∀ m, ∀ f g : WithConv (H m →ₐ[ℤ] ↥A),
    pFibrePoints m (f * g) = pFibrePoints m f + pFibrePoints m g

  pFibreGenericCompat : ∀ m, ∀ φ : WithConv (H m →ₐ[ℤ] ↥A),
    ∀ ψ : WithConv (H m →ₐ[ℤ] AlgebraicClosure ℚ),
    (∀ h : H m, ψ h = A.subtype (φ h)) →
    ((pFibrePoints m φ : ↥(toricEisensteinPart p q A hA m)) : JZero p)
      = ((genericPoints m ψ : ↥(eisensteinTorsionBar p q m)) : JZero p)

  Hff : ∀ (_m : ℕ) (ℓ : ℕ), ℓ.Prime → ℓ ≠ p → Type
  [instCommRing_Hff : ∀ m ℓ hℓ hℓp, CommRing (Hff m ℓ hℓ hℓp)]
  [instHopfAlgebra_Hff : ∀ m ℓ hℓ hℓp, HopfAlgebra (GaloisRep.ratLocalizedAt ℓ) (Hff m ℓ hℓ hℓp)]
  [instFinite_Hff : ∀ m ℓ hℓ hℓp, Module.Finite (GaloisRep.ratLocalizedAt ℓ) (Hff m ℓ hℓ hℓp)]
  [instFlat_Hff : ∀ m ℓ hℓ hℓp, Module.Flat (GaloisRep.ratLocalizedAt ℓ) (Hff m ℓ hℓ hℓp)]
  [instCocomm_Hff : ∀ m ℓ hℓ hℓp, Coalgebra.IsCocomm (GaloisRep.ratLocalizedAt ℓ) (Hff m ℓ hℓ hℓp)]

  ffPoints : ∀ m ℓ hℓ hℓp, WithConv (Hff m ℓ hℓ hℓp →ₐ[GaloisRep.ratLocalizedAt ℓ] AlgebraicClosure ℚ)
    ≃ ↥(eisensteinTorsionBar p q m)

  ffConv : ∀ m ℓ hℓ hℓp, ∀ f g, ffPoints m ℓ hℓ hℓp (f * g)
    = ffPoints m ℓ hℓ hℓp f + ffPoints m ℓ hℓ hℓp g

  ffGalois : ∀ m ℓ hℓ hℓp, ∀ σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ,
    ∀ f g : WithConv (Hff m ℓ hℓ hℓp →ₐ[GaloisRep.ratLocalizedAt ℓ] AlgebraicClosure ℚ),
    (∀ h, g h = σ (f h)) →
    ((ffPoints m ℓ hℓ hℓp g : ↥(eisensteinTorsionBar p q m)) : JZero p)
      = σ • ((ffPoints m ℓ hℓ hℓp f : ↥(eisensteinTorsionBar p q m)) : JZero p)

  Q : ℕ → Sheaf (smallFppfTopology specInt) Ab.{1}

  incl : ∀ m, 𝒥 m ⟶ 𝒥 (m + 1)

  proj : ∀ m, 𝒥 (m + 1) ⟶ Q m

  incl_proj : ∀ m, incl m ≫ proj m = 0

  ses_shortExact : ∀ m, (ShortComplex.mk (incl m) (proj m) (incl_proj m)).ShortExact

  inv : ℕ → AdmissibleInvariants q

  h0_pin : ∀ m, Nat.card (fppfCohomology specInt (𝒥 m) 0) = q ^ (inv m).h0

  h1_pin : ∀ m, Nat.card (fppfCohomology specInt (𝒥 m) 1) = q ^ (inv m).h1

  δ_pin : ∀ m, Nat.card ↥(eisensteinTorsionBar p q m)
    = q ^ (inv m).δ * Nat.card ↥(toricEisensteinPart p q A hA m)

  HffBarQ : ∀ (_m : ℕ), q ≠ p → Type
  [instCommRing_HffBarQ : ∀ m hqp, CommRing (HffBarQ m hqp)]
  [instHopfAlgebra_HffBarQ : ∀ m hqp, HopfAlgebra (ZMod q) (HffBarQ m hqp)]
  [instFinite_HffBarQ : ∀ m hqp, Module.Finite (ZMod q) (HffBarQ m hqp)]
  [instCocomm_HffBarQ : ∀ m hqp, Coalgebra.IsCocomm (ZMod q) (HffBarQ m hqp)]

  ffBarQ_red : ∀ m hqp, Hff m q Fact.out hqp →+* HffBarQ m hqp

  ffBarQ_red_surjective : ∀ m hqp, Function.Surjective (ffBarQ_red m hqp)

  ffBarQ_red_ker : ∀ m hqp, RingHom.ker (ffBarQ_red m hqp)
    = Ideal.span {((q : ℤ) : Hff m q Fact.out hqp)}

  α_pin : ∀ m, ∀ hqp : q ≠ p,
    Nat.card (WithConv (HffBarQ m hqp →ₐ[ZMod q] AlgebraicClosure (ZMod q))) = q ^ (inv m).α

  kummerRow : ∀ m,
    letI := heckeModuleBar p
    JKummerRow q m ↥(AddSubgroup.closure (eisensteinQuotientRational p (heckeModuleBar p)))

  kummerRow_H1Jtors : ∀ m,
    letI := heckeModuleBar p; letI := (kummerRow m).instH1Jtors;
    (kummerRow m).H1Jtors ≃+ fppfCohomology specInt (𝒥 m) 1

attribute [instance] JZeroNeronTorsionSheaf.instCommRing_H JZeroNeronTorsionSheaf.instHopfAlgebra_H
  JZeroNeronTorsionSheaf.instFiniteType_H JZeroNeronTorsionSheaf.instFlat_H
  JZeroNeronTorsionSheaf.instCommRing_Hff JZeroNeronTorsionSheaf.instHopfAlgebra_Hff
  JZeroNeronTorsionSheaf.instFinite_Hff JZeroNeronTorsionSheaf.instFlat_Hff
  JZeroNeronTorsionSheaf.instCocomm_Hff
  JZeroNeronTorsionSheaf.instCommRing_HffBarQ JZeroNeronTorsionSheaf.instHopfAlgebra_HffBarQ
  JZeroNeronTorsionSheaf.instFinite_HffBarQ JZeroNeronTorsionSheaf.instCocomm_HffBarQ

def HasJZeroNeronTorsionSheaf (p q : ℕ) [Fact p.Prime] [Fact q.Prime] : Prop :=
  ∀ (A : ValuationSubring (AlgebraicClosure ℚ)) (hA : A.LiesOverPrime p),
    Nonempty (JZeroNeronTorsionSheaf p q A hA)

section Falseprobe

end Falseprobe

end ModularCurve

end

Statements phrased using this module (35)