Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_JHNeronObjectAtP.lean

definition module

Néron interface for at a prime dividing

Fix a prime p, an integer M\ge 1 with p\mid M, a subgroup H\le(\mathbb Z/M)^\times, and a valuation subring A of \overline{\mathbb Q} lying over p whose residue field \kappa is algebraically closed of characteristic p. Two abbreviations set the lower level: ΓN is the congruence subgroup CohCarrier.GammaH (M / p) of the subgroup of (\mathbb Z/(M/p))^\times produced from H by infSubgroup, and Fbar is the q-expansion function field qExpFunctionFieldC κ (ΓN …) attached to it. LevelData packages the lower-level datum: a morphism \sigma_A:\operatorname{Spec}A\to\operatorname{Spec} of the base ring baseRing p with \overline{\mathbb Q}-point factoring the generic point, a scheme X over that base with a relative group law L, a bijection of J_{H'}(M/p) with the sections over the geometric generic point, and a bijection of \mathrm{Pic}^0(\kappa, Fbar ) with the sections over the residue point.

The structure JHNeronObjectAtP then records, relative to such a \Lambda, a scheme G\to\operatorname{Spec}baseRing p with a commutative relative group law L, smooth, separated, locally of finite type, quasi-compact, surjective, with preconnected fibres and proper generic fibre, multiplication by n>0 flat and surjective; a bijection pts of J_H(M) with its sections over the geometric generic point, additive and equivariant for \operatorname{Gal}(\overline{\mathbb Q}/\mathbb Q); for each generator t of CohCarrier.Gen M S an endomorphism over the base, additive on sections and inducing genOpH M H S t on J_H(M); a toric rank t_0, a closed immersion torusFibre of the split torus of rank t_0 into the special fibre, multiplicative on characters; two additive maps abqFibre from the special fibre of g to that of \Lambda.f whose pair is flat and surjective and whose joint kernel is exactly the image of the torus, commuting with automorphisms of the residue base; a finite set ssFinset of pairs of places equal to ssNodePairsQExp …, with t_0+1 its cardinality; a bijection ptsSp of GluedPic0 κ Fbar ssFinset with the sections over the residue point, additive, carrying the two abqFibre to the two components of GluedPic0.toPic0Pair and the range of GluedPic0.nodeUnit to the points factoring through the torus; two additive maps degPts from J_H(M) to J_{H'}(M/p) together with two homomorphisms degeneracyHom over the base inducing them on points, whose effect on residue points is Ribet's matrix: for a unit \bar e of \mathbb Z/(M/p) with \bar e\,p=1, one degeneracy map is abqFibre 0 plus the Frobenius push-forward of abqFibre 1, the other the Frobenius push-forward of abqFibre 0 plus the diamond operator attached to \bar e applied to abqFibre 1; and, for every m>0, a closed immersion toricLift of the \mu_m^{t_0}-scheme over A into the base change of g along \sigma_A, multiplicative on characters, compatible as m\mid m', reducing to torusFibre over \kappa, on which inertia acts through the cyclotomic character (\sigma\zeta=\zeta^c forces \sigma\cdot x=c\cdot x) and the decomposition group permutes the character points. The field hecke_special_twist asserts only the existence of a section of g over the residue point with the same underlying morphism as a given composite, which any such composite satisfies.

The remaining declarations read off data from an object O: toricPoint O m hm χ is the element of J_H(M) corresponding to the \mu_m-character point \chi composed with toricLift m hm, transported by pts.symm; toricPts O m is the subgroup generated by all these (and \bot for m=0); finPts O m is the subgroup generated by the m-torsion of \mathrm{Pic}^0(\overline{\mathbb Q}, xHFunctionFieldBar M H ) whose section extends over A in the sense of ExtendsToPlace; and Pts O is the type of sections over the geometric generic point, given the additive group structure transported along pts, with ptsAddEquiv the resulting additive isomorphism J_H(M)\cong O.Pts.

Relation to Mathlib

Mathlib has no Néron models, relative group laws or generalised Jacobians; the group law, base change, fibre restriction and glued \mathrm{Pic}^0 notions used here are the project's own, built on Mathlib's scheme pullbacks and Spec functoriality. The structure pins the object by its points and listed properties rather than by the Néron mapping property.

Where it is used

This is the level-\Gamma_H(M) counterpart of the \Gamma_0(N_0p) interface, describing the identity component of the Néron model of J_H(M) over \mathbb Z_{(p)} for p exactly dividing M: the split toric part of the special fibre, the two degeneracy maps to the lower level with Ribet's matrix, and the inertia action on the \mu_m-lifts. These are the inputs to the level-lowering step (Mazur's principle and Ribet's theorem) that removes the prime p from the level of the modular form attached to a Frey curve.

References

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

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_JZeroNeronObjectAtP
import Definitions.Def_GoodReductionJacobian_RelativeGroupLawBaseChange
import Definitions.Def_AlgebraicGeometry_NeronSpecialFibreRestriction
import Definitions.Def_ModularCurve_XHDifferentialsModL
import Definitions.Def_ModularCurve_XHOperators
import Definitions.Def_AlgebraicCurve_GluedPic0
import Definitions.Def_GaloisRep_Flat
import Definitions.Def_FLTPrelim_Ramification

set_option autoImplicit false
set_option maxHeartbeats 800000
set_option synthInstance.maxHeartbeats 400000

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  AlgebraicCurve IsLocalRing
open ModularCurve.JZeroNeronObjectAtP
open scoped MatrixGroups

noncomputable section

namespace ModularCurve

namespace JHNeronObjectAtP

abbrev ΓN (p M : ℕ) (H : Subgroup (ZMod M)ˣ) (hpM : p ∣ M) : Subgroup SL(2, ℤ) :=
  CohCarrier.GammaH (M / p) (infSubgroup p M H hpM)

abbrev Fbar (p M : ℕ) (H : Subgroup (ZMod M)ˣ) (hpM : p ∣ M) (κ : Type) [Field κ] : Type :=
  ↥(qExpFunctionFieldC κ (ΓN p M H hpM))

structure LevelData (p M : ℕ) [NeZero M] (H : Subgroup (ZMod M)ˣ) (hpM : p ∣ M)
    (A : ValuationSubring (AlgebraicClosure ℚ)) where

  σA : Spec (CommRingCat.of ↥A) ⟶ base p

  hσA : barPt A ≫ σA = genPt p

  X : Scheme.{0}

  f : X ⟶ base p

  L : RelativeGroupLaw (baseRing p) f

  pts : JH (M / p) (infSubgroup p M H hpM) ≃ SchemeHomOver (genPt p) f

  ptsSp : Pic0 (ResidueField ↥A) (Fbar p M H hpM (ResidueField ↥A)) ≃ SchemeHomOver (resPt A ≫ σA) f

end JHNeronObjectAtP

open JHNeronObjectAtP in

structure JHNeronObjectAtP (p M : ℕ) [Fact p.Prime] [NeZero M] (H : Subgroup (ZMod M)ˣ) (hpM : p ∣ M)
    (A : ValuationSubring (AlgebraicClosure ℚ)) (hA : A.LiesOverPrime p)
    [CharP (ResidueField ↥A) p] [IsAlgClosed (ResidueField ↥A)]
    (Λ : JHNeronObjectAtP.LevelData p M H hpM A) where

  G : Scheme.{0}

  g : G ⟶ base p

  L : RelativeGroupLaw (baseRing p) g

  pts : JH M H ≃ SchemeHomOver (genPt p) g

  comm : L.IsCommutative

  smooth : Smooth g
  separated : IsSeparated g
  locallyOfFiniteType : LocallyOfFiniteType g
  quasiCompact : QuasiCompact g
  surjective : Surjective g
  fibre_preconnected : ∀ s : base p, _root_.IsPreconnected (g.base ⁻¹' {s})

  pts_add : ∀ x y : JH M H, pts (x + y) = L.mul _ (pts x) (pts y)

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

  hecke : ∀ (S : Set ℕ), CohCarrier.Gen M S → SchemeHomOver g g

  hecke_mul : ∀ (S : Set ℕ) (t : CohCarrier.Gen M S) {T : Scheme.{0}} (s : T ⟶ base p) (x y : SchemeHomOver s g),
    NeronModelInfra.schemeHomOverComp (L.mul s x y) (hecke S t) =
      L.mul s (NeronModelInfra.schemeHomOverComp x (hecke S t)) (NeronModelInfra.schemeHomOverComp y (hecke S t))

  hecke_pts : ∀ (S : Set ℕ) (t : CohCarrier.Gen M S) (x : JH M H),
    (pts (genOpH M H S t x)).1 = (pts x).1 ≫ (hecke S t).1

  nsmul_flat : ∀ n : ℕ, 0 < n → Flat (L.schemeNsmul n)
  nsmul_surjective : ∀ n : ℕ, 0 < n → Surjective (L.schemeNsmul n)

  proper_generic : IsProper (pullback.snd g (Spec.map (CommRingCat.ofHom (algebraMap (baseRing p) ℚ))))

  toricRank : ℕ

  torusFibre : SchemeHomOver (torusStr (ResidueField ↥A) toricRank)
      (RelativeGroupLaw.baseChangeStr (resPt A ≫ Λ.σA) g)

  torusFibre_isClosedImmersion : IsClosedImmersion torusFibre.1

  torusFibre_mul :
    ∀ χ χ' : WithConv (torusCoord (ResidueField ↥A) toricRank →ₐ[ResidueField ↥A] ResidueField ↥A),
      NeronModelInfra.schemeHomOverComp (torusPt _ _ (χ * χ').ofConv) torusFibre =
        (L.baseChange (resPt A ≫ Λ.σA)).mul _
          (NeronModelInfra.schemeHomOverComp (torusPt _ _ χ.ofConv) torusFibre)
          (NeronModelInfra.schemeHomOverComp (torusPt _ _ χ'.ofConv) torusFibre)

  abqFibre : Fin 2 → SchemeHomOver (RelativeGroupLaw.baseChangeStr (resPt A ≫ Λ.σA) g)
      (RelativeGroupLaw.baseChangeStr (resPt A ≫ Λ.σA) Λ.f)
  abqFibre_mul : ∀ (i : Fin 2) {T : Scheme.{0}} (s : T ⟶ Spec (CommRingCat.of (ResidueField ↥A)))
      (x y : SchemeHomOver s (RelativeGroupLaw.baseChangeStr (resPt A ≫ Λ.σA) g)),
      NeronModelInfra.schemeHomOverComp ((L.baseChange (resPt A ≫ Λ.σA)).mul s x y) (abqFibre i) =
        (Λ.L.baseChange (resPt A ≫ Λ.σA)).mul s (NeronModelInfra.schemeHomOverComp x (abqFibre i))
          (NeronModelInfra.schemeHomOverComp y (abqFibre i))
  abqFibre_flat : Flat (pullback.lift (abqFibre 0).1 (abqFibre 1).1 ((abqFibre 0).2.trans (abqFibre 1).2.symm))
  abqFibre_surjective :
    Surjective (pullback.lift (abqFibre 0).1 (abqFibre 1).1 ((abqFibre 0).2.trans (abqFibre 1).2.symm))

  abqFibre_eq_one_iff : ∀ {T : Scheme.{0}} (s : T ⟶ Spec (CommRingCat.of (ResidueField ↥A)))
      (x : SchemeHomOver s (RelativeGroupLaw.baseChangeStr (resPt A ≫ Λ.σA) g)),
      (∀ i, NeronModelInfra.schemeHomOverComp x (abqFibre i) = (Λ.L.baseChange (resPt A ≫ Λ.σA)).one s) ↔
        ∃ y : SchemeHomOver s (torusStr (ResidueField ↥A) toricRank),
          NeronModelInfra.schemeHomOverComp y torusFibre = x

  abqFibre_twist : ∀ (τ : SchemeHomOver (resPt A ≫ Λ.σA) (resPt A ≫ Λ.σA)) (i : Fin 2)
      (x : SchemeHomOver (resPt A ≫ Λ.σA) g),
      fibreMap (abqFibre i) (GoodReductionJacobian.schemeHomOverComp τ.1 τ.2 x) =
        GoodReductionJacobian.schemeHomOverComp τ.1 τ.2 (fibreMap (abqFibre i) x)

  ssFinset : Finset (Place (ResidueField ↥A) (Fbar p M H hpM (ResidueField ↥A)) ×
    Place (ResidueField ↥A) (Fbar p M H hpM (ResidueField ↥A)))

  mem_ssFinset_iff : ∀ s, s ∈ ssFinset ↔ s ∈ ssNodePairsQExp (ResidueField ↥A) (ΓN p M H hpM) p

  toricRank_succ_eq_card : toricRank + 1 = ssFinset.card

  ptsSp : GluedPic0 (ResidueField ↥A) (Fbar p M H hpM (ResidueField ↥A)) ssFinset ≃
    SchemeHomOver (resPt A ≫ Λ.σA) g

  ptsSp_add : ∀ x y, ptsSp (x + y) =
      ofFibrePt ((L.baseChange (resPt A ≫ Λ.σA)).mul _ (toFibrePt (ptsSp x)) (toFibrePt (ptsSp y)))

  abqFibre_ptsSp : ∀ (x : GluedPic0 (ResidueField ↥A) (Fbar p M H hpM (ResidueField ↥A)) ssFinset) (i : Fin 2),
      Λ.ptsSp.symm (fibreMap (abqFibre i) (ptsSp x)) =
        if i = 0 then (GluedPic0.toPic0Pair ssFinset x).1 else (GluedPic0.toPic0Pair ssFinset x).2

  torus_ptsSp : ∀ x : GluedPic0 (ResidueField ↥A) (Fbar p M H hpM (ResidueField ↥A)) ssFinset,
      (∃ y : SchemeHomOver (𝟙 _) (torusStr (ResidueField ↥A) toricRank),
          NeronModelInfra.schemeHomOverComp y torusFibre = toFibrePt (ptsSp x)) ↔
        x ∈ (GluedPic0.nodeUnit ssFinset).range

  hecke_special_twist : ∀ (S : Set ℕ) (t : CohCarrier.Gen M S) (x : SchemeHomOver (resPt A ≫ Λ.σA) g),
      ∃ x' : SchemeHomOver (resPt A ≫ Λ.σA) g, (NeronModelInfra.schemeHomOverComp x (hecke S t)).1 = x'.1

  degPts : Fin 2 → (JH M H →+ JH (M / p) (infSubgroup p M H hpM))

  degeneracyHom : Fin 2 → SchemeHomOver g Λ.f
  degeneracyHom_mul : ∀ (i : Fin 2) {T : Scheme.{0}} (s : T ⟶ base p) (x y : SchemeHomOver s g),
      NeronModelInfra.schemeHomOverComp (L.mul s x y) (degeneracyHom i) =
        Λ.L.mul s (NeronModelInfra.schemeHomOverComp x (degeneracyHom i))
          (NeronModelInfra.schemeHomOverComp y (degeneracyHom i))

  degeneracyHom_pts : ∀ (i : Fin 2) (x : JH M H),
      (Λ.pts (degPts i x)).1 = (pts x).1 ≫ (degeneracyHom i).1

  degeneracyHom_special : ∀ (ē : (ZMod (M / p))ˣ), ((ē : (ZMod (M / p))ˣ) : ZMod (M / p)) * (p : ZMod (M / p)) = 1 →
    haveI : NeZero (M / p) := neZero_div p M hpM
    ∀ x : SchemeHomOver (resPt A ≫ Λ.σA) g,
      Λ.ptsSp.symm (NeronModelInfra.schemeHomOverComp x (degeneracyHom 0)) =
          Λ.ptsSp.symm (fibreMap (abqFibre 0) x) +
            qExpFrobeniusPushforwardModL (ResidueField ↥A) (ΓN p M H hpM) p (Λ.ptsSp.symm (fibreMap (abqFibre 1) x)) ∧
      Λ.ptsSp.symm (NeronModelInfra.schemeHomOverComp x (degeneracyHom 1)) =
          qExpFrobeniusPushforwardModL (ResidueField ↥A) (ΓN p M H hpM) p (Λ.ptsSp.symm (fibreMap (abqFibre 0) x)) +
            SemilinearAut.ofAlgAut (diamondActionModL (ResidueField ↥A) (M / p) (infSubgroup p M H hpM) (CuspForm.gammaLift (M / p) ē)) •
              Λ.ptsSp.symm (fibreMap (abqFibre 1) x)

  toricLift : ∀ m : ℕ, 0 < m → SchemeHomOver (muStr ↥A toricRank m) (RelativeGroupLaw.baseChangeStr Λ.σA g)
  toricLift_isClosedImmersion : ∀ (m : ℕ) (hm : 0 < m), IsClosedImmersion (toricLift m hm).1
  toricLift_mul : ∀ (m : ℕ) (hm : 0 < m) (χ χ' : WithConv (muCoord ↥A toricRank m →ₐ[↥A] AlgebraicClosure ℚ)),
      NeronModelInfra.schemeHomOverComp (muPt A toricRank m (χ * χ').ofConv) (toricLift m hm) =
        (L.baseChange Λ.σA).mul _ (NeronModelInfra.schemeHomOverComp (muPt A toricRank m χ.ofConv) (toricLift m hm))
          (NeronModelInfra.schemeHomOverComp (muPt A toricRank m χ'.ofConv) (toricLift m hm))
  toricLift_compat : ∀ (m m' : ℕ) (hm : 0 < m) (hm' : 0 < m') (h : m ∣ m'),
      muIncl ↥A toricRank h ≫ (toricLift m' hm').1 = (toricLift m hm).1
  toricLift_special : ∀ (m : ℕ) (hm : 0 < m),
      muBaseChange (residue ↥A) toricRank m ≫ (toricLift m hm).1 ≫ pullback.fst g Λ.σA =
        muToTorus (ResidueField ↥A) toricRank m ≫ torusFibre.1 ≫ pullback.fst g (resPt A ≫ Λ.σA)
  toricLift_inertia : ∀ (m : ℕ) (hm : 0 < m), ∀ σ ∈ A.inertiaSubgroupIn ℚ, ∀ c : ℕ,
      (∀ ζ : AlgebraicClosure ℚ, ζ ^ m = 1 → σ ζ = ζ ^ c) →
      ∀ χ : muCoord ↥A toricRank m →ₐ[↥A] AlgebraicClosure ℚ,
        σ • pts.symm (genOfBaseChangePt Λ.hσA
            (NeronModelInfra.schemeHomOverComp (muPt A toricRank m χ) (toricLift m hm))) =
          c • pts.symm (genOfBaseChangePt Λ.hσA
            (NeronModelInfra.schemeHomOverComp (muPt A toricRank m χ) (toricLift m hm)))
  toricLift_dec : ∀ (m : ℕ) (hm : 0 < m), ∀ σ ∈ A.decompositionSubgroup ℚ,
      ∀ χ : muCoord ↥A toricRank m →ₐ[↥A] AlgebraicClosure ℚ,
        ∃ χ' : muCoord ↥A toricRank m →ₐ[↥A] AlgebraicClosure ℚ,
          σ • pts.symm (genOfBaseChangePt Λ.hσA
              (NeronModelInfra.schemeHomOverComp (muPt A toricRank m χ) (toricLift m hm))) =
            pts.symm (genOfBaseChangePt Λ.hσA
              (NeronModelInfra.schemeHomOverComp (muPt A toricRank m χ') (toricLift m hm)))

attribute [nolint docBlame] JHNeronObjectAtP.separated JHNeronObjectAtP.locallyOfFiniteType
  JHNeronObjectAtP.quasiCompact JHNeronObjectAtP.surjective JHNeronObjectAtP.nsmul_surjective
  JHNeronObjectAtP.toricLift JHNeronObjectAtP.toricLift_isClosedImmersion JHNeronObjectAtP.toricLift_mul
  JHNeronObjectAtP.toricLift_compat JHNeronObjectAtP.toricLift_special JHNeronObjectAtP.toricLift_inertia
  JHNeronObjectAtP.toricLift_dec JHNeronObjectAtP.abqFibre_flat JHNeronObjectAtP.abqFibre_surjective
  JHNeronObjectAtP.abqFibre_mul JHNeronObjectAtP.degeneracyHom_mul

namespace JHNeronObjectAtP

variable {p M : ℕ} [Fact p.Prime] [NeZero M] {H : Subgroup (ZMod M)ˣ} {hpM : p ∣ M}
  {A : ValuationSubring (AlgebraicClosure ℚ)} {hA : A.LiesOverPrime p}
  [CharP (ResidueField ↥A) p] [IsAlgClosed (ResidueField ↥A)]
  {Λ : LevelData p M H hpM A}

def toricPoint (O : JHNeronObjectAtP p M H hpM A hA Λ) (m : ℕ) (hm : 0 < m)
    (χ : muCoord ↥A O.toricRank m →ₐ[↥A] AlgebraicClosure ℚ) : JH M H :=
  O.pts.symm (genOfBaseChangePt Λ.hσA
    (NeronModelInfra.schemeHomOverComp (muPt A O.toricRank m χ) (O.toricLift m hm)))

def toricPts (O : JHNeronObjectAtP p M H hpM A hA Λ) (m : ℕ) : AddSubgroup (JH M H) :=
  if hm : 0 < m then AddSubgroup.closure (Set.range (O.toricPoint m hm)) else ⊥

def finPts (O : JHNeronObjectAtP p M H hpM A hA Λ) (m : ℕ) : AddSubgroup (JH M H) :=
  AddSubgroup.closure {x | x ∈ Pic0.torsion (AlgebraicClosure ℚ) (xHFunctionFieldBar M H) m ∧ ExtendsToPlace A Λ.σA (O.pts x)}

def Pts (O : JHNeronObjectAtP p M H hpM A hA Λ) : Type := SchemeHomOver (genPt p) O.g

instance (O : JHNeronObjectAtP p M H hpM A hA Λ) : AddCommGroup O.Pts := O.pts.symm.addCommGroup

def ptsAddEquiv (O : JHNeronObjectAtP p M H hpM A hA Λ) : JH M H ≃+ O.Pts :=
  ((show O.Pts ≃ JH M H from O.pts.symm).addEquiv).symm

end JHNeronObjectAtP

end ModularCurve

end

Statements phrased using this module (468)

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