Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_DrinfeldCurve_LocalChart.lean

definition module

Local chart presentations for the Drinfeld form in two variables

Fix a prime q (a natural number with Fact q.Prime). For a commutative ring O, DrinfeldCurve.LocalChart.drinfeldForm q O is the element X_0X_1^{q}-X_0^{q}X_1 of the two-variable power series ring MvPowerSeries (Fin 2) O; it is the power-series analogue of the polynomial DrinfeldCurve.drinfeldPoly used in the imported construction of the Drinfeld curve, whose coordinate ring is the quotient by X_0X_1^{q}-X_0^{q}X_1-1.

For a commutative ring O and an element \varpi\in O, the structure ChartPresentation q O ϖ packages three power series f,u,v\in O[[X_0,X_1]] together with two proofs: that u and v are units of the power series ring, and that f-\bigl(X_0X_1^{q}-X_0^{q}X_1\bigr) lies in the (q+2)-nd power of the ideal generated by X_0 and X_1. Thus f is required only to agree with the Drinfeld form modulo terms of total degree at least q+2, with arbitrary coefficients in O; this is a congruence condition on a chosen presentation, not an isomorphism statement, and no hypothesis is imposed on O or \varpi beyond commutativity — in particular the parameter \varpi occurs in no field of the structure.

Given such a presentation pr, ChartPresentation.rel pr is the single power series \varpi^{q+1}v-fu (with \varpi^{q+1} entering as the constant series C(\varpi^{q+1})), and ChartPresentation.Ring pr is an abbreviation for the quotient O[[X_0,X_1]]/(\varpi^{q+1}v-fu), carrying only its ambient ring structure. Nothing is asserted about these objects here; they are vocabulary.

Relation to Mathlib

Mathlib supplies the ambient two-variable power series ring MvPowerSeries (Fin 2) O; the notion of a chart presentation and the associated relation and quotient ring are the project's own.

Where it is used

These definitions give the vocabulary for the local structure, over a base ring with distinguished element \varpi, of the equation \varpi^{q+1}v=fu with f congruent to the Drinfeld form; the intended application is the completed local ring at a supersingular point of a modular curve with full level-q structure, whose blow-up has exceptional part governed by the Drinfeld curve xy^{q}-x^{q}y=1 constructed in the imported coordinate-ring and function-field modules.

References

  1. N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, Annals of Mathematics Studies 108, Princeton University Press, 1985, §13.8
  2. I. I. Bouw and S. Wewers, Stable reduction of modular curves, in: Modular Curves and Abelian Varieties, Progress in Mathematics 224, Birkhäuser, 2004, 1–22
  3. J. Weinstein, Semistable models for modular curves of arbitrary level, Inventiones Mathematicae 205 (2016), 459–526

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib.RingTheory.MvPowerSeries.Basic ↗
import Mathlib.RingTheory.LocalRing.ResidueField.Basic ↗
import Mathlib.RingTheory.Valuation.ValuationSubring ↗
import Mathlib.FieldTheory.IsAlgClosed.Basic ↗
import Mathlib.RingTheory.DiscreteValuationRing.Basic ↗
import Definitions.Def_DrinfeldCurve_FunctionField

set_option autoImplicit false

noncomputable section

open MvPowerSeries IsLocalRing DrinfeldCurve

namespace DrinfeldCurve.LocalChart

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

def drinfeldForm (O : Type) [CommRing O] : MvPowerSeries (Fin 2) O :=
  X 0 * X 1 ^ q - X 0 ^ q * X 1

structure ChartPresentation (O : Type) [CommRing O] (ϖ : O) where
  f : MvPowerSeries (Fin 2) O
  u : MvPowerSeries (Fin 2) O
  v : MvPowerSeries (Fin 2) O
  isUnit_u : IsUnit u
  isUnit_v : IsUnit v
  f_sub_mem : f - drinfeldForm q O ∈ (Ideal.span {(X 0 : MvPowerSeries (Fin 2) O), X 1}) ^ (q + 2)

variable {q}

def ChartPresentation.rel {O : Type} [CommRing O] {ϖ : O} (pr : ChartPresentation q O ϖ) : MvPowerSeries (Fin 2) O :=
  C (ϖ ^ (q + 1)) * pr.v - pr.f * pr.u

abbrev ChartPresentation.Ring {O : Type} [CommRing O] {ϖ : O} (pr : ChartPresentation q O ϖ) : Type :=
  MvPowerSeries (Fin 2) O ⧸ Ideal.span {pr.rel}

end DrinfeldCurve.LocalChart

end

Statements phrased using this module (444)

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