Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_JZeroNeronObjectAtP_NeronExtension.lean

definition module

Néron extensions over the inertia-fixed valuation ring

Fix N_0\ge 1, a prime p with p\nmid N_0, a valuation subring A of \overline{\mathbb Q} lying over p, level data \Lambda at p read at A, and an object O of type JZeroNeronObjectAtP for these data. The first group of declarations builds the base over which the extension lives: invField A is the fixed field \overline{\mathbb Q}^{I_A} of the inertia subgroup A.inertiaSubgroupIn ℚ, shRing A is the valuation subring of that field obtained by pulling A back along the inclusion, shBase A its spectrum, shToPlace the induced ring map \mathrm{shRing}\,A\to A (with coe_shToPlace recording that it is the identity on underlying elements of \overline{\mathbb Q}) and shPt the corresponding morphism \operatorname{Spec} A\to \mathrm{shBase}\,A. In the LevelData namespace, baseToPlace is the ring map \mathbb Z_{(p)}=\mathrm{baseRing}\,p\to A underlying \Lambda.\sigma_A, baseToSh its factorisation through \mathrm{shRing}\,A (rational elements being inertia-fixed), shStr the resulting structure morphism \mathrm{shBase}\,A\to\mathrm{base}\,p, together with the commutations \mathrm{shStr}\circ\mathrm{shPt}=\sigma_A and \mathrm{shStr}\circ\mathrm{shPt}\circ\mathrm{barPt}=\mathrm{genPt}, and shLift, shGenLift, which transport A-points and \overline{\mathbb Q}-points of a scheme over \mathrm{base}\,p to points of its base change along shStr.

The structure NeronExtension O then packages: a scheme \mathcal N with a morphism g_{\mathcal N} to \mathrm{shBase}\,A and a commutative relative group law over \mathrm{shRing}\,A; a field hN asserting, under the hypothesis that \mathrm{shRing}\,A is a Dedekind domain, the Néron property bundle for g_{\mathcal N} relative to \mathrm{invField}\,A (smooth, separated, locally of finite type, quasi-compact, and for every smooth T\to\operatorname{Spec}\mathrm{shRing}\,A restriction to the generic fibre is bijective on sections); a morphism openImm from the base change of O.g along shStr into \mathcal N over \mathrm{shBase}\,A, required to be an open immersion, to be a homomorphism on T-valued points for all T, and to be surjective on points over \mathrm{shPt}\circ\mathrm{barPt} with all such points coming from \Lambda.\mathrm{shGenLift}(O.\mathrm{pts}\,x), x\in\mathrm{JZero}(N_0p); and a map specN from points of g_{\mathcal N} over \mathrm{shPt}\,A to componentGroup O.width, which is additive, surjective, vanishes exactly on the points obtained through openImm from points of O.g over \sigma_A, and satisfies comp_eq_specN: for x in inertiaInvariants A (N₀ * p), if the point attached to x equals s\circ\mathrm{barPt} for an A-point s, then O.\mathrm{comp}\,x=\mathrm{specN}\,s.

Finally, ptsN F x names the point of \mathcal N attached to x\in\mathrm{JZero}(N_0p), ExtN F x says that this point factors as s\circ\mathrm{barPt} for some point s over \mathrm{shPt}\,A, and finPts F m is the subgroup of \mathrm{JZero}(N_0p) generated by the m-torsion elements satisfying ExtN.

Relation to Mathlib

Mathlib has no Néron models, relative group laws or component groups of degenerating Jacobians; RelativeGroupLaw, NeronModelPropertyBundle and componentGroup are the project's own notions, while the base ring here is assembled from Mathlib's ValuationSubring, IntermediateField.fixedField and Spec.

Where it is used

These definitions provide the geometric object over the valuation ring of the inertia-fixed field on which the comparison between A-points of the full Néron model of J_0(N_0p) and the component group of widths is made, the input to the component-group and specialisation arguments used in the level-lowering step at p.

References

  1. M. Raynaud, Spécialisation du foncteur de Picard, Publ. Math. IHÉS 38 (1970), 27–76
  2. S. Bosch, W. Lütkebohmert and M. Raynaud, Néron Models, Ergebnisse der Mathematik und ihrer Grenzgebiete 21, Springer, 1990
  3. A. Grothendieck et al., Groupes de monodromie en géométrie algébrique (SGA 7 I), Exposé IX, Lecture Notes in Mathematics 288, Springer, 1972

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_JZeroNeronObjectAtP
import Definitions.Def_AlgebraicGeometry_NeronModelPropertyBundleCarrier

set_option autoImplicit false

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  AlgebraicCurve IsLocalRing

noncomputable section

namespace ModularCurve

namespace JZeroNeronObjectAtP

attribute [local instance] instDecidableEqResidueFieldSemistable
  instAlgebraResidueFieldModularFunctionFieldCSemistable

section ShBase

variable (A : ValuationSubring (AlgebraicClosure ℚ))

abbrev invField : IntermediateField ℚ (AlgebraicClosure ℚ) :=
  IntermediateField.fixedField (A.inertiaSubgroupIn ℚ)

abbrev shRing : ValuationSubring ↥(invField A) :=
  A.comap (algebraMap ↥(invField A) (AlgebraicClosure ℚ))

abbrev shBase : Scheme.{0} := Spec (CommRingCat.of ↥(shRing A))

def shToPlace : ↥(shRing A) →+* ↥A :=
  ((algebraMap ↥(invField A) (AlgebraicClosure ℚ)).comp (shRing A).subtype).codRestrict A.toSubring
    (fun x => x.2)

@[simp]
theorem coe_shToPlace (x : ↥(shRing A)) :
    ((shToPlace A x : ↥A) : AlgebraicClosure ℚ) = ((x : ↥(invField A)) : AlgebraicClosure ℚ) := rfl

abbrev shPt : Spec (CommRingCat.of ↥A) ⟶ shBase A := Spec.map (CommRingCat.ofHom (shToPlace A))

end ShBase

namespace LevelData

variable {N₀ p : ℕ} [NeZero N₀] {A : ValuationSubring (AlgebraicClosure ℚ)} (Λ : LevelData N₀ p A)

def baseToPlace : baseRing p →+* ↥A := (Spec.preimage Λ.σA).hom

theorem specMap_baseToPlace : Spec.map (CommRingCat.ofHom Λ.baseToPlace) = Λ.σA := by
  rw [baseToPlace, CommRingCat.ofHom_hom, Spec.map_preimage]

theorem coe_baseToPlace (r : baseRing p) :
    ((Λ.baseToPlace r : ↥A) : AlgebraicClosure ℚ) = algebraMap (baseRing p) (AlgebraicClosure ℚ) r := by
  have h1 := Λ.hσA
  rw [← Λ.specMap_baseToPlace, barPt, genPt, ← Spec.map_comp] at h1
  have := congrArg (fun f => (f : baseRing p →+* AlgebraicClosure ℚ) r)
    (congrArg CommRingCat.Hom.hom (Spec.map_injective h1))
  simpa using this

theorem algebraMap_baseRing_eq (r : baseRing p) :
    algebraMap (baseRing p) (AlgebraicClosure ℚ) r = algebraMap ℚ (AlgebraicClosure ℚ) (r : ℚ) := rfl

def baseToSh : baseRing p →+* ↥(shRing A) where
  toFun r := ⟨⟨algebraMap (baseRing p) (AlgebraicClosure ℚ) r, by
      rw [IntermediateField.mem_fixedField_iff]
      intro σ _
      rw [algebraMap_baseRing_eq, AlgEquiv.commutes]⟩, by
      change algebraMap (baseRing p) (AlgebraicClosure ℚ) r ∈ A
      rw [← Λ.coe_baseToPlace]; exact (Λ.baseToPlace r).2⟩
  map_one' := by apply Subtype.ext; apply Subtype.ext; exact map_one _
  map_mul' x y := by apply Subtype.ext; apply Subtype.ext; exact map_mul _ x y
  map_zero' := by apply Subtype.ext; apply Subtype.ext; exact map_zero _
  map_add' x y := by apply Subtype.ext; apply Subtype.ext; exact map_add _ x y

theorem shToPlace_comp_baseToSh : (shToPlace A).comp Λ.baseToSh = Λ.baseToPlace := by
  ext r
  exact (Λ.coe_baseToPlace r).symm

abbrev shStr : shBase A ⟶ base p := Spec.map (CommRingCat.ofHom Λ.baseToSh)

theorem shPt_comp_shStr : shPt A ≫ Λ.shStr = Λ.σA := by
  rw [shPt, shStr, ← Spec.map_comp, ← CommRingCat.ofHom_comp, shToPlace_comp_baseToSh, specMap_baseToPlace]

theorem barPt_shPt_shStr : (barPt A ≫ shPt A) ≫ Λ.shStr = genPt p := by
  rw [Category.assoc, shPt_comp_shStr, Λ.hσA]

def shLift {X : Scheme.{0}} {f : X ⟶ base p} (s : SchemeHomOver Λ.σA f) :
    SchemeHomOver (shPt A) (RelativeGroupLaw.baseChangeStr Λ.shStr f) :=
  RelativeGroupLaw.baseChangePointOfBase Λ.shStr (castOver Λ.shPt_comp_shStr.symm s)

def shGenLift {X : Scheme.{0}} {f : X ⟶ base p} (y : SchemeHomOver (genPt p) f) :
    SchemeHomOver (barPt A ≫ shPt A) (RelativeGroupLaw.baseChangeStr Λ.shStr f) :=
  RelativeGroupLaw.baseChangePointOfBase Λ.shStr (castOver Λ.barPt_shPt_shStr.symm y)

end LevelData

variable {N₀ p : ℕ} [NeZero N₀] [Fact p.Prime] [NeZero p] {hpN₀ : ¬ p ∣ N₀}
  {A : ValuationSubring (AlgebraicClosure ℚ)} {hA : A.LiesOverPrime p}
  {Λ : LevelData N₀ p A}

set_option synthInstance.maxHeartbeats 400000 in
set_option maxHeartbeats 4000000 in

structure NeronExtension (O : JZeroNeronObjectAtP N₀ p hpN₀ A hA Λ) : Type 1 where

  Nfull : Scheme.{0}

  gN : Nfull ⟶ shBase A

  LN : RelativeGroupLaw ↥(shRing A) gN

  commN : LN.IsCommutative

  hN : ∀ [IsDedekindDomain ↥(shRing A)], NeronModelPropertyBundle ↥(shRing A) ↥(invField A) gN

  openImm : SchemeHomOver (RelativeGroupLaw.baseChangeStr Λ.shStr O.g) gN

  openImm_isOpenImmersion : IsOpenImmersion openImm.1

  openImm_mul : ∀ {T : Scheme.{0}} (s : T ⟶ shBase A)
      (x y : SchemeHomOver s (RelativeGroupLaw.baseChangeStr Λ.shStr O.g)),
      NeronModelInfra.schemeHomOverComp ((O.L.baseChange Λ.shStr).mul s x y) openImm =
        LN.mul s (NeronModelInfra.schemeHomOverComp x openImm) (NeronModelInfra.schemeHomOverComp y openImm)

  openImm_pts_surjective : ∀ y : SchemeHomOver (barPt A ≫ shPt A) gN,
      ∃ x : JZero (N₀ * p), NeronModelInfra.schemeHomOverComp (Λ.shGenLift (O.pts x)) openImm = y

  specN : SchemeHomOver (shPt A) gN → componentGroup O.width

  specN_mul : ∀ s s' : SchemeHomOver (shPt A) gN, specN (LN.mul (shPt A) s s') = specN s + specN s'

  specN_surjective : Function.Surjective specN

  specN_eq_zero_iff : ∀ s : SchemeHomOver (shPt A) gN,
      specN s = 0 ↔ ∃ s₀ : SchemeHomOver Λ.σA O.g, NeronModelInfra.schemeHomOverComp (Λ.shLift s₀) openImm = s

  comp_eq_specN : ∀ (x : ↥(inertiaInvariants A (N₀ * p))) (s : SchemeHomOver (shPt A) gN),
      (NeronModelInfra.schemeHomOverComp (Λ.shGenLift (O.pts (x : JZero (N₀ * p)))) openImm).1 = barPt A ≫ s.1 →
        O.comp x = specN s

namespace NeronExtension

variable {O : JZeroNeronObjectAtP N₀ p hpN₀ A hA Λ}

abbrev ptsN (F : O.NeronExtension) (x : JZero (N₀ * p)) : SchemeHomOver (barPt A ≫ shPt A) F.gN :=
  NeronModelInfra.schemeHomOverComp (Λ.shGenLift (O.pts x)) F.openImm

def ExtN (F : O.NeronExtension) (x : JZero (N₀ * p)) : Prop :=
  ∃ s : SchemeHomOver (shPt A) F.gN, (F.ptsN x).1 = barPt A ≫ s.1

def finPts (F : O.NeronExtension) (m : ℕ) : AddSubgroup (JZero (N₀ * p)) :=
  AddSubgroup.closure {x | x ∈ jZeroTorsion (N₀ * p) m ∧ F.ExtN x}

end NeronExtension

end JZeroNeronObjectAtP

end ModularCurve

end

Statements phrased using this module (24)