Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AlgebraicCurve_LocalResidue.lean

definition module

Local residues at places and Weil differentials of Kähler forms

Throughout, F/K is an extension of fields and a place v of F/K is the project's structure: a valuation subring \mathcal O_v \subsetneq F containing the image of K and a principal ideal ring (hence a discrete valuation ring), with normalised valuation \operatorname{ord}_v, residue field \kappa(v) and uniformiser \pi_v (a chosen irreducible of \mathcal O_v, so \operatorname{ord}_v \pi_v = 1). A LocalResidueData for v is a structure carrying a K-linear map \operatorname{res} : F \to \kappa(v) together with two properties as fields: \operatorname{res} f = 0 for f \in \mathcal O_v, and \operatorname{res} f = \overline{\pi_v f} whenever \pi_v f \in \mathcal O_v (the class of \pi_v f in \kappa(v)); informally, \operatorname{res} is the residue of f\,d\pi_v. CanonicalLocalResidueDataK extends this by the further field \operatorname{res}(\pi_v^{-(n+1)}) = 0 for all n \ge 1. Three classes package the availability of such data: HasLocalResidue and HasCanonicalLocalResidueK are propositions asserting that each place admits (respectively, canonical) data, while HasCanonicalLocalResidueKStar is data-valued, choosing CanonicalLocalResidueDataK at every place; the evident implications between them are instances. Under the last class, Place.localResidue is the chosen map, and lemmas record its vanishing on \mathcal O_v, the simple-pole formula, the vanishing on \pi_v^{-(n+1)} (n\ge 1), its vanishing whenever f = 0 or \operatorname{ord}_v f \ge 0, and \operatorname{res}_v(\pi_v^{-1}) = 1.

For a Kähler differential \omega \in \Omega[F\!\mid\!K] with local coefficient \partial_v\omega (the coefficient in \omega = \partial_v\omega \cdot d\pi_v), the local term is \operatorname{Tr}_{\kappa(v)/K}\operatorname{res}_v(\alpha_v\,\partial_v\omega), defined both for the chosen family (kaehlerResidueTerm) and for an explicitly given family R of canonical data (Place.kaehlerResidueTermK, kaehlerResidueTermKFam). Assuming a canonical divisor exists and every place satisfies DCoordGenerates, the support of v \mapsto term is contained in the support of D - \operatorname{div}(\omega) for \alpha \in adeleBdd D, hence finite for adèles, and weilOfKaehlerK is the resulting K-linear functional \alpha \mapsto \sum_v^{\mathrm f} (terms) on adeleSpace K F; it vanishes on adeleBdd (canonicalDivisorOf hω). Auxiliary declarations show \operatorname{ord}_v f \ge 0 forces f \in \mathcal O_v, that \partial_v\omega \neq 0 for \omega \neq 0 at a place with DCoordGenerates, and that \operatorname{Pi.single} v\, g lies in adeleBdd D (given v-adic bound) and in adeleSpace K F (adeleSingle). HasSeparableResidue asserts that \operatorname{Tr}_{\kappa(v)/K} \neq 0 as a K-linear map at every place. Finally ResidueTheoremK K F is the proposition that for every family of canonical data, assuming principal divisors exist, every nonzero \omega and every f \in F, the functional weilOfKaehlerK annihilates the diagonal adèle of f.

Relation to Mathlib

The local residue maps, the classes supplying them at all places, and the induced functional on the adèle space are the project's own notions; the ambient ingredients (valuation subrings and their residue fields, Kähler differentials \Omega[F\!\mid\!K], Algebra.trace, Module.Dual) are Mathlib's.

Where it is used

These residues provide the link between Kähler differentials of a function field and Weil differentials, i.e. functionals on the adèle space annihilating the diagonal and a bounded subspace; the residue theorem in this form is what supplies a nonzero Weil differential and hence the Riemann–Roch theorem for the curves occurring in the modular-curve part of the argument.

References

  1. J. Tate, Residues of differentials on curves, Annales scientifiques de l'École Normale Supérieure (4) 1 (1968), 149–159
  2. H. Stichtenoth, Algebraic Function Fields and Codes, Graduate Texts in Mathematics 254, Springer, 2nd edition, 2009

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_CanonicalDivisorUniformizer
import Definitions.Def_AlgebraicCurve_CanonicalDivisor
import Definitions.Def_AlgebraicCurve_AdelicIndex

set_option autoImplicit false

noncomputable section

open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential

namespace AlgebraicCurve

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

namespace Place

variable (v : Place K F)

structure LocalResidueData where

  res : F →ₗ[K] v.ResidueField

  res_of_mem : ∀ f : F, f ∈ v.toValuationSubring → res f = 0

  res_simplePole : ∀ (f : F) (hf : v.uniformizer * f ∈ v.toValuationSubring),
    res f = IsLocalRing.residue _ ⟨v.uniformizer * f, hf⟩

structure CanonicalLocalResidueDataK extends v.LocalResidueData where

  res_higherPoleMonomial : ∀ (n : ℕ), 1 ≤ n → res (v.uniformizer ^ (n + 1))⁻¹ = 0

end Place

variable (K F) in

class HasLocalResidue : Prop where
  exists_data : ∀ v : Place K F, Nonempty v.LocalResidueData

variable (K F) in

class HasCanonicalLocalResidueK : Prop where
  exists_data : ∀ v : Place K F, Nonempty v.CanonicalLocalResidueDataK

instance (priority := 100) instHasLocalResidue_of_hasCanonicalLocalResidueK
    [HasCanonicalLocalResidueK K F] : HasLocalResidue K F :=
  ⟨fun v => (HasCanonicalLocalResidueK.exists_data v).map (·.toLocalResidueData)⟩

variable (K F) in

class HasCanonicalLocalResidueKStar where

  dataKStar : ∀ v : Place K F, v.CanonicalLocalResidueDataK

instance (priority := 100) instHasCanonicalLocalResidueK_of_hasCanonicalLocalResidueKStar
    [HasCanonicalLocalResidueKStar K F] : HasCanonicalLocalResidueK K F :=
  ⟨fun v => ⟨HasCanonicalLocalResidueKStar.dataKStar v⟩⟩

namespace Place

variable (v : Place K F)

private theorem mem_of_ord_nonneg_localResidueAux {f : F} (hf : f ≠ 0) (h : 0 ≤ v.ord f) :
    f ∈ v.toValuationSubring := by
  obtain ⟨π, hπ⟩ := IsDiscreteValuationRing.exists_irreducible v.toValuationSubring
  obtain ⟨u, hu⟩ := v.exists_unit_mul_zpow hf hπ
  rw [hu, show v.ord f = (((v.ord f).toNat : ℕ) : ℤ) from (Int.toNat_of_nonneg h).symm,
    zpow_natCast]
  exact mul_mem (u : v.toValuationSubring).2 (pow_mem (π : v.toValuationSubring).2 _)

noncomputable def localResidue [HasCanonicalLocalResidueKStar K F] :
    F →ₗ[K] v.ResidueField :=
  (HasCanonicalLocalResidueKStar.dataKStar v).res

theorem localResidue_of_mem [HasCanonicalLocalResidueKStar K F] {f : F}
    (hf : f ∈ v.toValuationSubring) :
    v.localResidue f = 0 :=
  (HasCanonicalLocalResidueKStar.dataKStar v).res_of_mem f hf

theorem localResidue_simplePole [HasCanonicalLocalResidueKStar K F] (f : F)
    (hf : v.uniformizer * f ∈ v.toValuationSubring) :
    v.localResidue f = IsLocalRing.residue _ ⟨v.uniformizer * f, hf⟩ :=
  (HasCanonicalLocalResidueKStar.dataKStar v).res_simplePole f hf

theorem localResidue_higherPoleMonomial [HasCanonicalLocalResidueKStar K F]
    (n : ℕ) (hn : 1 ≤ n) :
    v.localResidue (v.uniformizer ^ (n + 1))⁻¹ = 0 :=
  (HasCanonicalLocalResidueKStar.dataKStar v).res_higherPoleMonomial n hn

theorem localResidue_eq_zero_of_ord_nonneg [HasCanonicalLocalResidueKStar K F] {f : F}
    (hf : f = 0 ∨ 0 ≤ v.ord f) : v.localResidue f = 0 := by
  rcases hf with rfl | hf
  · exact map_zero _
  · rcases eq_or_ne f 0 with rfl | hf0
    · exact map_zero _
    · exact v.localResidue_of_mem (v.mem_of_ord_nonneg_localResidueAux hf0 hf)

theorem gate_localResidue_uniformizer_inv [HasCanonicalLocalResidueKStar K F] :
    v.localResidue v.uniformizer⁻¹ = 1 := by
  have hmem : v.uniformizer * v.uniformizer⁻¹ ∈ v.toValuationSubring := by
    rw [mul_inv_cancel₀ v.uniformizer_ne_zero]; exact one_mem _
  rw [v.localResidue_simplePole _ hmem]
  have h1 : (⟨v.uniformizer * v.uniformizer⁻¹, hmem⟩ : v.toValuationSubring) = 1 :=
    Subtype.ext (mul_inv_cancel₀ v.uniformizer_ne_zero)
  rw [h1, map_one]

end Place

variable [HasCanonicalLocalResidueKStar K F]

def kaehlerResidueTerm (ω : Ω[F⁄K]) (α : Place K F → F) (v : Place K F) : K :=
  Algebra.trace K v.ResidueField (v.localResidue (α v * v.differentialCoeff ω))

theorem kaehlerResidueTerm_eq_zero_of_ord_nonneg {ω : Ω[F⁄K]} {α : Place K F → F}
    {v : Place K F} (h : α v * v.differentialCoeff ω = 0 ∨
      0 ≤ v.ord (α v * v.differentialCoeff ω)) :
    kaehlerResidueTerm ω α v = 0 := by
  unfold kaehlerResidueTerm
  rw [v.localResidue_eq_zero_of_ord_nonneg h, map_zero]

omit [HasCanonicalLocalResidueKStar K F] in

theorem Place.differentialCoeff_ne_zero (v : Place K F) [v.DCoordGenerates]
    {ω : Ω[F⁄K]} (hω : ω ≠ 0) : v.differentialCoeff ω ≠ 0 := fun h =>
  hω (by rw [← v.differentialCoeff_smul_dCoord ω, h, zero_smul])

namespace Place

theorem LocalResidueData.res_eq_zero_of_ord_nonneg {v : Place K F} (R : v.LocalResidueData)
    {f : F} (hf : f = 0 ∨ 0 ≤ v.ord f) : R.res f = 0 := by
  rcases hf with rfl | hf
  · exact map_zero _
  · rcases eq_or_ne f 0 with rfl | hf0
    · exact map_zero _
    · exact R.res_of_mem f (v.mem_of_ord_nonneg_localResidueAux hf0 hf)

theorem CanonicalLocalResidueDataK.res_eq_zero_of_ord_nonneg {v : Place K F}
    (R : v.CanonicalLocalResidueDataK) {f : F} (hf : f = 0 ∨ 0 ≤ v.ord f) : R.res f = 0 :=
  R.toLocalResidueData.res_eq_zero_of_ord_nonneg hf

end Place

section Single

open scoped Classical in

theorem single_mem_adeleBdd (v : Place K F) (g : F) (D : Divisor K F)
    (hg : v.adicValuation g ≤ WithZero.exp (D v)) :
    Pi.single v g ∈ adeleBdd D := by
  intro w
  rcases eq_or_ne w v with rfl | hw
  · simpa only [Pi.single_eq_same] using hg
  · rw [Pi.single_eq_of_ne hw, Valuation.map_zero]; exact zero_le'

open scoped Classical in

theorem single_mem_adeleSpace (v : Place K F) (g : F) :
    Pi.single v g ∈ adeleSpace K F := by
  rcases eq_or_ne g 0 with rfl | hg
  · simpa only [Pi.single_zero] using (adeleSpace K F).zero_mem
  · refine adeleBdd_le_adeleSpace
      (single_mem_adeleBdd v g (Finsupp.single v (-v.ord g)) ?_)
    rw [v.adicValuation_eq_exp_neg_ord hg, Finsupp.single_eq_same]

open scoped Classical in

def adeleSingle (v : Place K F) (g : F) : adeleSpace K F :=
  ⟨Pi.single v g, single_mem_adeleSpace v g⟩

open scoped Classical in
@[simp]
theorem adeleSingle_coe (v : Place K F) (g : F) :
    (adeleSingle v g : Place K F → F) = Pi.single v g := rfl

end Single

variable (K F) in

class HasSeparableResidue : Prop where
  trace_ne_zero : ∀ v : Place K F, (Algebra.trace K v.ResidueField : _ →ₗ[K] K) ≠ 0

section CanonicalKResidueTerm

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

def Place.kaehlerResidueTermK (v : Place K F) (R : v.CanonicalLocalResidueDataK)
    (ω : Ω[F⁄K]) (f : F) : K :=
  Algebra.trace K v.ResidueField (R.res (f * v.differentialCoeff ω))

def kaehlerResidueTermKFam (Rfam : ∀ v : Place K F, v.CanonicalLocalResidueDataK)
    (ω : Ω[F⁄K]) (α : Place K F → F) (v : Place K F) : K :=
  v.kaehlerResidueTermK (Rfam v) ω (α v)

@[simp]
theorem kaehlerResidueTermKFam_apply (Rfam : ∀ v : Place K F, v.CanonicalLocalResidueDataK)
    (ω : Ω[F⁄K]) (α : Place K F → F) (v : Place K F) :
    kaehlerResidueTermKFam Rfam ω α v
      = Algebra.trace K v.ResidueField ((Rfam v).res (α v * v.differentialCoeff ω)) := rfl

theorem kaehlerResidueTermKFam_eq_zero_of_ord_nonneg
    (Rfam : ∀ v : Place K F, v.CanonicalLocalResidueDataK) {ω : Ω[F⁄K]}
    {α : Place K F → F} {v : Place K F}
    (h : α v * v.differentialCoeff ω = 0 ∨ 0 ≤ v.ord (α v * v.differentialCoeff ω)) :
    kaehlerResidueTermKFam Rfam ω α v = 0 := by
  rw [kaehlerResidueTermKFam_apply, (Rfam v).res_eq_zero_of_ord_nonneg h, map_zero]

section SupportMachinery

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

theorem kaehlerResidueTermKFam_eq_zero_of_adeleBdd_canonical
    (Rfam : ∀ v : Place K F, v.CanonicalLocalResidueDataK) {ω : Ω[F⁄K]} (hω : ω ≠ 0)
    {α : Place K F → F} (hα : α ∈ adeleBdd (canonicalDivisorOf hω)) (v : Place K F) :
    kaehlerResidueTermKFam Rfam ω α v = 0 := by
  refine kaehlerResidueTermKFam_eq_zero_of_ord_nonneg Rfam ?_
  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 kaehlerResidueTermKFam_support_subset
    (Rfam : ∀ v : Place K F, v.CanonicalLocalResidueDataK) {ω : Ω[F⁄K]} (hω : ω ≠ 0)
    {D : Divisor K F} {α : Place K F → F} (hα : α ∈ adeleBdd D) :
    Function.support (kaehlerResidueTermKFam Rfam ω α)
      ⊆ ↑(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 kaehlerResidueTermKFam_eq_zero_of_ord_nonneg Rfam ?_
  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 kaehlerResidueTermKFam_support_finite
    (Rfam : ∀ v : Place K F, v.CanonicalLocalResidueDataK) {ω : Ω[F⁄K]} (hω : ω ≠ 0)
    {D : Divisor K F} {α : Place K F → F} (hα : α ∈ adeleBdd D) :
    (Function.support (kaehlerResidueTermKFam Rfam ω α)).Finite :=
  Set.Finite.subset (Finset.finite_toSet _)
    (kaehlerResidueTermKFam_support_subset Rfam hω hα)

theorem kaehlerResidueTermKFam_support_finite_of_adeleSpace
    (Rfam : ∀ v : Place K F, v.CanonicalLocalResidueDataK) {ω : Ω[F⁄K]} (hω : ω ≠ 0)
    {α : Place K F → F} (hα : α ∈ adeleSpace K F) :
    (Function.support (kaehlerResidueTermKFam Rfam ω α)).Finite := by
  obtain ⟨D, hD⟩ := mem_adeleSpace_iff.mp hα
  exact kaehlerResidueTermKFam_support_finite Rfam hω hD

def weilOfKaehlerK (Rfam : ∀ v : Place K F, v.CanonicalLocalResidueDataK)
    {ω : Ω[F⁄K]} (hω : ω ≠ 0) : Module.Dual K (adeleSpace K F) where
  toFun α := ∑ᶠ v, kaehlerResidueTermKFam Rfam ω (α : Place K F → F) v
  map_add' α β := by
    have hsupα := kaehlerResidueTermKFam_support_finite_of_adeleSpace Rfam hω α.2
    have hsupβ := kaehlerResidueTermKFam_support_finite_of_adeleSpace Rfam hω β.2
    rw [← finsum_add_distrib hsupα hsupβ]
    refine finsum_congr fun v => ?_
    simp only [kaehlerResidueTermKFam_apply]
    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 => ?_
    simp only [kaehlerResidueTermKFam_apply]
    rw [Submodule.coe_smul, Pi.smul_apply, Algebra.smul_def, mul_assoc,
      ← Algebra.smul_def, map_smul, map_smul]

theorem weilOfKaehlerK_apply (Rfam : ∀ v : Place K F, v.CanonicalLocalResidueDataK)
    {ω : Ω[F⁄K]} (hω : ω ≠ 0) (α : adeleSpace K F) :
    weilOfKaehlerK Rfam hω α
      = ∑ᶠ v, kaehlerResidueTermKFam Rfam ω (α : Place K F → F) v := rfl

theorem weilOfKaehlerK_vanish_adeleBdd_canonical
    (Rfam : ∀ v : Place K F, v.CanonicalLocalResidueDataK) {ω : Ω[F⁄K]} (hω : ω ≠ 0)
    {α : adeleSpace K F} (hα : (α : Place K F → F) ∈ adeleBdd (canonicalDivisorOf hω)) :
    weilOfKaehlerK Rfam hω α = 0 := by
  rw [weilOfKaehlerK_apply]
  exact finsum_eq_zero_of_forall_eq_zero
    (kaehlerResidueTermKFam_eq_zero_of_adeleBdd_canonical Rfam hω hα)

variable (K F)

def ResidueTheoremK : Prop :=
  ∀ (Rfam : ∀ v : Place K F, v.CanonicalLocalResidueDataK) [HasPrincipalDivisors K F]
    {ω : Ω[F⁄K]} (hω : ω ≠ 0) (f : F),
    weilOfKaehlerK Rfam hω ⟨diagonalHom K F f, diagonal_mem_adeleSpace f⟩ = 0

end SupportMachinery

end CanonicalKResidueTerm

end AlgebraicCurve

end

Statements phrased using this module (45)