Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_DRResolvedModelPackageLevelRam.lean

definition module

Resolved Deligne–Rapoport model package over a ramified base

Fix N_0\ge 1, a prime q\nmid N_0, a Deligne–Rapoport model package \mathfrak{X} of level N_0q over R= R q (the localisation of \mathbb{Q} at q), a ring map \rho\colon R\to O, an element \varpi\in O, an algebraically closed field \kappa of characteristic q and a ring map \mathrm{to}\kappa\colon O\to\kappa. The helper ModularCurve.DRLevel.unifOn toBase ϖ U is the image of \varpi in \Gamma(Y,U) for an affine open U of a scheme Y equipped with a morphism toBase to \operatorname{Spec} O: the global section obtained from \varpi by the morphism on structure sheaves, restricted to U; unifOn_natCast records that for \varpi=(n:O) with n a natural number this is (n:\Gamma(Y,U)).

The structure DRResolvedModelPackageLevelRam bundles: an integral, locally Noetherian scheme Y, proper and flat over \operatorname{Spec} O, together with a proper morphism \mathrm{toDR}\colon Y\to\mathfrak{X}\times_R\operatorname{Spec} O over \operatorname{Spec} O; regularity of all stalks at points lying outside the preimage of D(q), with Krull dimension at most 2 there; \mathrm{toDR} restricting to an isomorphism over the preimage of \mathfrak{X}'s smooth locus and over the preimage of D(q); a finite type node with widths \mathrm{width}(n)\ge1 and a bijection of node with the points of the crossing scheme \mathfrak{X}_{\kappa,0}\times_{\mathfrak{X}_\kappa}\mathfrak{X}_{\kappa,1}; a family comp of quasi-coherent ideal sheaves indexed by \mathrm{Fin}\,2\sqcup\coprod_n\mathrm{Fin}(\mathrm{width}(n)-1), each invertible (locally generated by a nonzerodivisor) with integral closed subscheme and support over q=0; designated generic points \eta_v whose stalks see exactly one component, and an exhaustion of codimension-one points over q=0 by the \eta_v; identifications of the two \mathrm{Fin}\,2-components after base change to \kappa with the level-N_0 Igusa fibre compatibly with \mathfrak{X}'s components, contraction of each exceptional component to its node, and its identification with a curve model with function field \kappa(t); named edge points, injectively indexed by (n,d), lying on consecutive chain positions chainPos, exhausting all pairwise intersections of components, and crossing transversally in the sense that the sum of the two ideals generates the maximal ideal; and an open set, smooth of relative dimension 1 over O, containing every non-edge point. The sole difference from DRResolvedModelPackageLevel is the field comp_prod, which here asserts that on every affine open the product of all component ideals is generated by \varpi rather than by q; accordingly ofUnramified reads an unramified package as a ramified one with \varpi=(q:O).

Relation to Mathlib

Mathlib has no notion of a (resolved) arithmetic model of a modular curve; this structure is the project's own, phrased with Mathlib's Scheme.IdealSheafData, stalks and germs, and the morphism classes IsProper, Flat, SmoothOfRelativeDimension. The invertibility predicate used for the components is the project's Scheme.IdealSheafData.IsInvertible (local generation by a nonzerodivisor on affine basic opens).

Where it is used

Regular models of X_0(N_0q) with the special fibre presented as a subdivided dual graph feed the computation of component groups of the Néron model of J_0(N_0q), which is where level lowering at q in the Frey–Serre–Ribet step is carried out. Allowing a uniformiser \varpi distinct from q covers the situation of a ramified base, where the reduced special fibre is cut out by \varpi and the chains of exceptional curves lengthen by the ramification index.

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. B. Edixhoven, Minimal resolution and stable reduction of X_0(N), Annales de l'Institut Fourier 40 (1990), 31–67
  3. Q. Liu, Algebraic Geometry and Arithmetic Curves, Oxford Graduate Texts in Mathematics 6, Oxford University Press, 2002, Chapter 10

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_DRModelPackageLevel
import Definitions.Def_ModularCurve_X0MqResolvedTable
import Definitions.Def_AlgebraicCurve_RelCartier
import Definitions.Def_ModularCurve_DRResolvedModelPackageLevel

set_option autoImplicit false
set_option maxHeartbeats 800000
set_option synthInstance.maxHeartbeats 400000

noncomputable section

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
open ModularCurve.IgusaScheme

namespace ModularCurve

attribute [local instance] DRModelPackageLevel.neZero_mul

namespace DRLevel

abbrev unifOn {O : Type} [CommRing O] {Y : Scheme.{0}} (toBase : Y ⟶ Spec (CommRingCat.of O)) (ϖ : O) (U : Y.affineOpens) : Γ(Y, U) :=
  (Y.presheaf.map (homOfLE le_top).op) (toBase.appTop ((Scheme.ΓSpecIso (CommRingCat.of O)).inv ϖ))

theorem unifOn_natCast {O : Type} [CommRing O] {Y : Scheme.{0}} (toBase : Y ⟶ Spec (CommRingCat.of O)) (n : ℕ)
    (U : Y.affineOpens) : unifOn toBase (n : O) U = (n : Γ(Y, U)) := by
  simp [unifOn, map_natCast]

end DRLevel

open DRLevel

structure DRResolvedModelPackageLevelRam (N₀ q : ℕ) [NeZero N₀] [Fact q.Prime] {hqN : ¬ q ∣ N₀} (𝔛 : DRModelPackageLevel N₀ q hqN)
    (O : Type) [CommRing O] (ρ : R q →+* O) (ϖ : O)
    (κ : Type) [Field κ] [CharP κ q] [IsAlgClosed κ] [DecidableEq κ] (toκ : O →+* κ) where

  Y : Scheme.{0}
  toBase : Y ⟶ Spec (CommRingCat.of O)
  toDR : Y ⟶ XO (N₀ := N₀) ρ
  toDR_over : toDR ≫ pullback.snd _ _ = toBase
  [toDR_proper : IsProper toDR]
  [isProper : IsProper toBase]
  [flat : Flat toBase]
  [isIntegral : IsIntegral Y]
  [isLocallyNoetherian : IsLocallyNoetherian Y]

  regular : ∀ y : Y, y ∉ toBase ⁻¹ᵁ (PrimeSpectrum.basicOpen ((q : ℕ) : O) : (Spec (CommRingCat.of O)).Opens) →
    IsRegularLocalRing (Y.presheaf.stalk y)
  stalk_dim_le_two : ∀ y : Y, y ∉ toBase ⁻¹ᵁ (PrimeSpectrum.basicOpen ((q : ℕ) : O) : (Spec (CommRingCat.of O)).Opens) →
    ringKrullDim (Y.presheaf.stalk y) ≤ 2

  toDR_iso_smoothLocus : IsIso (toDR ∣_ (pullback.fst (DRLevel.toBase N₀ q) (Spec.map (CommRingCat.ofHom ρ)) ⁻¹ᵁ 𝔛.smoothLocus))
  toDR_iso_generic : IsIso (toDR ∣_ (pullback.snd (DRLevel.toBase N₀ q) (Spec.map (CommRingCat.ofHom ρ)) ⁻¹ᵁ
      (PrimeSpectrum.basicOpen ((q : ℕ) : O) : (Spec (CommRingCat.of O)).Opens)))

  node : Type
  [node_fintype : Fintype node]
  [node_deq : DecidableEq node]
  width : node → ℕ
  one_le_width : ∀ n, 1 ≤ width n

  nodeEquiv : node ≃ ↥(pullback (𝔛.comp κ (toκ.comp ρ) 0) (𝔛.comp κ (toκ.comp ρ) 1))
  comp : X0MqComponents width → Y.IdealSheafData
  comp_isInvertible : ∀ v, (comp v).IsInvertible
  comp_integral : ∀ v, IsIntegral (comp v).subscheme
  comp_support : ∀ v (y : Y), y ∈ (comp v).support →
    y ∉ toBase ⁻¹ᵁ (PrimeSpectrum.basicOpen ((q : ℕ) : O) : (Spec (CommRingCat.of O)).Opens)
  comp_prod : ∀ U : Y.affineOpens, (∏ v, comp v).ideal U = Ideal.span {DRLevel.unifOn toBase ϖ U}
  η : X0MqComponents width → Y
  η_not_mem : ∀ v, η v ∉ toBase ⁻¹ᵁ (PrimeSpectrum.basicOpen ((q : ℕ) : O) : (Spec (CommRingCat.of O)).Opens)
  η_stalk : ∀ v, ∃ (U : Y.affineOpens) (hU : η v ∈ (U : Y.Opens)),
    Ideal.map (Y.presheaf.germ (U : Y.Opens) (η v) hU).hom ((comp v).ideal U) =
        IsLocalRing.maximalIdeal (Y.presheaf.stalk (η v)) ∧
      ∀ w, w ≠ v → Ideal.map (Y.presheaf.germ (U : Y.Opens) (η v) hU).hom ((comp w).ideal U) = ⊤
  codim : ∀ y : Y, y ∉ toBase ⁻¹ᵁ (PrimeSpectrum.basicOpen ((q : ℕ) : O) : (Spec (CommRingCat.of O)).Opens) →
    ringKrullDim (Y.presheaf.stalk y) ≤ 1 → ∃ v, y = η v

  strict_iso : ∀ i : Fin 2,
    ∃ e : pullback ((comp (Sum.inl i)).subschemeι ≫ toBase) (Spec.map (CommRingCat.ofHom toκ)) ⟶ fibre0 (N₀ := N₀) (toκ.comp ρ),
      IsIso e ∧ e ≫ pullback.snd _ _ = pullback.snd _ _ ∧
        e ≫ 𝔛.comp κ (toκ.comp ρ) i ≫ bcMap ρ toκ = pullback.fst _ _ ≫ (comp (Sum.inl i)).subschemeι ≫ toDR

  exc_image : ∀ (n : node) (i : Fin (width n - 1)), ∀ y ∈ (comp (Sum.inr ⟨n, i⟩)).support,
    toDR.base y = (pullback.fst (𝔛.comp κ (toκ.comp ρ) 0) (𝔛.comp κ (toκ.comp ρ) 1) ≫ 𝔛.comp κ (toκ.comp ρ) 0 ≫
      bcMap ρ toκ).base (nodeEquiv n)

  edgePt : (n : node) → Fin (width n) → Y
  edgePt_injective : Function.Injective (fun e : Σ n, Fin (width n) => edgePt e.1 e.2)
  edgePt_mem : ∀ (n : node) (d : Fin (width n)),
    edgePt n d ∈ ((comp (DRResolvedModelPackageLevel.chainPos width n d)).support : Set Y) ∩
      ((comp (DRResolvedModelPackageLevel.chainPos width n (d + 1))).support : Set Y)
  edgePt_over : ∀ (n : node) (d : Fin (width n)),
    toDR.base (edgePt n d) = (pullback.fst (𝔛.comp κ (toκ.comp ρ) 0) (𝔛.comp κ (toκ.comp ρ) 1) ≫ 𝔛.comp κ (toκ.comp ρ) 0 ≫
      bcMap ρ toκ).base (nodeEquiv n)
  edgePt_exhaust : ∀ v w, v ≠ w → ∀ y ∈ ((comp v).support : Set Y) ∩ ((comp w).support : Set Y),
    ∃ (n : node) (d : Fin (width n)), y = edgePt n d ∧
      ((v = DRResolvedModelPackageLevel.chainPos width n d ∧ w = DRResolvedModelPackageLevel.chainPos width n (d + 1)) ∨
       (w = DRResolvedModelPackageLevel.chainPos width n d ∧ v = DRResolvedModelPackageLevel.chainPos width n (d + 1)))
  edgePt_transversal : ∀ (n : node) (d : Fin (width n)), ∃ (U : Y.affineOpens) (hU : edgePt n d ∈ (U : Y.Opens)),
    Ideal.map (Y.presheaf.germ (U : Y.Opens) (edgePt n d) hU).hom
        ((comp (DRResolvedModelPackageLevel.chainPos width n d)).ideal U ⊔
          (comp (DRResolvedModelPackageLevel.chainPos width n (d + 1))).ideal U) =
      IsLocalRing.maximalIdeal (Y.presheaf.stalk (edgePt n d))

  exc_rational : ∀ (n : node) (i : Fin (width n - 1)),
    ∃ (M : AlgebraicCurve.CurveModel κ (RatFunc κ))
      (e : M.C ⟶ pullback ((comp (Sum.inr ⟨n, i⟩)).subschemeι ≫ toBase) (Spec.map (CommRingCat.ofHom toκ))),
      IsIso e ∧ e ≫ pullback.snd _ _ = M.toBase

  smoothOffEdges : Y.Opens
  [smoothOffEdges_smooth : SmoothOfRelativeDimension 1 (smoothOffEdges.ι ≫ toBase)]
  mem_smoothOffEdges : ∀ y : Y, (∀ (n : node) (d : Fin (width n)), y ≠ edgePt n d) → y ∈ smoothOffEdges

attribute [instance] DRResolvedModelPackageLevelRam.toDR_proper DRResolvedModelPackageLevelRam.isProper DRResolvedModelPackageLevelRam.flat
  DRResolvedModelPackageLevelRam.isIntegral DRResolvedModelPackageLevelRam.isLocallyNoetherian DRResolvedModelPackageLevelRam.node_fintype
  DRResolvedModelPackageLevelRam.node_deq DRResolvedModelPackageLevelRam.smoothOffEdges_smooth

def DRResolvedModelPackageLevelRam.ofUnramified {N₀ q : ℕ} [NeZero N₀] [Fact q.Prime] {hqN : ¬ q ∣ N₀} {𝔛 : DRModelPackageLevel N₀ q hqN}
    {O : Type} [CommRing O] {ρ : R q →+* O} {κ : Type} [Field κ] [CharP κ q] [IsAlgClosed κ] [DecidableEq κ] {toκ : O →+* κ}
    (𝔜 : DRResolvedModelPackageLevel N₀ q 𝔛 O ρ κ toκ) : DRResolvedModelPackageLevelRam N₀ q 𝔛 O ρ ((q : ℕ) : O) κ toκ :=
  { 𝔜 with comp_prod := fun U => (𝔜.comp_prod U).trans (by rw [DRLevel.unifOn_natCast]) }

end ModularCurve

end

Statements phrased using this module (0)

No statement module imports it directly (it is used through other definition modules or by proofs).