Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_CanonicalDivisorUniformizer.lean

definition module

Chosen uniformizer at a place and its order

The setting is a field extension F/K of fields and a place v : \mathrm{Place}\ K\ F, i.e. (in the project's sense) a valuation subring \mathcal{O}_v \subseteq F containing \mathrm{algebraMap}\ K\ F of all of K, distinct from F itself, and a principal ideal ring; such a ring is then a discrete valuation ring, v.\mathrm{ord} is the associated normalised additive valuation on F (minus the logarithm of the \mathfrak{m}_v-adic valuation, with the convention v.\mathrm{ord}\,0 = 0), and v.\mathrm{dCoord} \in \Omega[F\,\vert\,K] is the Kähler differential of a uniformizer at v.

AlgebraicCurve.Place.uniformizer makes this choice available as a public definition: it is the element of F obtained by coercing the irreducible element of \mathcal{O}_v whose existence is given by the discrete valuation ring structure on \mathcal{O}_v. Thus it is a chosen generator of the maximal ideal, canonical only up to a unit. Three facts accompany it. ord_uniformizer states v.\mathrm{ord}(\pi_v) = 1, so the chosen element does have order exactly one at v; it follows from the computation of \mathrm{ord} on the image of an irreducible element of \mathcal{O}_v. uniformizer_ne_zero states \pi_v \neq 0 in F, obtained from the previous statement together with v.\mathrm{ord}\,0 = 0. Finally dCoord_eq identifies the differential used for the canonical-divisor formalism with the differential of this element: v.\mathrm{dCoord} = D_{K/F}(\pi_v) in the module of Kähler differentials \Omega[F\,\vert\,K], where D is Mathlib's universal derivation. The point of the module is therefore to expose, under a stable name and with its basic properties, the same chosen irreducible element that is used privately in the definition of dCoord, so that the differential coefficient and order-of-differential constructions can be computed against an explicit local parameter.

Relation to Mathlib

The notion of Place of F/K as a valuation subring containing K, proper and principal, together with its ord, is the project's own; the existence of an irreducible element and the module of Kähler differentials \Omega[F\,\vert\,K] with its universal derivation KaehlerDifferential.D are taken from Mathlib.

Where it is used

These declarations serve the divisor-theoretic treatment of curves, in particular of modular curves, where orders of functions and of differentials at a place are computed against a local parameter; they underlie the definitions of the differential coefficient, the order of a differential and hence of the canonical divisor.

References

  1. H. Stichtenoth, Algebraic Function Fields and Codes, Springer, 1993
  2. J.-P. Serre, Local Fields, Graduate Texts in Mathematics 67, Springer, 1979

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_CanonicalDivisor

set_option autoImplicit false

open KaehlerDifferential

noncomputable section

namespace AlgebraicCurve

variable {K F : Type*} [Field K] [Field F] [Algebra K F]

namespace Place

variable (v : Place K F)

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

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

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

theorem dCoord_eq : v.dCoord = KaehlerDifferential.D K F v.uniformizer := rfl

end Place

end AlgebraicCurve

end

Statements phrased using this module (32)