Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_NeronModelInfra_WeakNeronModel.lean

definition module

Index-one local extensions and families of models catching their points

Two notions are introduced. First, IsIndexOneExtension R R', for local rings R, R' with a local R-algebra structure on R': a two-field structure asserting that the ideal generated by the image of the maximal ideal of R is the maximal ideal of R', and that the induced extension of residue fields is formally smooth (Mathlib's Algebra.FormallySmooth), which is the way separability of a not necessarily algebraic residue extension is expressed. It is proved that R \to R is such an extension. Second, ModelFamily R K gK, for a commutative ring R, a field K with an R-algebra structure and a K-scheme g_K \colon A_K \to \operatorname{Spec} K: a family indexed by a type \iota of R-schemes \mathrm{str}\,i \colon X_i \to \operatorname{Spec} R, together with, for each i, a morphism chart i from the generic fibre X_i \times_{\operatorname{Spec} R} \operatorname{Spec} K (realised as pullback.snd (str i) (specGenericFibreInclusion R K)) to A_K commuting with the structure maps to \operatorname{Spec} K, carrying as a further field the assertion that each such chart is an open immersion.

The predicate ModelFamily.CatchesIndexOnePoints (for R local) says: for every discrete valuation ring R' that is a local R-algebra and an index-one extension of R, with fraction field K' made a K-algebra compatibly with R, every K'-point a of A_K over \operatorname{Spec} K arises, for some index i, as an R'-point x of X_i over \operatorname{Spec} R passed to generic fibres and then composed with chart i. The passage to generic fibres is the map pointGenericFibre, sending such an x to the K'-point of X_i \times_{\operatorname{Spec} R} \operatorname{Spec} K determined by \operatorname{Spec} K' \to \operatorname{Spec} R' followed by x and by \operatorname{Spec} K' \to \operatorname{Spec} K; its compositions with the two pullback projections are recorded, as is the commutativity of the square of \operatorname{Spec} maps used to define it. Finally two extreme cases: the one-member family \operatorname{Spec} R catches all index-one points of the identity on \operatorname{Spec} K, while for R a discrete valuation ring with fraction field K the empty family fails to catch them as soon as A_K has a K-point, so the predicate has content. No existence of models is asserted.

Relation to Mathlib

Mathlib has no notion of weak Néron model, of a family of models with charts, or of an extension of ramification index one; these are the project's own, built on Mathlib's schemes, pullbacks, local rings and Algebra.FormallySmooth.

Where it is used

These definitions form the vocabulary layer for Néron and weak Néron models over a discrete valuation ring, used in the reduction theory of the elliptic curves occurring in the Frey curve argument.

References

  1. S. Bosch, W. Lütkebohmert and M. Raynaud, Néron Models, Ergebnisse der Mathematik und ihrer Grenzgebiete 21, Springer, 1990, §§3.5–3.6
  2. A. Grothendieck and J. Dieudonné, Éléments de géométrie algébrique IV, première partie, Publ. Math. IHÉS 20 (1964), 0_IV 19.6.1

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_AlgebraicGeometry_NeronModelEndomorphismExtension

set_option autoImplicit false

noncomputable section

universe u

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry

namespace NeronModelInfra

structure IsIndexOneExtension (R R' : Type u) [CommRing R] [IsLocalRing R] [CommRing R'] [IsLocalRing R']
    [Algebra R R'] [IsLocalHom (algebraMap R R')] : Prop where

  map_maximalIdeal :
    Ideal.map (algebraMap R R') (IsLocalRing.maximalIdeal R) = IsLocalRing.maximalIdeal R'

  formallySmooth_residueField :
    Algebra.FormallySmooth (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField R')

theorem IsIndexOneExtension.refl (R : Type u) [CommRing R] [IsLocalRing R] :
    IsIndexOneExtension R R where
  map_maximalIdeal := by
    rw [Algebra.algebraMap_self, Ideal.map_id]
  formallySmooth_residueField := by
    have e : (IsLocalRing.ResidueField.instAlgebra :
        Algebra (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField R)) =
        Algebra.id (IsLocalRing.ResidueField R) := by
      apply Algebra.algebra_ext
      intro x
      obtain ⟨x, rfl⟩ := IsLocalRing.residue_surjective x
      rfl
    have h : @Algebra.FormallySmooth (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField R) _ _
        (Algebra.id (IsLocalRing.ResidueField R)) := inferInstance
    convert h

section PointGenericFibre

variable {R : Type u} [CommRing R] {K : Type u} [Field K] [Algebra R K]
variable {R' : Type u} [CommRing R'] [Algebra R R']
variable {K' : Type u} [CommRing K'] [Algebra R' K'] [Algebra R K'] [IsScalarTower R R' K']
  [Algebra K K'] [IsScalarTower R K K']

theorem specMap_algebraMap_comp_specMap_algebraMap (R K R' K' : Type u) [CommRing R] [Field K]
    [Algebra R K] [CommRing R'] [Algebra R R'] [CommRing K'] [Algebra R' K'] [Algebra R K']
    [IsScalarTower R R' K'] [Algebra K K'] [IsScalarTower R K K'] :
    Spec.map (CommRingCat.ofHom (algebraMap R' K')) ≫ Spec.map (CommRingCat.ofHom (algebraMap R R')) =
      Spec.map (CommRingCat.ofHom (algebraMap K K')) ≫ Spec.map (CommRingCat.ofHom (algebraMap R K)) := by
  rw [← Spec.map_comp, ← Spec.map_comp, ← CommRingCat.ofHom_comp, ← CommRingCat.ofHom_comp,
    ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]

variable {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of R)}

def pointGenericFibre (x : SchemeHomOver (Spec.map (CommRingCat.ofHom (algebraMap R R'))) f) :
    SchemeHomOver (Spec.map (CommRingCat.ofHom (algebraMap K K')))
      (pullback.snd f (specGenericFibreInclusion R K)) :=
  ⟨pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R' K')) ≫ x.1)
      (Spec.map (CommRingCat.ofHom (algebraMap K K')))
      (by rw [Category.assoc, x.2, specGenericFibreInclusion_eq,
            specMap_algebraMap_comp_specMap_algebraMap R K R' K']),
    pullback.lift_snd _ _ _⟩

@[simp]
theorem pointGenericFibre_coe_comp_fst
    (x : SchemeHomOver (Spec.map (CommRingCat.ofHom (algebraMap R R'))) f) :
    (pointGenericFibre (K := K) (K' := K') x).1 ≫ pullback.fst f (specGenericFibreInclusion R K) =
      Spec.map (CommRingCat.ofHom (algebraMap R' K')) ≫ x.1 :=
  pullback.lift_fst _ _ _

@[simp]
theorem pointGenericFibre_coe_comp_snd
    (x : SchemeHomOver (Spec.map (CommRingCat.ofHom (algebraMap R R'))) f) :
    (pointGenericFibre (K := K) (K' := K') x).1 ≫ pullback.snd f (specGenericFibreInclusion R K) =
      Spec.map (CommRingCat.ofHom (algebraMap K K')) :=
  pullback.lift_snd _ _ _

end PointGenericFibre

structure ModelFamily (R K : Type u) [CommRing R] [Field K] [Algebra R K]
    {AK : Scheme.{u}} (gK : AK ⟶ Spec (CommRingCat.of K)) where

  ι : Type u

  X : ι → Scheme.{u}

  str : ∀ i, X i ⟶ Spec (CommRingCat.of R)

  chart : ∀ i, SchemeHomOver (pullback.snd (str i) (specGenericFibreInclusion R K)) gK

  isOpenImmersion_chart : ∀ i, IsOpenImmersion (chart i).1

attribute [instance] ModelFamily.isOpenImmersion_chart

def ModelFamily.CatchesIndexOnePoints {R K : Type u} [CommRing R] [IsLocalRing R] [Field K] [Algebra R K]
    {AK : Scheme.{u}} {gK : AK ⟶ Spec (CommRingCat.of K)} (M : ModelFamily R K gK) : Prop :=
  ∀ (R' : Type u) [CommRing R'] [IsDomain R'] [IsDiscreteValuationRing R'] [Algebra R R']
    [IsLocalHom (algebraMap R R')]
    (K' : Type u) [Field K'] [Algebra R' K'] [IsFractionRing R' K'] [Algebra R K'] [IsScalarTower R R' K']
    [Algebra K K'] [IsScalarTower R K K'],
    IsIndexOneExtension R R' →
    ∀ a : SchemeHomOver (Spec.map (CommRingCat.ofHom (algebraMap K K'))) gK,
      ∃ (i : M.ι) (x : SchemeHomOver (Spec.map (CommRingCat.ofHom (algebraMap R R'))) (M.str i)),
        schemeHomOverComp (pointGenericFibre x) (M.chart i) = a

section Gates

variable (R K : Type u) [CommRing R] [IsLocalRing R] [Field K] [Algebra R K]

def ModelFamily.trivial : ModelFamily R K (𝟙 (Spec (CommRingCat.of K))) where
  ι := PUnit
  X := fun _ => Spec (CommRingCat.of R)
  str := fun _ => 𝟙 _
  chart := fun _ => ⟨pullback.snd (𝟙 _) (specGenericFibreInclusion R K), Category.comp_id _⟩
  isOpenImmersion_chart := fun _ => inferInstance

theorem gate_catchesIndexOnePoints_trivial : (ModelFamily.trivial R K).CatchesIndexOnePoints := by
  intro R' _ _ _ _ _ K' _ _ _ _ _ _ _ _ a
  refine ⟨PUnit.unit, ⟨Spec.map (CommRingCat.ofHom (algebraMap R R')), Category.comp_id _⟩, ?_⟩
  exact (subsingleton_schemeHomOver_of_isIso (Spec.map (CommRingCat.ofHom (algebraMap K K')))
    (𝟙 (Spec (CommRingCat.of K)))).allEq _ _

def ModelFamily.empty {AK : Scheme.{u}} (gK : AK ⟶ Spec (CommRingCat.of K)) : ModelFamily R K gK where
  ι := PEmpty
  X := fun i => i.elim
  str := fun i => i.elim
  chart := fun i => i.elim
  isOpenImmersion_chart := fun i => i.elim

theorem gate_not_catchesIndexOnePoints_empty [IsDomain R] [IsDiscreteValuationRing R] [IsFractionRing R K]
    {AK : Scheme.{u}} (gK : AK ⟶ Spec (CommRingCat.of K)) (a : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) gK) :
    ¬ (ModelFamily.empty R K gK).CatchesIndexOnePoints := by
  intro h
  have ha : Spec.map (CommRingCat.ofHom (algebraMap K K)) = 𝟙 (Spec (CommRingCat.of K)) := by
    rw [Algebra.algebraMap_self, CommRingCat.ofHom_id]; exact Spec.map_id _
  obtain ⟨i, -, -⟩ := h R K (IsIndexOneExtension.refl R) ⟨a.1, by rw [ha]; exact a.2⟩
  exact i.elim

end Gates

end NeronModelInfra

end

/--
info: 'NeronModelInfra.IsIndexOneExtension.refl' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms NeronModelInfra.IsIndexOneExtension.refl

/--
info: 'NeronModelInfra.gate_catchesIndexOnePoints_trivial' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms NeronModelInfra.gate_catchesIndexOnePoints_trivial

/--
info: 'NeronModelInfra.gate_not_catchesIndexOnePoints_empty' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms NeronModelInfra.gate_not_catchesIndexOnePoints_empty

Statements phrased using this module (31)