Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_CanonicalDivisor.lean

definition module

Order of a Kähler differential at a place of a function field

Throughout, K \subseteq F are fields with F a K-algebra and v is a place of F over K in the sense of AlgebraicCurve.Place: a valuation subring of F containing the image of K, different from \top, whose ideals are principal, so that it is a discrete valuation ring and v carries the normalised order function v.ord on F with v.ord of a uniformizer equal to 1 and v.ord\,0 = 0. A uniformizer of v is fixed (by a choice of an irreducible element of the valuation ring) and used only internally; from it AlgebraicCurve.Place.dCoord is the Kähler differential d\pi_v \in \Omega[F\!\restriction\!K], the image of the chosen uniformizer under Mathlib's universal derivation. The class AlgebraicCurve.Place.DCoordGenerates is the single-field hypothesis that the F-submodule of \Omega[F\!\restriction\!K] spanned by \{d\pi_v\} is everything; it is thus a hypothesis on the chosen uniformizer, asserting that d\pi_v is a generator of the module of differentials, not a theorem proved here. Under it every \omega is of the form f\cdot d\pi_v, and differentialCoeff returns such an f (and 0 when no such f exists); when \Omega[F\!\restriction\!K] is nontrivial, d\pi_v \neq 0 and the coefficient is unique, so differentialCoeff is F-homogeneous, sends d\pi_v to 1 and 0 to 0.

Finally AlgebraicCurve.Place.ordDifferential is defined by \operatorname{ord}_v(\omega) := v.ord(\,\mathrm{differentialCoeff}\ \omega\,), an integer; since v.ord vanishes at 0, this convention assigns the value 0 rather than +\infty to the zero differential. Two basic properties are recorded: the order of d\pi_v itself is 0, and for c \neq 0 with \omega of nonzero coefficient, \operatorname{ord}_v(c\,\omega) = v.ord(c) + \operatorname{ord}_v(\omega).

Relation to Mathlib

The module of differentials is Mathlib's KaehlerDifferential \Omega[F\!\restriction\!K]; Mathlib has no notion of the order of a differential at a place of a function field, and DCoordGenerates and the coefficient and order functions are the project's own.

Where it is used

These notions supply the local order of a differential, hence the data needed to form canonical divisors and to study the Cartier operator and Hasse–Witt matrix of a modular curve in the project's treatment of divisors on curves.

References

  1. H. Stichtenoth, Algebraic Function Fields and Codes, Springer, 2nd edition, 2009, Chapter IV
  2. 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_CanonicalDivisor.lean

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_AlgebraicCurve_DivisorClassGroup

set_option autoImplicit false

open KaehlerDifferential

noncomputable section

namespace AlgebraicCurve

variable (K F : Type*) [Field K] [Field F] [Algebra K F]

namespace Place

variable {K F}
variable (v : Place K F)

private def uniformizer : F :=
  ((IsDiscreteValuationRing.exists_irreducible v.toValuationSubring).choose : F)

private theorem ord_uniformizer : v.ord v.uniformizer = 1 := by
  have hirr := (IsDiscreteValuationRing.exists_irreducible v.toValuationSubring).choose_spec
  simpa [uniformizer] using v.ord_coe_irreducible hirr

private theorem uniformizer_ne_zero : v.uniformizer ≠ 0 := by
  intro h
  simpa [h, v.ord_zero] using v.ord_uniformizer

def dCoord : Ω[F⁄K] := KaehlerDifferential.D K F v.uniformizer

class DCoordGenerates : Prop where
  span_eq_top : Submodule.span F {v.dCoord} = ⊤

theorem dCoord_ne_zero [v.DCoordGenerates] [Nontrivial Ω[F⁄K]] : v.dCoord ≠ 0 := by
  intro h0
  have htop := DCoordGenerates.span_eq_top (v := v)
  obtain ⟨x, hx⟩ := exists_ne (0 : Ω[F⁄K])
  have hx_mem : x ∈ Submodule.span F {v.dCoord} := htop ▸ Submodule.mem_top
  rw [h0, Submodule.span_zero_singleton] at hx_mem
  exact hx hx_mem

def differentialCoeff (ω : Ω[F⁄K]) : F :=
  letI := Classical.propDecidable
  if h : ∃ f : F, ω = f • v.dCoord then h.choose else 0

theorem exists_eq_smul_dCoord [v.DCoordGenerates] (ω : Ω[F⁄K]) :
    ∃ f : F, ω = f • v.dCoord := by
  have hω : ω ∈ (⊤ : Submodule F Ω[F⁄K]) := Submodule.mem_top
  rw [← DCoordGenerates.span_eq_top (v := v), Submodule.mem_span_singleton] at hω
  exact hω.imp fun _ hf => hf.symm

theorem differentialCoeff_smul_dCoord [v.DCoordGenerates] (ω : Ω[F⁄K]) :
    v.differentialCoeff ω • v.dCoord = ω := by
  rw [differentialCoeff, dif_pos (v.exists_eq_smul_dCoord ω)]
  exact (v.exists_eq_smul_dCoord ω).choose_spec.symm

theorem differentialCoeff_unique [v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
    {ω : Ω[F⁄K]} {f : F} (hf : ω = f • v.dCoord) : v.differentialCoeff ω = f := by
  have key : (v.differentialCoeff ω - f) • v.dCoord = 0 := by
    rw [sub_smul, v.differentialCoeff_smul_dCoord ω, hf, sub_self]
  rcases smul_eq_zero.mp key with h | h
  · exact sub_eq_zero.mp h
  · exact absurd h v.dCoord_ne_zero

@[simp]
theorem differentialCoeff_dCoord [v.DCoordGenerates] [Nontrivial Ω[F⁄K]] :
    v.differentialCoeff v.dCoord = 1 :=
  v.differentialCoeff_unique (one_smul F v.dCoord).symm

@[simp]
theorem differentialCoeff_zero [v.DCoordGenerates] [Nontrivial Ω[F⁄K]] :
    v.differentialCoeff (0 : Ω[F⁄K]) = 0 :=
  v.differentialCoeff_unique (zero_smul F v.dCoord).symm

theorem differentialCoeff_smul [v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
    (c : F) (ω : Ω[F⁄K]) :
    v.differentialCoeff (c • ω) = c * v.differentialCoeff ω :=
  v.differentialCoeff_unique
    (by rw [mul_smul, v.differentialCoeff_smul_dCoord])

def ordDifferential (ω : Ω[F⁄K]) : ℤ := v.ord (v.differentialCoeff ω)

theorem gate_ordDifferential_dCoord [v.DCoordGenerates] [Nontrivial Ω[F⁄K]] :
    v.ordDifferential v.dCoord = 0 := by
  rw [ordDifferential, v.differentialCoeff_dCoord, v.ord_one]

theorem ordDifferential_smul [v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
    {c : F} (hc : c ≠ 0) {ω : Ω[F⁄K]} (hω : v.differentialCoeff ω ≠ 0) :
    v.ordDifferential (c • ω) = v.ord c + v.ordDifferential ω := by
  rw [ordDifferential, ordDifferential, v.differentialCoeff_smul, v.ord_mul hc hω]

end Place

end AlgebraicCurve

end

Statements phrased using this module (56)