Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_DRModelPackage.lean

definition module

Integral two-chart model of and its property package

Fix a prime p. DRModel p is the scheme \mathfrak X = AlgebraicCurve.TwoChartIntegralModel over \mathbf Z attached to the field F = modularFunctionFieldFull p, the subfield of \mathbf Q-Laurent series generated by the q-expansions j(q^d) for the divisors d of p, and to the element j = IgusaScheme.jFull p of F: the pushout of \operatorname{Spec} of the integral closure of \mathbf Z[j] in F and \operatorname{Spec} of the integral closure of \mathbf Z[j^{-1}] in F, glued along \operatorname{Spec} of the integral closure of \mathbf Z[j,j^{-1}]. DRModel.toBase p is its structure morphism to \operatorname{Spec}\mathbf Z, and DRModel.pFibre p the base change along \mathbf Z \to \mathbf Z/(p). For a section \varepsilon of the structure morphism and a ring homomorphism a\colon\mathbf Z\to\kappa, DRModel.sectionFibre is the induced \kappa-point of the base change of \mathfrak X along a.

DRModelPackage p is a structure bundling data and properties of (\mathfrak X,\ \text{toBase}); it asserts nothing on its own. Its fields are: properness, flatness, integrality and affine-local integral closedness (normality); a CurveModel M_0 of F/\mathbf Q and a CurveModel M_\eta of modularFunctionFieldBar p over \overline{\mathbf Q}, each with an isomorphism onto the corresponding base change of \mathfrak X over the structure morphism, together with equivariance of the points-to-places bijection of M_\eta for the action arithmeticGalois of \operatorname{Gal}(\overline{\mathbf Q}/\mathbf Q), and compatibility of the valuation subrings of places of M_\eta and M_0 at points lying over the same point of \mathfrak X; two sections \varepsilon_\infty,\varepsilon_0 over \mathbf Z; an open smoothLocus, smooth of relative dimension 1 over \mathbf Z and containing every open on which the structure morphism is smooth, containing the images of both sections, smoothness after inverting p; reducedness of the fibre at p; for every algebraically closed \kappa of characteristic p, a curve model of \kappa(T) over \kappa with two closed immersions into the fibre over \kappa, jointly surjective, with distinct images, reduced scheme-theoretic intersection whose cardinality equals that of the supersingular j-set ssJSet p κ, and receiving the reductions of \varepsilon_\infty and \varepsilon_0 respectively; an involutive automorphism w of \mathfrak X over \mathbf Z exchanging the two sections; and finiteness of each chart algebra over \mathbf Z[X], where X acts as j, respectively j^{-1}. A helper lemma supplies NeZero p.

Relation to Mathlib

Mathlib has no modular curves or integral models of them; TwoChartIntegralModel, CurveModel, modularFunctionFieldFull, ssJSet and this package are the project's own. The package is phrased entirely in terms of Mathlib's morphism classes (IsProper, Flat, Smooth, SmoothOfRelativeDimension, IsClosedImmersion), pushouts and pullbacks of schemes, and Mathlib's function-field and valuation-subring API.

Where it is used

The package is the interface through which the arithmetic geometry of X_0(p) over \mathbf Z — its generic fibre, its two rational components crossing at the supersingular points in the fibre at p, the two cusp sections and the Atkin–Lehner involution — is fed into the construction of J_0(p) and of the identity component of its Néron model at p, which is what the level-lowering step of the Fermat argument consumes.

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. N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, Annals of Mathematics Studies 108, Princeton University Press, 1985
  3. J.-I. Igusa, Kroneckerian model of fields of elliptic modular functions, American Journal of Mathematics 81 (1959), 561–577

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_X0
import Definitions.Def_ModularCurve_IgusaScheme
import Definitions.Def_AlgebraicCurve_TwoChartIntegralModel
import Definitions.Def_AlgebraicCurve_CurveModel
import Definitions.Def_ModularCurve_GeometricBaseChange
import Definitions.Def_ModularCurve_ArithmeticGalois
import Definitions.Def_AlgebraicGeometry_NeronModelPropertyBundleCarrier
import Definitions.Def_ModularCurve_SupersingularModuli
import Definitions.Def_AlgebraicGeometry_TwoAffineOpenCover

set_option autoImplicit false

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra ModularCurve AlgebraicCurve IsLocalRing

noncomputable section

namespace ModularCurve

variable (p : ℕ) [Fact p.Prime]

theorem DRModelPackage.neZero_of_fact_prime : NeZero p := ⟨(Fact.out : p.Prime).ne_zero⟩

attribute [local instance] DRModelPackage.neZero_of_fact_prime

abbrev DRModel : Scheme.{0} :=
  AlgebraicCurve.TwoChartIntegralModel ℤ ↥(modularFunctionFieldFull p) (IgusaScheme.jFull p)

abbrev DRModel.toBase : DRModel p ⟶ Spec (CommRingCat.of ℤ) :=
  AlgebraicCurve.TwoChartIntegralModel.toBase ℤ ↥(modularFunctionFieldFull p) (IgusaScheme.jFull p)

abbrev DRModel.pFibre : Scheme.{0} :=
  AlgebraicCurve.TwoChartIntegralModel.fibre ℤ ↥(modularFunctionFieldFull p) (IgusaScheme.jFull p) (Ideal.span {(p : ℤ)})

variable {p} in

def DRModel.sectionFibre (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of ℤ))) (DRModel.toBase p))
    {κ : Type} [CommRing κ] (a : ℤ →+* κ) :
    Spec (CommRingCat.of κ) ⟶ pullback (DRModel.toBase p) (Spec.map (CommRingCat.ofHom a)) :=
  pullback.lift (Spec.map (CommRingCat.ofHom a) ≫ ε.1) (𝟙 _)
    (by rw [Category.assoc, ε.2, Category.comp_id, Category.id_comp])

structure DRModelPackage where

  isProper : IsProper (DRModel.toBase p)
  flat : Flat (DRModel.toBase p)
  isIntegral : IsIntegral (DRModel p)

  normal : ∀ U : (DRModel p).Opens, IsAffineOpen U → IsIntegrallyClosed Γ(DRModel p, U)

  M₀ : CurveModel ℚ ↥(modularFunctionFieldFull p)
  e₀ : M₀.C ⟶ pullback (DRModel.toBase p) (Spec.map (CommRingCat.ofHom (algebraMap ℤ ℚ)))
  [e₀_iso : IsIso e₀]
  he₀ : e₀ ≫ pullback.snd _ _ = M₀.toBase
  Mη : CurveModel (AlgebraicClosure ℚ) (modularFunctionFieldBar p)
  eη : Mη.C ⟶ pullback (DRModel.toBase p) (Spec.map (CommRingCat.ofHom (algebraMap ℤ (AlgebraicClosure ℚ))))
  [eη_iso : IsIso eη]
  heη : eη ≫ pullback.snd _ _ = Mη.toBase
  hgal : ∀ (g : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ)
      (x x' : {q : Spec (CommRingCat.of (AlgebraicClosure ℚ)) ⟶ Mη.C // q ≫ Mη.toBase = 𝟙 _}),
      x'.1 ≫ eη ≫ pullback.fst _ _ =
        Spec.map (CommRingCat.ofHom (g : AlgebraicClosure ℚ →+* AlgebraicClosure ℚ)) ≫ x.1 ≫ eη ≫ pullback.fst _ _ →
      Mη.pointEquivPlace x' = arithmeticGalois (L := AlgebraicClosure ℚ) (modularFunctionFieldFull p) g • Mη.pointEquivPlace x
  hcompat : ∀ (x : {q : Spec (CommRingCat.of (AlgebraicClosure ℚ)) ⟶ Mη.C // q ≫ Mη.toBase = 𝟙 _})
        (y : Spec (CommRingCat.of (AlgebraicClosure ℚ)) ⟶
          pullback (DRModel.toBase p) (Spec.map (CommRingCat.ofHom (algebraMap ℤ ℚ))))
        (x₀ : closedPoints M₀.C),
      y ≫ pullback.fst (DRModel.toBase p) _ = x.1 ≫ eη ≫ pullback.fst (DRModel.toBase p) _ →
      (y ≫ inv e₀).base (IsLocalRing.closedPoint (AlgebraicClosure ℚ)) = x₀.1 →
      ((Mη.pointEquivPlace x).toValuationSubring.toSubring.comap
          ((baseChangeEquiv (AlgebraicClosure ℚ) (modularFunctionFieldFull p)).toAlgHom.toRingHom.comp
            (Algebra.TensorProduct.includeRight (R := ℚ) (A := AlgebraicClosure ℚ)
              (B := ↥(modularFunctionFieldFull p))).toRingHom) =
        (M₀.placeOfPoint x₀).toValuationSubring.toSubring)

  εinf : SchemeHomOver (𝟙 (Spec (CommRingCat.of ℤ))) (DRModel.toBase p)
  εzero : SchemeHomOver (𝟙 (Spec (CommRingCat.of ℤ))) (DRModel.toBase p)

  smoothLocus : (DRModel p).Opens

  [smoothLocus_relDim : SmoothOfRelativeDimension 1 (smoothLocus.ι ≫ DRModel.toBase p)]
  smoothLocus_maximal : ∀ U : (DRModel p).Opens, Smooth (U.ι ≫ DRModel.toBase p) → U ≤ smoothLocus
  εinf_mem_smoothLocus : Set.range εinf.1.base ⊆ (smoothLocus : Set (DRModel p))
  εzero_mem_smoothLocus : Set.range εzero.1.base ⊆ (smoothLocus : Set (DRModel p))
  smooth_away : Smooth (pullback.snd (DRModel.toBase p)
      (Spec.map (CommRingCat.ofHom (algebraMap ℤ (Localization.Away (p : ℤ))))))

  pFibre_reduced : IsReduced (DRModel.pFibre p)

  ratModel : ∀ (κ : Type) [Field κ] [CharP κ p] [IsAlgClosed κ], CurveModel κ (RatFunc κ)

  compInf : ∀ (κ : Type) [Field κ] [CharP κ p] [IsAlgClosed κ],
      (ratModel κ).C ⟶ pullback (DRModel.toBase p) (Spec.map (CommRingCat.ofHom (algebraMap ℤ κ)))
  compZero : ∀ (κ : Type) [Field κ] [CharP κ p] [IsAlgClosed κ],
      (ratModel κ).C ⟶ pullback (DRModel.toBase p) (Spec.map (CommRingCat.ofHom (algebraMap ℤ κ)))
  compInf_over : ∀ (κ : Type) [Field κ] [CharP κ p] [IsAlgClosed κ], compInf κ ≫ pullback.snd _ _ = (ratModel κ).toBase
  compZero_over : ∀ (κ : Type) [Field κ] [CharP κ p] [IsAlgClosed κ], compZero κ ≫ pullback.snd _ _ = (ratModel κ).toBase
  compInf_isClosedImmersion : ∀ (κ : Type) [Field κ] [CharP κ p] [IsAlgClosed κ], IsClosedImmersion (compInf κ)
  compZero_isClosedImmersion : ∀ (κ : Type) [Field κ] [CharP κ p] [IsAlgClosed κ], IsClosedImmersion (compZero κ)
  comp_jointly_surjective : ∀ (κ : Type) [Field κ] [CharP κ p] [IsAlgClosed κ]
      (x : ↥(pullback (DRModel.toBase p) (Spec.map (CommRingCat.ofHom (algebraMap ℤ κ))))),
      x ∈ Set.range (compInf κ).base ∨ x ∈ Set.range (compZero κ).base

  range_compInf_ne : ∀ (κ : Type) [Field κ] [CharP κ p] [IsAlgClosed κ],
      Set.range (compInf κ).base ≠ Set.range (compZero κ).base

  crossing_reduced : ∀ (κ : Type) [Field κ] [CharP κ p] [IsAlgClosed κ], IsReduced (pullback (compInf κ) (compZero κ))

  crossing_card : ∀ (κ : Type) [Field κ] [CharP κ p] [IsAlgClosed κ] [DecidableEq κ],
      Nat.card ↥(pullback (compInf κ) (compZero κ)) = Nat.card ↥(ssJSet p κ)

  εinf_mem_compInf : ∀ (κ : Type) [Field κ] [CharP κ p] [IsAlgClosed κ],
      Set.range (DRModel.sectionFibre εinf (algebraMap ℤ κ)).base ⊆ Set.range (compInf κ).base
  εzero_mem_compZero : ∀ (κ : Type) [Field κ] [CharP κ p] [IsAlgClosed κ],
      Set.range (DRModel.sectionFibre εzero (algebraMap ℤ κ)).base ⊆ Set.range (compZero κ).base

  w : DRModel p ≅ DRModel p
  w_over : w.hom ≫ DRModel.toBase p = DRModel.toBase p
  w_invol : w.hom ≫ w.hom = 𝟙 _

  w_sections : εinf.1 ≫ w.hom = εzero.1

  chartFin_finite : letI := (AlgebraicCurve.TwoChartIntegralModel.polynomialToChartFin ℤ ↥(modularFunctionFieldFull p)
      (IgusaScheme.jFull p)).toRingHom.toAlgebra
    Module.Finite (Polynomial ℤ) ↥(AlgebraicCurve.TwoChartIntegralModel.chartAlgFin ℤ ↥(modularFunctionFieldFull p) (IgusaScheme.jFull p))
  chartInf_finite : letI := (AlgebraicCurve.TwoChartIntegralModel.polynomialToChartInf ℤ ↥(modularFunctionFieldFull p)
      (IgusaScheme.jFull p)).toRingHom.toAlgebra
    Module.Finite (Polynomial ℤ) ↥(AlgebraicCurve.TwoChartIntegralModel.chartAlgInf ℤ ↥(modularFunctionFieldFull p) (IgusaScheme.jFull p))

attribute [instance] DRModelPackage.e₀_iso DRModelPackage.eη_iso DRModelPackage.smoothLocus_relDim

end ModularCurve

end

Statements phrased using this module (109)