Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_NodeLocalizedPlaces.lean

definition module

Node-localised integer rings and node coordinates

Fix a prime q, a level N\ge 1, a valuation subring A of \overline{\mathbb Q}, a field k of characteristic q with a ring map \mathrm{red}\colon A\to k, modular polynomial data for q with its Kronecker congruence, integrality data for the two Hecke embeddings, a place specialisation P and a prolongation tuple R over P; R supplies two regular prolongations R_1,R_2 of A to the geometric level-Nq function field \bar F=\mathtt{modularFunctionFieldBar}(Nq) together with residue homomorphisms \mathrm{res}_1,\mathrm{res}_2 into the level-N fibre field \mathtt{modularFunctionFieldC}\,k\,N, and P supplies the reduction map V\mapsto P.\mathrm{reduceFst}(V) from places of \bar F to places of the fibre field. For a place w of the fibre field, nodeIntegers R w is the subring of \bar F consisting of the f lying in the integers of R_1, in the integers of R_2, and in the valuation subring of every place V of \bar F with P.\mathrm{reduceFst}(V)=w; accompanying lemmas record the defining equivalence, the three projections, and that \mathrm{ord}_V f\ge 0 for all such V. The two residue maps restrict to ring homomorphisms nodeResidue₁ w, nodeResidue₂ w from this ring to the fibre field. For an intermediate field K of \overline{\mathbb Q}/\mathbb Q, nodeIntegersOver K w is the subring of those f whose underlying Laurent series lies in \mathtt{NodeLocalized.fieldOver}(Nq)\,K, the subfield of \mathrm{LaurentSeries}(\overline{\mathbb Q}) generated by the constants from K and the two q-expansions j and j_{Nq}; it is contained in nodeIntegers w, constants from A always lie in the latter, and nodeConst K w is the resulting homomorphism from A\cap K into it. Finally, for perfect k, NodeCoordinates R K w is a structure with two elements x,y of nodeIntegersOver K w subject to the four conditions \mathrm{res}_1(x)=0, \mathrm{ord}_{\varphi\cdot w}(\mathrm{res}_2(x))=1, \mathrm{res}_2(y)=0, \mathrm{ord}_w(\mathrm{res}_1(y))=1, where \varphi=\mathtt{arithFrobC}\,q\,k\,N. No node equation relating x and y is part of the datum. The closing lemmas state that both residues of xy vanish and that \mathrm{res}_2(x) and \mathrm{res}_1(y) are non-zero.

Relation to Mathlib

Mathlib has no counterpart for these rings; they are built as Mathlib Subrings of the project's geometric modular function field, using the project's notions of place, regular prolongation and place specialisation.

Where it is used

These rings play the role of the local rings at the nodes of the special fibre at q of the modular curve of level Nq — two copies of the level-N fibre glued along a place w and its Frobenius translate \varphi\cdot w — but are defined purely valuation-theoretically, as intersections of valuation rings, with no model chosen. They are the local input for the description of the semistable reduction at q of the level-Nq Jacobian that underlies the level-lowering step.

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. K. A. Ribet, On modular representations of \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) arising from modular forms, Inventiones Mathematicae 100 (1990), 431–476

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

Imports

Imported by

Declarations

Source

import Definitions.Def_ModularCurve_ProlongationTuple
import Definitions.Def_ModularCurve_NodeDescent
set_option synthInstance.maxHeartbeats 400000
set_option maxHeartbeats 800000
set_option autoImplicit false

noncomputable section

open AlgebraicCurve IsLocalRing ModularCurve

namespace ModularCurve.PlaceSpecialization

variable {q : ℕ} [Fact q.Prime] {A : ValuationSubring (AlgebraicClosure ℚ)} {N : ℕ} [NeZero N]
  {k : Type*} [Field k] [CharP k q] {red : A →+* k}
  {data : ModularPolynomialData q} {hKr : KroneckerCongruence q data}
  {hα : HeckeAlphaBarIntegral (AlgebraicClosure ℚ) N q}
  {hβ : HeckeBetaBarIntegral (AlgebraicClosure ℚ) N q}
  {P : PlaceSpecialization A q N data hKr k red hα hβ}

namespace ProlongationTuple

variable (R : ProlongationTuple P)

def nodeIntegers (w : Place k (modularFunctionFieldC k N)) : Subring ↥(modularFunctionFieldBar (N * q)) where
  carrier := {f | f ∈ R.R₁.integers ∧ f ∈ R.R₂.integers ∧
    ∀ V : Place (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar (N * q)), P.reduceFst V = w →
      f ∈ V.toValuationSubring}
  zero_mem' := ⟨zero_mem _, zero_mem _, fun V _ => zero_mem _⟩
  one_mem' := ⟨one_mem _, one_mem _, fun V _ => one_mem _⟩
  add_mem' := by
    rintro f g ⟨hf₁, hf₂, hf⟩ ⟨hg₁, hg₂, hg⟩
    exact ⟨add_mem hf₁ hg₁, add_mem hf₂ hg₂, fun V hV => add_mem (hf V hV) (hg V hV)⟩
  neg_mem' := by
    rintro f ⟨hf₁, hf₂, hf⟩
    exact ⟨neg_mem hf₁, neg_mem hf₂, fun V hV => neg_mem (hf V hV)⟩
  mul_mem' := by
    rintro f g ⟨hf₁, hf₂, hf⟩ ⟨hg₁, hg₂, hg⟩
    exact ⟨mul_mem hf₁ hg₁, mul_mem hf₂ hg₂, fun V hV => mul_mem (hf V hV) (hg V hV)⟩

theorem mem_nodeIntegers_iff (w : Place k (modularFunctionFieldC k N)) (f : ↥(modularFunctionFieldBar (N * q))) :
    f ∈ R.nodeIntegers w ↔ f ∈ R.R₁.integers ∧ f ∈ R.R₂.integers ∧
      ∀ V : Place (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar (N * q)), P.reduceFst V = w →
        f ∈ V.toValuationSubring :=
  Iff.rfl

theorem mem_integersFst_of_mem_nodeIntegers {w : Place k (modularFunctionFieldC k N)}
    {f : ↥(modularFunctionFieldBar (N * q))} (hf : f ∈ R.nodeIntegers w) : f ∈ R.R₁.integers :=
  hf.1

theorem mem_integersSnd_of_mem_nodeIntegers {w : Place k (modularFunctionFieldC k N)}
    {f : ↥(modularFunctionFieldBar (N * q))} (hf : f ∈ R.nodeIntegers w) : f ∈ R.R₂.integers :=
  hf.2.1

theorem mem_toValuationSubring_of_mem_nodeIntegers {w : Place k (modularFunctionFieldC k N)}
    {f : ↥(modularFunctionFieldBar (N * q))} (hf : f ∈ R.nodeIntegers w)
    {V : Place (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar (N * q))} (hV : P.reduceFst V = w) :
    f ∈ V.toValuationSubring :=
  hf.2.2 V hV

theorem ord_nonneg_of_mem_nodeIntegers {w : Place k (modularFunctionFieldC k N)}
    {f : ↥(modularFunctionFieldBar (N * q))} (hf : f ∈ R.nodeIntegers w)
    {V : Place (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar (N * q))} (hV : P.reduceFst V = w) :
    0 ≤ V.ord f :=
  V.ord_nonneg_of_mem (hf.2.2 V hV)

def nodeResidue₁ (w : Place k (modularFunctionFieldC k N)) :
    ↥(R.nodeIntegers w) →+* ↥(modularFunctionFieldC k N) where
  toFun f := R.residue₁ ⟨f, f.2.1⟩
  map_one' := by
    rw [show (⟨((1 : ↥(R.nodeIntegers w)) : ↥(modularFunctionFieldBar (N * q))), (1 : ↥(R.nodeIntegers w)).2.1⟩
      : ↥(R.R₁.integers)) = 1 from rfl, map_one]
  map_mul' f g := by
    rw [show (⟨((f * g : ↥(R.nodeIntegers w)) : ↥(modularFunctionFieldBar (N * q))), (f * g).2.1⟩
      : ↥(R.R₁.integers)) = ⟨f, f.2.1⟩ * ⟨g, g.2.1⟩ from rfl, map_mul]
  map_zero' := by
    rw [show (⟨((0 : ↥(R.nodeIntegers w)) : ↥(modularFunctionFieldBar (N * q))), (0 : ↥(R.nodeIntegers w)).2.1⟩
      : ↥(R.R₁.integers)) = 0 from rfl, map_zero]
  map_add' f g := by
    rw [show (⟨((f + g : ↥(R.nodeIntegers w)) : ↥(modularFunctionFieldBar (N * q))), (f + g).2.1⟩
      : ↥(R.R₁.integers)) = ⟨f, f.2.1⟩ + ⟨g, g.2.1⟩ from rfl, map_add]

def nodeResidue₂ (w : Place k (modularFunctionFieldC k N)) :
    ↥(R.nodeIntegers w) →+* ↥(modularFunctionFieldC k N) where
  toFun f := R.residue₂ ⟨f, f.2.2.1⟩
  map_one' := by
    rw [show (⟨((1 : ↥(R.nodeIntegers w)) : ↥(modularFunctionFieldBar (N * q))), (1 : ↥(R.nodeIntegers w)).2.2.1⟩
      : ↥(R.R₂.integers)) = 1 from rfl, map_one]
  map_mul' f g := by
    rw [show (⟨((f * g : ↥(R.nodeIntegers w)) : ↥(modularFunctionFieldBar (N * q))), (f * g).2.2.1⟩
      : ↥(R.R₂.integers)) = ⟨f, f.2.2.1⟩ * ⟨g, g.2.2.1⟩ from rfl, map_mul]
  map_zero' := by
    rw [show (⟨((0 : ↥(R.nodeIntegers w)) : ↥(modularFunctionFieldBar (N * q))), (0 : ↥(R.nodeIntegers w)).2.2.1⟩
      : ↥(R.R₂.integers)) = 0 from rfl, map_zero]
  map_add' f g := by
    rw [show (⟨((f + g : ↥(R.nodeIntegers w)) : ↥(modularFunctionFieldBar (N * q))), (f + g).2.2.1⟩
      : ↥(R.R₂.integers)) = ⟨f, f.2.2.1⟩ + ⟨g, g.2.2.1⟩ from rfl, map_add]

@[simp] theorem nodeResidue₁_apply (w : Place k (modularFunctionFieldC k N)) (f : ↥(R.nodeIntegers w)) :
    R.nodeResidue₁ w f = R.residue₁ ⟨f, f.2.1⟩ := rfl

@[simp] theorem nodeResidue₂_apply (w : Place k (modularFunctionFieldC k N)) (f : ↥(R.nodeIntegers w)) :
    R.nodeResidue₂ w f = R.residue₂ ⟨f, f.2.2.1⟩ := rfl

def nodeIntegersOver (K : IntermediateField ℚ (AlgebraicClosure ℚ)) (w : Place k (modularFunctionFieldC k N)) :
    Subring ↥(modularFunctionFieldBar (N * q)) where
  carrier := {f | f ∈ R.nodeIntegers w ∧
    ((f : ↥(modularFunctionFieldBar (N * q))) : LaurentSeries (AlgebraicClosure ℚ))
      ∈ NodeLocalized.fieldOver (N * q) K}
  zero_mem' := ⟨zero_mem _, by rw [ZeroMemClass.coe_zero]; exact zero_mem _⟩
  one_mem' := ⟨one_mem _, by rw [OneMemClass.coe_one]; exact one_mem _⟩
  add_mem' := by
    rintro f g ⟨hf, hfK⟩ ⟨hg, hgK⟩
    exact ⟨add_mem hf hg, by rw [AddMemClass.coe_add]; exact add_mem hfK hgK⟩
  neg_mem' := by
    rintro f ⟨hf, hfK⟩
    exact ⟨neg_mem hf, by rw [NegMemClass.coe_neg]; exact neg_mem hfK⟩
  mul_mem' := by
    rintro f g ⟨hf, hfK⟩ ⟨hg, hgK⟩
    exact ⟨mul_mem hf hg, by rw [MulMemClass.coe_mul]; exact mul_mem hfK hgK⟩

theorem mem_nodeIntegersOver_iff (K : IntermediateField ℚ (AlgebraicClosure ℚ))
    (w : Place k (modularFunctionFieldC k N)) (f : ↥(modularFunctionFieldBar (N * q))) :
    f ∈ R.nodeIntegersOver K w ↔ f ∈ R.nodeIntegers w ∧
      ((f : ↥(modularFunctionFieldBar (N * q))) : LaurentSeries (AlgebraicClosure ℚ))
        ∈ NodeLocalized.fieldOver (N * q) K :=
  Iff.rfl

theorem nodeIntegersOver_le (K : IntermediateField ℚ (AlgebraicClosure ℚ)) (w : Place k (modularFunctionFieldC k N)) :
    R.nodeIntegersOver K w ≤ R.nodeIntegers w :=
  fun _ hf => hf.1

theorem algebraMap_mem_nodeIntegers (w : Place k (modularFunctionFieldC k N)) (c : A) :
    algebraMap (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar (N * q)) (c : AlgebraicClosure ℚ) ∈ R.nodeIntegers w :=
  ⟨(R.R₁.algebraMap_mem_iff (c : AlgebraicClosure ℚ)).mpr c.2, (R.R₂.algebraMap_mem_iff (c : AlgebraicClosure ℚ)).mpr c.2,
    fun V _ => V.algebraMap_mem' _⟩

def nodeConst (K : IntermediateField ℚ (AlgebraicClosure ℚ)) (w : Place k (modularFunctionFieldC k N)) :
    ↥(NodeLocalized.coeffSubring A K) →+* ↥(R.nodeIntegersOver K w) where
  toFun c :=
    ⟨algebraMap (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar (N * q)) (c : AlgebraicClosure ℚ),
      R.algebraMap_mem_nodeIntegers w ⟨(c : AlgebraicClosure ℚ), c.2.1⟩,
      by
        have hc : ((algebraMap (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar (N * q)) (c : AlgebraicClosure ℚ)
              : ↥(modularFunctionFieldBar (N * q))) : LaurentSeries (AlgebraicClosure ℚ))
            = CharPReduction.constSeries K.toSubalgebra.toSubring ⟨(c : AlgebraicClosure ℚ), c.2.2⟩ := rfl
        rw [hc]
        exact Subfield.subset_closure (Or.inl ⟨_, rfl⟩)⟩
  map_one' := Subtype.ext (by
    show algebraMap (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar (N * q)) ((1 : ↥(NodeLocalized.coeffSubring A K)) : AlgebraicClosure ℚ) = _
    rw [OneMemClass.coe_one, map_one]; rfl)
  map_mul' c d := Subtype.ext (by
    show algebraMap (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar (N * q)) ((c * d : ↥(NodeLocalized.coeffSubring A K)) : AlgebraicClosure ℚ) = _
    rw [MulMemClass.coe_mul, map_mul]; rfl)
  map_zero' := Subtype.ext (by
    show algebraMap (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar (N * q)) ((0 : ↥(NodeLocalized.coeffSubring A K)) : AlgebraicClosure ℚ) = _
    rw [ZeroMemClass.coe_zero, map_zero]; rfl)
  map_add' c d := Subtype.ext (by
    show algebraMap (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar (N * q)) ((c + d : ↥(NodeLocalized.coeffSubring A K)) : AlgebraicClosure ℚ) = _
    rw [AddMemClass.coe_add, map_add]; rfl)

@[simp] theorem coe_nodeConst (K : IntermediateField ℚ (AlgebraicClosure ℚ)) (w : Place k (modularFunctionFieldC k N))
    (c : ↥(NodeLocalized.coeffSubring A K)) :
    ((R.nodeConst K w c : ↥(R.nodeIntegersOver K w)) : ↥(modularFunctionFieldBar (N * q)))
      = algebraMap (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar (N * q)) (c : AlgebraicClosure ℚ) := rfl

structure NodeCoordinates [PerfectField k] (K : IntermediateField ℚ (AlgebraicClosure ℚ))
    (w : Place k (modularFunctionFieldC k N)) where

  x : ↥(R.nodeIntegersOver K w)

  y : ↥(R.nodeIntegersOver K w)
  x_fst : R.nodeResidue₁ w ⟨x, x.2.1⟩ = 0
  x_snd : (arithFrobC q k N • w).ord (R.nodeResidue₂ w ⟨x, x.2.1⟩) = 1
  y_snd : R.nodeResidue₂ w ⟨y, y.2.1⟩ = 0
  y_fst : w.ord (R.nodeResidue₁ w ⟨y, y.2.1⟩) = 1

namespace NodeCoordinates

variable {R} [PerfectField k] {K : IntermediateField ℚ (AlgebraicClosure ℚ)}
  {w : Place k (modularFunctionFieldC k N)} (c : R.NodeCoordinates K w)

theorem nodeResidue₁_x_mul_y :
    R.nodeResidue₁ w (⟨c.x, c.x.2.1⟩ * ⟨c.y, c.y.2.1⟩) = 0 := by
  rw [map_mul, c.x_fst, zero_mul]

theorem nodeResidue₂_x_mul_y :
    R.nodeResidue₂ w (⟨c.x, c.x.2.1⟩ * ⟨c.y, c.y.2.1⟩) = 0 := by
  rw [map_mul, c.y_snd, mul_zero]

theorem nodeResidue₂_x_ne_zero : R.nodeResidue₂ w ⟨c.x, c.x.2.1⟩ ≠ 0 := by
  intro h
  have h1 := c.x_snd
  rw [h, Place.ord_zero] at h1
  exact zero_ne_one h1

theorem nodeResidue₁_y_ne_zero : R.nodeResidue₁ w ⟨c.y, c.y.2.1⟩ ≠ 0 := by
  intro h
  have h1 := c.y_fst
  rw [h, Place.ord_zero] at h1
  exact zero_ne_one h1

end NodeCoordinates

end ProlongationTuple

end ModularCurve.PlaceSpecialization

end

Statements phrased using this module (153)

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