Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AlgebraicCurve_Differentials.lean

definition module

Order of a differential at a place; regular differentials

The module works over a field extension K \subseteq F and takes the differentials of F/K to be Mathlib's module of Kähler differentials \Omega[F\!\mid\!K] with its universal derivation D = KaehlerDifferential.D K F; the places of F/K and their \mathbb{Z}-valued order function Place.ord (normalised so that an irreducible element of the valuation ring has order 1, and with \operatorname{ord} 0 = 0) are those of the divisor-class-group module. Four total, choice-based definitions are made. For a place v, Place.uniformizer_alt is a chosen t \in F with v.\mathrm{ord}\,t = 1 when such a t exists and 0 otherwise; ord_uniformizer_alt records that under the hypothesis that some element of order 1 exists, the chosen element has order 1. For t \in F and \omega \in \Omega[F\!\mid\!K], Place.diffCoeff t ω is a chosen g \in F with \omega = g \cdot D t when \omega lies in the F-line through D t, and 0 otherwise; diffCoeff_smul_D and diffCoeff_of_not_exists are the two defining cases. The order of \omega at v is then v.\mathrm{ordDiff}\,\omega = v.\mathrm{ord}\big(\mathrm{diffCoeff}\ v.\mathrm{uniformizer\_alt}\ \omega\big), a total \mathbb{Z}-valued quantity which takes the default value 0 in the degenerate cases; accordingly the existence of a uniformizer, the uniqueness of the coefficient g and the independence of ordDiff of the chosen uniformizer are assertions external to these definitions. A differential is regular, IsRegularDiff K F ω, when 0 \le v.\mathrm{ordDiff}\,\omega for every place v, and regularDiffs K F is defined as the K-span of the set of regular differentials, a K-submodule of \Omega[F\!\mid\!K] containing every regular differential. Finally, for a K-algebra map \varphi : F \to F' into a second field, pullbackDiff φ is the K-linear map \Omega[F\!\mid\!K] \to \Omega[F'\!\mid\!K] coming from KaehlerDifferential.map for the F-algebra structure on F' given by \varphi; it sends D_{F/K}x to D_{F'/K}(\varphi x).

Relation to Mathlib

The carrier and universal derivation are Mathlib's KaehlerDifferential module \Omega[F⁄K], and pullbackDiff is KaehlerDifferential.map for the algebra structure induced by a K-algebra map, restricted to K-scalars. The order of a differential at a place, the predicate of regularity and the submodule of regular differentials are the project's own notions, built on the places and order function of the project's divisor module.

Where it is used

These notions belong to the project's self-contained divisor and differential theory of function fields, alongside places, divisors, the degree map and the torsion of \mathrm{Pic}^0; the regular differentials and the order function at a place are the objects over which the genus-type statements used in the curve-theoretic part of the development are formulated.

References

  1. H. Stichtenoth, Algebraic Function Fields and Codes, Universitext, Springer, 1993
  2. R. Hartshorne, Algebraic Geometry, Graduate Texts in Mathematics 52, Springer, 1977, Ch. IV

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

Imports

Imported by

Declarations

Source

import Definitions.Def_AlgebraicCurve_DivisorClassGroup
import Mathlib.RingTheory.Kaehler.Basic ↗

noncomputable section

open KaehlerDifferential

namespace AlgebraicCurve

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

namespace Place

variable (v : Place K F)

open Classical in

def uniformizer_alt : F :=
  if h : ∃ t : F, v.ord t = 1 then h.choose else 0

theorem ord_uniformizer_alt (h : ∃ t : F, v.ord t = 1) : v.ord v.uniformizer_alt = 1 := by
  rw [uniformizer_alt, dif_pos h]
  exact h.choose_spec

open Classical in

def diffCoeff (t : F) (ω : Ω[F⁄K]) : F :=
  if h : ∃ g : F, ω = g • D K F t then h.choose else 0

theorem diffCoeff_smul_D {t : F} {ω : Ω[F⁄K]} (h : ∃ g : F, ω = g • D K F t) :
    diffCoeff t ω • D K F t = ω := by
  rw [diffCoeff, dif_pos h]
  exact h.choose_spec.symm

theorem diffCoeff_of_not_exists {t : F} {ω : Ω[F⁄K]} (h : ¬ ∃ g : F, ω = g • D K F t) :
    diffCoeff t ω = 0 := by
  rw [diffCoeff, dif_neg h]

def ordDiff (ω : Ω[F⁄K]) : ℤ :=
  v.ord (diffCoeff v.uniformizer_alt ω)

theorem ordDiff_def (ω : Ω[F⁄K]) : v.ordDiff ω = v.ord (diffCoeff v.uniformizer_alt ω) := rfl

end Place

variable (K F) in

def IsRegularDiff (ω : Ω[F⁄K]) : Prop :=
  ∀ v : Place K F, 0 ≤ v.ordDiff ω

theorem isRegularDiff_iff (ω : Ω[F⁄K]) :
    IsRegularDiff K F ω ↔ ∀ v : Place K F, 0 ≤ v.ordDiff ω := Iff.rfl

variable (K F) in

def regularDiffs : Submodule K Ω[F⁄K] :=
  Submodule.span K {ω : Ω[F⁄K] | IsRegularDiff K F ω}

theorem mem_regularDiffs_of_isRegularDiff {ω : Ω[F⁄K]} (h : IsRegularDiff K F ω) :
    ω ∈ regularDiffs K F :=
  Submodule.subset_span h

theorem regularDiffs_eq_span :
    regularDiffs K F = Submodule.span K {ω : Ω[F⁄K] | IsRegularDiff K F ω} := rfl

section Pullback

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

def pullbackDiff (φ : F →ₐ[K] F') : Ω[F⁄K] →ₗ[K] Ω[F'⁄K] :=
  letI : Algebra F F' := φ.toRingHom.toAlgebra
  haveI : IsScalarTower K F F' := IsScalarTower.of_algebraMap_eq fun k => (φ.commutes k).symm
  (KaehlerDifferential.map K K F F').restrictScalars K

theorem pullbackDiff_D (φ : F →ₐ[K] F') (x : F) :
    pullbackDiff φ (D K F x) = D K F' (φ x) := by
  letI : Algebra F F' := φ.toRingHom.toAlgebra
  haveI : IsScalarTower K F F' := IsScalarTower.of_algebraMap_eq fun k => (φ.commutes k).symm
  exact KaehlerDifferential.map_D K K F F' x

end Pullback

end AlgebraicCurve

end

Statements phrased using this module (64)