Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AlgebraicCurve_RiemannRochRows.lean

definition module

Riemann–Roch rows for function fields: named statements

For a field extension F/K this module names, as Prop-valued statements, the successive rows of the Riemann–Roch programme; none of them is asserted here. Each of the six definitions quantifies internally over the curve hypotheses: IsCurveOver K F (existence of principal divisors, residue field K-finite at every place, and \Omega[F/K] free of rank one over F), HasCanonicalDivisor (every nonzero \omega\in\Omega[F/K] has a finitely supported divisor with coefficient v.\mathrm{ordDifferential}\,\omega at each place v), and for the duality rows the condition that every place's chosen differential d\pi_v spans \Omega[F/K] over F. Throughout, \ell(D)=\dim_K L(D) with L(D)=\{f\in F:\ v(f)\le \exp(D v)\text{ for all }v\}, the index of specialty i(D) is the K-dimension of the quotient of the adele space by the sum of the D-bounded adeles and the diagonal copy of F, \Omega(D) is the annihilator of that sum in the K-dual of the adele space, (\omega) is canonicalDivisorOf applied to a nonzero differential, and g is the genus defined as \lfloor(\deg(\omega)+2)^{+}/2\rfloor for a chosen nonzero differential.

The rows are: RiemannInequality, \deg D+1-g\le\ell(D); RiemannIndexFormula, i(D)=\ell(D)-(\deg D+1-g); WeilDualityAdelic, i(D)=\ell((\omega)-D); WeilDuality, \ell(D)-(\deg D+1-g)=\ell((\omega)-D); WeilOmegaEllAgrees, \dim_K\Omega(D)=\ell((\omega)-D) (the imported identity \dim_K\Omega(D)=i(D) makes this a restatement of the previous row); and FunctionFieldRiemannRoch, \ell(D)-\ell((\omega)-D)=\deg D+1-g, each for all divisors D and all nonzero \omega. Two short theorems record the linear rearrangements between them: FunctionFieldRiemannRoch follows from WeilDuality, and WeilDuality from RiemannIndexFormula together with WeilDualityAdelic. The constant 1 in these rows is the one appropriate when K is the full field of constants.

Relation to Mathlib

Mathlib has no Riemann–Roch theorem for function fields; the vocabulary used here (places as valuation subrings, divisors, L-spaces, adeles, index of specialty, canonical divisor and genus) is the project's own, built on Mathlib's valuation subrings, adic valuations of Dedekind domains and Kähler differentials.

Where it is used

These named rows are the interface through which downstream statements about curves and their function fields — in particular modular curves — may take Riemann–Roch, Weil duality or the Riemann inequality as an explicit hypothesis rather than re-deriving it.

References

  1. H. Stichtenoth, Algebraic Function Fields and Codes, Universitext, Springer, 1993
  2. C. Chevalley, Introduction to the Theory of Algebraic Functions of One Variable, Mathematical Surveys 6, American Mathematical Society, 1951

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_AlgebraicCurve_AdelicIndex
import Definitions.Def_AlgebraicCurve_CanonicalDivisor
import Definitions.Def_AlgebraicCurve_IsCurveOver

set_option autoImplicit false

noncomputable section

open KaehlerDifferential

namespace AlgebraicCurve

variable (K F : Type*) [Field K] [Field F] [Algebra K F]

def RiemannInequality : Prop :=
  ∀ [IsCurveOver K F] [HasCanonicalDivisor (K := K) (F := F)],
    ∀ D : Divisor K F, Divisor.degree D + 1 - (genus K F : ℤ) ≤ (ell D : ℤ)

def RiemannIndexFormula : Prop :=
  ∀ [IsCurveOver K F] [HasCanonicalDivisor (K := K) (F := F)],
    ∀ D : Divisor K F,
      (indexOfSpecialty D : ℤ) = (ell D : ℤ) - (Divisor.degree D + 1 - (genus K F : ℤ))

def WeilDualityAdelic : Prop :=
  ∀ [IsCurveOver K F] [HasCanonicalDivisor (K := K) (F := F)]
    [∀ v : Place K F, v.DCoordGenerates],
    ∀ {ω : Ω[F⁄K]} (hω : ω ≠ 0) (D : Divisor K F),
      (indexOfSpecialty D : ℤ) = (ell (canonicalDivisorOf hω - D) : ℤ)

def WeilDuality : Prop :=
  ∀ [IsCurveOver K F] [HasCanonicalDivisor (K := K) (F := F)]
    [∀ v : Place K F, v.DCoordGenerates],
    ∀ {ω : Ω[F⁄K]} (hω : ω ≠ 0) (D : Divisor K F),
      (ell D : ℤ) - (Divisor.degree D + 1 - (genus K F : ℤ))
        = (ell (canonicalDivisorOf hω - D) : ℤ)

def WeilOmegaEllAgrees : Prop :=
  ∀ [IsCurveOver K F] [HasCanonicalDivisor (K := K) (F := F)]
    [∀ v : Place K F, v.DCoordGenerates],
    ∀ {ω : Ω[F⁄K]} (hω : ω ≠ 0) (D : Divisor K F),
      (Module.finrank K ↥(omegaSpace D) : ℤ) = (ell (canonicalDivisorOf hω - D) : ℤ)

def FunctionFieldRiemannRoch : Prop :=
  ∀ [IsCurveOver K F] [HasCanonicalDivisor (K := K) (F := F)]
    [∀ v : Place K F, v.DCoordGenerates],
    ∀ {ω : Ω[F⁄K]} (hω : ω ≠ 0) (D : Divisor K F),
      (ell D : ℤ) - (ell (canonicalDivisorOf hω - D) : ℤ)
        = Divisor.degree D + 1 - (genus K F : ℤ)

theorem functionFieldRiemannRoch_of_riemann_and_duality
    (hWD : WeilDuality K F) : FunctionFieldRiemannRoch K F := by
  intro _ _ _ ω hω D
  linarith [hWD hω D]

theorem weilDuality_of_riemannIndex_of_adelic
    (hRI : RiemannIndexFormula K F) (hWD : WeilDualityAdelic K F) :
    WeilDuality K F := by
  intro _ _ _ ω hω D
  have h1 := hRI D
  have h2 := hWD hω D
  linarith

end AlgebraicCurve

end

Statements phrased using this module (24)