Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_JHChartSemicontinuity.lean

definition module

Cusp chart predicates for Γ_H-level first-component places

Throughout, p is prime, M is a level divisible by p, H \le (\mathbb{Z}/M)^\times, and A is a valuation subring of \overline{\mathbb{Q}} whose residue field \kappa is algebraically closed of characteristic p; P is a JHPlaceSpecialization (a specialisation map \mathrm{sp} from places of F_{M/p} = xHFunctionFieldBar (M/p) (infSubgroup p M H hpM) to places of the characteristic-p function field \mathrm{Fbar}, together with its divisor and Picard compatibilities), \theta an \overline{\mathbb{Q}}-algebra automorphism of F_M = xHFunctionFieldBar M H, and R a ProlongationDatum for P and \theta, carrying two regular prolongations R_1, R_2 of A to F_M with residues in \mathrm{Fbar}.

Four notions are introduced for a set S \subseteq F_M of chart functions. chartClosure S is the subring of F_M generated by S. chartLocalSetFst R v S, for a place v of \mathrm{Fbar} over \kappa, is the set of f \in F_M admitting g, u \in chartClosure S with u \in R_1, the R_1-residue of u not taking the value 0 at v, and f u = g; so it consists of the fractions g/u with v-unit denominator. ChartEtaleAt R α v S, for an \overline{\mathbb{Q}}-algebra map \alpha : F_{M/p} \to F_M, asserts the existence of z \in S and a monic m over F_{M/p} of degree p+1 such that: z lies in R_2 and some q-expansion coefficient of its R_2-residue in a degree n with p \nmid n is nonzero; \overline{\mathbb{Q}}(\alpha(F_{M/p}) \cup \{z\}) = F_M; z is a root of m pushed along \alpha; each \alpha(m_i) lies in chartClosure S; and whenever the derivative of m pushed along \alpha, evaluated at z, lies in R_1, its residue does not take the value 0 at v.

IsCuspChartFstAt R α hα v S (with hα the integrality of \alpha) is a structure whose fields record six conditions: S \subseteq R_1; the R_1-residues of elements of S lie in the valuation ring of v; each s \in S lies in the valuation ring of every place W of F_M with P.reduceFst α hα W = v, i.e. with \mathrm{sp} of the restriction of W along \alpha equal to v; any \varphi \in F_{M/p} with \alpha\varphi \in R_1 that is regular at every place u_0 of F_{M/p} with \mathrm{sp}(u_0) = v can be written \alpha\varphi = s/e with s, e \in S and e of nonzero residue at v; the étale clause above; and, for every place W of F_M satisfying IsZeroSide and lying over v, the existence of u \in S whose residue at v is nonzero and with \mathrm{ord}_W u > 0.

Relation to Mathlib

chartClosure is Mathlib's Subring.closure under a local name; the remaining notions are specific to this development, built on the project's own Place, RegularProlongation and specialisation data rather than on any Mathlib notion.

Where it is used

These chart predicates supply the local vocabulary in which the behaviour of functions on X_H(M) near an \infty-side cusp reading is compared with the first component of the reduction at a prime p exactly dividing M, feeding the semicontinuity statements used to describe the special fibre of the Jacobian at p and hence the level-lowering arguments.

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, esp. VII §2
  2. N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, Annals of Mathematics Studies 108, Princeton University Press, 1985, §8.11
  3. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_JHNeronObjectAtP
import Definitions.Def_ModularCurve_JHPlaceSpecialization

set_option autoImplicit false

open AlgebraicCurve IsLocalRing ModularCurve
open scoped MatrixGroups

namespace ModularCurve

variable {p M : ℕ} [Fact p.Prime] [NeZero M] {H : Subgroup (ZMod M)ˣ} {hpM : p ∣ M}
variable {A : ValuationSubring (AlgebraicClosure ℚ)}
variable [CharP (ResidueField ↥A) p] [IsAlgClosed (ResidueField ↥A)] [NeZero (M / p)]

namespace JHPlaceSpecialization

namespace ProlongationDatum

variable {P : JHPlaceSpecialization p M H hpM A}
variable {θ : ↥(xHFunctionFieldBar M H) ≃ₐ[AlgebraicClosure ℚ] ↥(xHFunctionFieldBar M H)}

noncomputable def chartClosure (S : Set ↥(xHFunctionFieldBar M H)) : Subring ↥(xHFunctionFieldBar M H) :=
  Subring.closure S

def chartLocalSetFst (R : ProlongationDatum P θ) (v : Place (ResidueField ↥A) (JHNeronObjectAtP.Fbar p M H hpM (ResidueField ↥A))) (S : Set ↥(xHFunctionFieldBar M H)) : Set ↥(xHFunctionFieldBar M H) :=
  {f | ∃ (g u : ↥(xHFunctionFieldBar M H)) (_ : g ∈ chartClosure S) (_ : u ∈ chartClosure S) (hu₁ : u ∈ R.R₁.integers),
      ¬ v.HasValue (R.R₁.residue ⟨u, hu₁⟩) (0 : (ResidueField ↥A)) ∧ f * u = g}

def ChartEtaleAt (R : ProlongationDatum P θ) (α : ↥(xHFunctionFieldBar (M / p) (ModularCurve.infSubgroup p M H hpM)) →ₐ[AlgebraicClosure ℚ] ↥(xHFunctionFieldBar M H)) (v : Place (ResidueField ↥A) (JHNeronObjectAtP.Fbar p M H hpM (ResidueField ↥A))) (S : Set ↥(xHFunctionFieldBar M H)) : Prop :=
  ∃ (z : ↥(xHFunctionFieldBar M H)) (m : Polynomial ↥(xHFunctionFieldBar (M / p) (ModularCurve.infSubgroup p M H hpM))),
    z ∈ S ∧
    (∃ hz₂ : z ∈ R.R₂.integers, ∃ n : ℤ, ¬ (p : ℤ) ∣ n ∧
      ((R.R₂.residue ⟨z, hz₂⟩ : (JHNeronObjectAtP.Fbar p M H hpM (ResidueField ↥A))) : LaurentSeries (ResidueField ↥A)).coeff n ≠ 0) ∧
    IntermediateField.adjoin (AlgebraicClosure ℚ) (Set.range α ∪ {z}) = ⊤ ∧
    m.Monic ∧ m.natDegree = p + 1 ∧
    (m.map α.toRingHom).eval z = 0 ∧
    (∀ i : ℕ, α (m.coeff i) ∈ Subring.closure S) ∧
    ∀ h : (Polynomial.derivative (m.map α.toRingHom)).eval z ∈ R.R₁.integers,
      ¬ v.HasValue (R.R₁.residue ⟨_, h⟩) (0 : (ResidueField ↥A))

structure IsCuspChartFstAt (R : ProlongationDatum P θ) (α : ↥(xHFunctionFieldBar (M / p) (ModularCurve.infSubgroup p M H hpM)) →ₐ[AlgebraicClosure ℚ] ↥(xHFunctionFieldBar M H)) (hα : α.IsIntegral)
    (v : Place (ResidueField ↥A) (JHNeronObjectAtP.Fbar p M H hpM (ResidueField ↥A))) (S : Set ↥(xHFunctionFieldBar M H)) : Prop where
  integral : ∀ s ∈ S, s ∈ R.R₁.integers
  regular : ∀ (s : ↥(xHFunctionFieldBar M H)) (hs : s ∈ S), (R.R₁.residue ⟨s, integral s hs⟩ : (JHNeronObjectAtP.Fbar p M H hpM (ResidueField ↥A))) ∈ v.toValuationSubring
  regularOver : ∀ s ∈ S, ∀ W : Place (AlgebraicClosure ℚ) ↥(xHFunctionFieldBar M H), P.reduceFst α hα W = v → s ∈ W.toValuationSubring
  nIncl : ∀ φ : ↥(xHFunctionFieldBar (M / p) (ModularCurve.infSubgroup p M H hpM)), α φ ∈ R.R₁.integers →
    (∀ u₀ : Place (AlgebraicClosure ℚ) ↥(xHFunctionFieldBar (M / p) (ModularCurve.infSubgroup p M H hpM)), P.sp u₀ = v → φ ∈ u₀.toValuationSubring) →
    ∃ (s : ↥(xHFunctionFieldBar M H)) (_ : s ∈ S) (e : ↥(xHFunctionFieldBar M H)) (he : e ∈ S),
      ¬ v.HasValue (R.R₁.residue ⟨e, integral e he⟩) (0 : (ResidueField ↥A)) ∧ α φ * e = s
  etale : R.ChartEtaleAt α v S
  separates : ∀ W : Place (AlgebraicClosure ℚ) ↥(xHFunctionFieldBar M H),
    IsZeroSide (p := p) (M := M) (H := H) (A := A) W → P.reduceFst α hα W = v →
      ∃ (u : ↥(xHFunctionFieldBar M H)) (hu : u ∈ S), ¬ v.HasValue (R.R₁.residue ⟨u, integral u hu⟩) (0 : (ResidueField ↥A)) ∧ 0 < W.ord u

end ProlongationDatum
end JHPlaceSpecialization
end ModularCurve

Statements phrased using this module (5)