Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AlgebraicCurve_PlaceEvaluation.lean

definition module

Evaluation at rational places and divisors; Weil reciprocity predicate

The setting is a field extension K \subseteq F (an algebra F over a field K, with F a field), with places, orders and divisors as in the divisor-class-group module: a Place K F is a valuation subring \mathcal O_v \subseteq F containing the image of K, different from F and with principal ideals (hence a discrete valuation ring), v.\mathrm{ord} is minus the logarithm of the associated adic valuation, and a divisor is a finitely supported function from places to \mathbb Z. Here a place v is declared IsRational when the structure map K \to \kappa(v) into the residue field of \mathcal O_v is surjective; since that map is automatically injective, this says \kappa(v) = K, i.e. \deg v = 1. The map residueInv is a chosen left inverse of K \to \kappa(v) (the Function.invFun, so it is a genuine inverse exactly when v is rational, and arbitrary elsewhere), and evalAt sends f \in F to residueInv of the residue class of f when f \in \mathcal O_v, and to 0 otherwise; thus f(v) \in K is the value of f at v when v is rational and f has no pole there, with the junk value 0 at poles. The accompanying lemmas record the two inversion identities, the defining equation of evalAt on \mathcal O_v, the fact that K \to \kappa(v) carries f(v) to the residue of f when v is rational, and 1(v) = 1.

For a divisor D, Divisor.evalFun f D is the finite product \prod_{v \in \mathrm{supp}\,D} f(v)^{D(v)} of integer powers in K; it is 1 on the zero divisor and equals f(v)^n on n \cdot v. Finally WeilReciprocity K F is a predicate on the pair (K,F), not a theorem: it asserts that for all nonzero f, g \in F and all divisors D_f, D_g with D_f(v) = \mathrm{ord}_v f and D_g(v) = \mathrm{ord}_v g at every place, such that at each place at least one of \mathrm{ord}_v f, \mathrm{ord}_v g vanishes and such that every place in the support of D_f or of D_g is rational, one has f(D_g) = g(D_f).

Relation to Mathlib

Built on Mathlib's ValuationSubring and IsLocalRing.ResidueField, with residueInv obtained from Function.invFun; the evaluation of a function at a place or at a divisor, and the Weil reciprocity statement, are the project's own, Mathlib having no such notions.

Where it is used

These definitions underlie the project's treatment of Weil reciprocity for function fields and, through it, the divisor-class description of the Weil pairing e_n(D_1,D_2) = f_1(D_2)/f_2(D_1) on elliptic curves, which feeds into the study of the mod n Galois representations used on the Frey-curve side of the argument.

References

  1. J. H. Silverman, The Arithmetic of Elliptic Curves, Graduate Texts in Mathematics 106, Springer, 1986
  2. H. Stichtenoth, Algebraic Function Fields and Codes, Universitext, Springer, 1993
  3. J.-P. Serre, Groupes algébriques et corps de classes, Hermann, 1959

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_AlgebraicCurve_DivisorClassGroup

set_option autoImplicit false

noncomputable section

open IsLocalRing

namespace AlgebraicCurve

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

namespace Place

variable (v : Place K F)

def IsRational : Prop := Function.Surjective (algebraMap K v.ResidueField)

theorem algebraMap_residueField_injective :
    Function.Injective (algebraMap K v.ResidueField) :=
  (algebraMap K v.ResidueField).injective

def residueInv : v.ResidueField → K :=
  Function.invFun (algebraMap K v.ResidueField)

theorem algebraMap_residueInv (hv : v.IsRational) (x : v.ResidueField) :
    algebraMap K v.ResidueField (v.residueInv x) = x :=
  Function.invFun_eq (hv x)

theorem residueInv_algebraMap (a : K) : v.residueInv (algebraMap K v.ResidueField a) = a :=
  Function.leftInverse_invFun v.algebraMap_residueField_injective a

open Classical in

def evalAt (f : F) : K :=
  if hf : f ∈ v.toValuationSubring then
    v.residueInv (residue v.toValuationSubring ⟨f, hf⟩)
  else 0

theorem evalAt_of_mem {f : F} (hf : f ∈ v.toValuationSubring) :
    v.evalAt f = v.residueInv (residue v.toValuationSubring ⟨f, hf⟩) :=
  dif_pos hf

theorem algebraMap_evalAt (hv : v.IsRational) {f : F} (hf : f ∈ v.toValuationSubring) :
    algebraMap K v.ResidueField (v.evalAt f)
      = residue v.toValuationSubring (⟨f, hf⟩ : v.toValuationSubring) := by
  rw [v.evalAt_of_mem hf]
  exact v.algebraMap_residueInv hv _

@[simp]
theorem evalAt_one : v.evalAt (1 : F) = 1 := by
  rw [v.evalAt_of_mem (one_mem _)]
  have h1 : (⟨(1 : F), one_mem _⟩ : v.toValuationSubring) = 1 := rfl
  rw [h1, map_one, ← map_one (algebraMap K v.ResidueField), v.residueInv_algebraMap]

end Place

namespace Divisor

def evalFun (f : F) (D : Divisor K F) : K :=
  D.prod fun v n => v.evalAt f ^ n

theorem evalFun_def (f : F) (D : Divisor K F) :
    evalFun f D = ∏ v ∈ D.support, v.evalAt f ^ D v := rfl

@[simp]
theorem evalFun_zero (f : F) : evalFun f (0 : Divisor K F) = 1 :=
  Finsupp.prod_zero_index

theorem evalFun_single (f : F) (v : Place K F) (n : ℤ) :
    evalFun f (Finsupp.single v n) = v.evalAt f ^ n :=
  Finsupp.prod_single_index (zpow_zero _)

end Divisor

variable (K F) in

def WeilReciprocity : Prop :=
  ∀ (f g : F) (Df Dg : Divisor K F), f ≠ 0 → g ≠ 0 →
    (∀ v : Place K F, Df v = v.ord f) → (∀ v : Place K F, Dg v = v.ord g) →
    (∀ v : Place K F, v.ord f = 0 ∨ v.ord g = 0) →
    (∀ v ∈ Df.support, Place.IsRational v) → (∀ v ∈ Dg.support, Place.IsRational v) →
    Divisor.evalFun f Dg = Divisor.evalFun g Df

end AlgebraicCurve

Statements phrased using this module (275)

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