Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AlgebraicCurve_WeilOfKaehler.lean

definition module

Traced Kähler residue functional on adèles; residue-theorem predicates

Throughout, F is a field extension of a field K equipped with a chosen family of canonical local residue data \mathrm{res}_v : F \to_{K} \kappa(v) at every place v (each K-linear, vanishing on the valuation subring, computing simple poles via the residue of \pi_v f, and killing \pi_v^{-(n+1)} for n \ge 1), with the standing assumptions that every nonzero \omega \in \Omega_{F/K} has a canonical divisor, that d\pi_v spans \Omega_{F/K} over F at each place, and that \Omega_{F/K} is nontrivial. For such \omega the local term is \mathrm{Tr}_{\kappa(v)/K}\bigl(\mathrm{res}_v(\alpha_v \cdot g_v(\omega))\bigr), where g_v(\omega) is the coefficient with \omega = g_v(\omega)\, d\pi_v. The first group of results shows this term vanishes at every place when \alpha lies in the bounded adèles \mathrm{adeleBdd} of \mathrm{canonicalDivisorOf}\ h\omega (the divisor v \mapsto \mathrm{ord}_v g_v(\omega)), that for \alpha bounded by D the terms are supported in the finite support of D - \mathrm{canonicalDivisorOf}\ h\omega, and hence that the support is finite for any adèle.

weilOfKaehler K F hω is then the element of \mathrm{Dual}_K(\mathbb{A}_F) sending an adèle \alpha to the finitely supported sum \sum_v \mathrm{Tr}_{\kappa(v)/K}(\mathrm{res}_v(\alpha_v g_v(\omega))); it vanishes on adèles bounded by the canonical divisor. Three further declarations are Prop-valued statements, asserting nothing by themselves: ResidueTheorem K F says that, given principal divisors, this functional kills every diagonal (global) adèle f \in F; WeilKaehlerAgree K F says it is nonzero, lies in \mathrm{omegaSpace}(\mathrm{canonicalDivisorOf}\ h\omega), and that \mathrm{canonicalDivisorOf}\ h\omega is maximal among divisors D with the functional in \mathrm{omegaSpace}\ D; ResiduePairingSurjective K F says that for divisors W, D and a nonzero \varphi \in \mathrm{omegaSpace}\ W whose bounding divisor W is maximal, the map \mathrm{residuePairing} from L(W-D) to \mathrm{omegaSpace}\ D, g \mapsto g\varphi, is surjective.

Relation to Mathlib

Mathlib supplies \Omega_{F/K} (KaehlerDifferential) and Module.Dual; the places, divisors, adèle spaces, local residues and Weil differentials used here are the project's own notions.

Where it is used

These definitions form the residue-theoretic bridge between Kähler differentials and Weil differentials for a function field over a not necessarily algebraically closed base, the per-place trace allowing places of arbitrary residue degree. They feed the adelic Riemann–Roch machinery applied to function fields of modular curves.

References

  1. H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Graduate Texts in Mathematics 254, Springer, 2009, Ch. I.5 and I.7
  2. J.-P. Serre, Groupes algébriques et corps de classes, Hermann, 1959, Ch. II

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_AlgebraicCurve_LocalResidue

set_option autoImplicit false

noncomputable section

open IsDedekindDomain WithZero Module IsLocalRing

namespace AlgebraicCurve

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

variable [HasCanonicalLocalResidueKStar K F]

theorem kaehlerResidueTerm_eq_zero_of_adeleBdd_canonical
    [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
    [Nontrivial Ω[F⁄K]] {ω : Ω[F⁄K]} (hω : ω ≠ 0)
    {α : Place K F → F} (hα : α ∈ adeleBdd (canonicalDivisorOf hω)) (v : Place K F) :
    kaehlerResidueTerm ω α v = 0 := by
  refine kaehlerResidueTerm_eq_zero_of_ord_nonneg ?_
  rcases eq_or_ne (α v) 0 with h0 | h0
  · exact Or.inl (by rw [h0, zero_mul])
  · refine Or.inr ?_
    have hg := v.differentialCoeff_ne_zero hω
    rw [v.ord_mul h0 hg]

    have hαv : -(canonicalDivisorOf hω v) ≤ v.ord (α v) := by
      have hval := hα v
      rw [v.adicValuation_eq_exp_neg_ord h0] at hval
      exact neg_le_of_neg_le (WithZero.exp_le_exp.mp hval)
    rw [canonicalDivisorOf_apply hω v, Place.ordDifferential] at hαv
    linarith

theorem kaehlerResidueTerm_support_subset
    [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
    [Nontrivial Ω[F⁄K]] {ω : Ω[F⁄K]} (hω : ω ≠ 0)
    {D : Divisor K F} {α : Place K F → F} (hα : α ∈ adeleBdd D) :
    Function.support (kaehlerResidueTerm ω α) ⊆ ↑(D - canonicalDivisorOf hω).support := by
  intro v hv

  rw [Finset.mem_coe, Finsupp.mem_support_iff, Finsupp.sub_apply, ne_eq, sub_eq_zero]
  intro hDω
  apply hv
  refine kaehlerResidueTerm_eq_zero_of_ord_nonneg ?_
  rcases eq_or_ne (α v) 0 with h0 | h0
  · exact Or.inl (by rw [h0, zero_mul])
  · refine Or.inr ?_
    have hg := v.differentialCoeff_ne_zero hω
    rw [v.ord_mul h0 hg]
    have hαv : -(D v) ≤ v.ord (α v) := by
      have hval := hα v
      rw [v.adicValuation_eq_exp_neg_ord h0] at hval
      exact neg_le_of_neg_le (WithZero.exp_le_exp.mp hval)
    rw [hDω, canonicalDivisorOf_apply hω v, Place.ordDifferential] at hαv
    linarith

theorem kaehlerResidueTerm_support_finite
    [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
    [Nontrivial Ω[F⁄K]] {ω : Ω[F⁄K]} (hω : ω ≠ 0)
    {D : Divisor K F} {α : Place K F → F} (hα : α ∈ adeleBdd D) :
    (Function.support (kaehlerResidueTerm ω α)).Finite :=
  Set.Finite.subset (Finset.finite_toSet _) (kaehlerResidueTerm_support_subset hω hα)

theorem kaehlerResidueTerm_support_finite_of_adeleSpace
    [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
    [Nontrivial Ω[F⁄K]] {ω : Ω[F⁄K]} (hω : ω ≠ 0)
    {α : Place K F → F} (hα : α ∈ adeleSpace K F) :
    (Function.support (kaehlerResidueTerm ω α)).Finite := by
  obtain ⟨D, hD⟩ := mem_adeleSpace_iff.mp hα
  exact kaehlerResidueTerm_support_finite hω hD

variable [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
  [Nontrivial Ω[F⁄K]]

variable (K F) in

def weilOfKaehler {ω : Ω[F⁄K]} (hω : ω ≠ 0) : Module.Dual K (adeleSpace K F) where
  toFun α := ∑ᶠ v, kaehlerResidueTerm ω (α : Place K F → F) v
  map_add' α β := by
    have hsupα := kaehlerResidueTerm_support_finite_of_adeleSpace hω α.2
    have hsupβ := kaehlerResidueTerm_support_finite_of_adeleSpace hω β.2
    rw [← finsum_add_distrib hsupα hsupβ]
    refine finsum_congr fun v => ?_
    unfold kaehlerResidueTerm
    rw [Submodule.coe_add, Pi.add_apply, add_mul, map_add, map_add]
  map_smul' c α := by
    simp only [RingHom.id_apply]
    rw [smul_finsum]
    refine finsum_congr fun v => ?_
    unfold kaehlerResidueTerm
    rw [Submodule.coe_smul, Pi.smul_apply, Algebra.smul_def, mul_assoc,
      ← Algebra.smul_def, map_smul, map_smul]

theorem weilOfKaehler_apply {ω : Ω[F⁄K]} (hω : ω ≠ 0) (α : adeleSpace K F) :
    weilOfKaehler K F hω α = ∑ᶠ v, kaehlerResidueTerm ω (α : Place K F → F) v := rfl

theorem weilOfKaehler_vanish_adeleBdd_canonical {ω : Ω[F⁄K]} (hω : ω ≠ 0)
    {α : adeleSpace K F} (hα : (α : Place K F → F) ∈ adeleBdd (canonicalDivisorOf hω)) :
    weilOfKaehler K F hω α = 0 := by
  rw [weilOfKaehler_apply]
  exact finsum_eq_zero_of_forall_eq_zero
    (kaehlerResidueTerm_eq_zero_of_adeleBdd_canonical hω hα)

variable (K F)

def ResidueTheorem : Prop :=
  ∀ [HasPrincipalDivisors K F] {ω : Ω[F⁄K]} (hω : ω ≠ 0) (f : F),
    weilOfKaehler K F hω ⟨diagonalHom K F f, diagonal_mem_adeleSpace f⟩ = 0

variable {K F}

variable (K F)

def WeilKaehlerAgree : Prop :=
  ∀ [HasPrincipalDivisors K F] {ω : Ω[F⁄K]} (hω : ω ≠ 0),
    weilOfKaehler K F hω ≠ 0 ∧
    weilOfKaehler K F hω ∈ omegaSpace (canonicalDivisorOf hω) ∧
    ∀ D : Divisor K F, weilOfKaehler K F hω ∈ omegaSpace D → D ≤ canonicalDivisorOf hω

variable {K F}

variable (K F)

def ResiduePairingSurjective : Prop :=
  ∀ [HasPrincipalDivisors K F] (W D : Divisor K F)
    {φ : Module.Dual K (adeleSpace K F)} (hφ : φ ∈ omegaSpace W) (_hφ0 : φ ≠ 0)
    (_hWmax : ∀ E : Divisor K F, φ ∈ omegaSpace E → E ≤ W),
    Function.Surjective (residuePairing K F W D hφ)

end AlgebraicCurve

end

Statements phrased using this module (38)