Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_UVCrossingGaussOrder.lean

definition module

Gauss orders on the crossing model

Throughout, W is a commutative ring, and the crossing model \mathrm{UVCrossingModel}\ W\ \pi is the quotient of W[[U,V]] = MvPowerSeries (Fin 2) W by the ideal generated by X_0X_1 - \pi, with quotient map mk π.

Two embeddings of one-variable series are defined coefficientwise: inU a is the two-variable series whose coefficient at a multi-index d is the d_0-th coefficient of a when d_1 = 0 and 0 otherwise, i.e. a(U); symmetrically inV b is b(V). The lemmas coeff_inU and coeff_inV record these coefficient formulas.

The weight function annulusWeight e t d is the natural number d_0 t + d_1 (e - t), the subtraction being truncated subtraction in \mathbb{N}. Given a function v : W \to \mathbb{N}\cup\{\infty\} (the intended input being an additive valuation) and natural numbers e, t, the order of a representative is \mathrm{repGaussOrder}\ v\ e\ t\ F \;=\; \inf_{d \in \mathbb{N}^2} \bigl( v(\mathrm{coeff}_d F) + d_0 t + d_1 (e-t) \bigr), an infimum in \mathbb{N}\cup\{\infty\} over all multi-indices. The order of an element x of the crossing model is then the supremum of \mathrm{repGaussOrder}\ v\ e\ t\ F over all F \in W[[U,V]] with \mathrm{mk}\ \pi\ F = x: \mathrm{gaussOrder}\ v\ \pi\ e\ t\ x \;=\; \sup \{\mathrm{repGaussOrder}\ v\ e\ t\ F : \mathrm{mk}\ \pi\ F = x\}, so that it is defined through presentations of x rather than intrinsically. No hypotheses beyond commutativity of W are imposed on v, \pi, e or t.

The remaining declarations are the order-theoretic interface: repGaussOrder_le (the infimum is bounded by each term), le_repGaussOrder_iff (a bound n \le \mathrm{repGaussOrder} holds precisely when it holds coefficientwise), repGaussOrder_le_gaussOrder (each representative bounds the order of its class from below), and gaussOrder_le_iff (an upper bound for the order of a class is equivalent to the same bound for every representative).

Relation to Mathlib

Mathlib has no weighted order or Gauss-type valuation on such a crossing model; these are the project's own definitions, built on Mathlib's MvPowerSeries, PowerSeries and the complete lattice structure of \mathbb{N}\cup\{\infty\}.

Where it is used

The crossing model W[[U,V]]/(UV-\pi) is the shape of the completed local ring of a modular curve at a supersingular point, and the weights d_0 t + d_1(e-t) interpolate between the two branches, the parameter t playing the role of the valuation of U on the annulus cut out by UV = \pi. These definitions supply the vocabulary in which later statements about such local rings (slope behaviour in t, multiplicativity, normal forms) are phrased.

References

  1. S. Bosch, U. Güntzer and R. Remmert, Non-Archimedean Analysis, Grundlehren der mathematischen Wissenschaften 261, Springer, 1984

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_UVCrossingModel

set_option autoImplicit false

universe u

namespace ModularCurve.UVCrossingModel

noncomputable section

variable {W : Type u} [CommRing W]

def inU (a : PowerSeries W) : MvPowerSeries (Fin 2) W :=
  fun d => if d 1 = 0 then PowerSeries.coeff (d 0) a else 0

def inV (b : PowerSeries W) : MvPowerSeries (Fin 2) W :=
  fun d => if d 0 = 0 then PowerSeries.coeff (d 1) b else 0

theorem coeff_inU (a : PowerSeries W) (d : Fin 2 →₀ ℕ) :
    MvPowerSeries.coeff d (inU a) = if d 1 = 0 then PowerSeries.coeff (d 0) a else 0 := rfl

theorem coeff_inV (b : PowerSeries W) (d : Fin 2 →₀ ℕ) :
    MvPowerSeries.coeff d (inV b) = if d 0 = 0 then PowerSeries.coeff (d 1) b else 0 := rfl

def annulusWeight (e t : ℕ) (d : Fin 2 →₀ ℕ) : ℕ := d 0 * t + d 1 * (e - t)

def repGaussOrder (v : W → ℕ∞) (e t : ℕ) (F : MvPowerSeries (Fin 2) W) : ℕ∞ :=
  ⨅ d : Fin 2 →₀ ℕ, v (MvPowerSeries.coeff d F) + (annulusWeight e t d : ℕ∞)

def gaussOrder (v : W → ℕ∞) (π : W) (e t : ℕ) (x : UVCrossingModel W π) : ℕ∞ :=
  ⨆ F ∈ {F : MvPowerSeries (Fin 2) W | mk π F = x}, repGaussOrder v e t F

theorem repGaussOrder_le (v : W → ℕ∞) (e t : ℕ) (F : MvPowerSeries (Fin 2) W) (d : Fin 2 →₀ ℕ) :
    repGaussOrder v e t F ≤ v (MvPowerSeries.coeff d F) + (annulusWeight e t d : ℕ∞) :=
  iInf_le _ d

theorem le_repGaussOrder_iff (v : W → ℕ∞) (e t : ℕ) (F : MvPowerSeries (Fin 2) W) (n : ℕ∞) :
    n ≤ repGaussOrder v e t F ↔ ∀ d, n ≤ v (MvPowerSeries.coeff d F) + (annulusWeight e t d : ℕ∞) :=
  le_iInf_iff

theorem repGaussOrder_le_gaussOrder (v : W → ℕ∞) (π : W) (e t : ℕ) (F : MvPowerSeries (Fin 2) W) :
    repGaussOrder v e t F ≤ gaussOrder v π e t (mk π F) :=
  le_iSup₂ (f := fun G (_ : G ∈ {G : MvPowerSeries (Fin 2) W | mk π G = mk π F}) => repGaussOrder v e t G) F rfl

theorem gaussOrder_le_iff (v : W → ℕ∞) (π : W) (e t : ℕ) (x : UVCrossingModel W π) (n : ℕ∞) :
    gaussOrder v π e t x ≤ n ↔ ∀ F, mk π F = x → repGaussOrder v e t F ≤ n :=
  iSup₂_le_iff

end

end ModularCurve.UVCrossingModel

Statements phrased using this module (28)