Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AlgebraicCurve_PoleDivisorPackage.lean

definition module

Pole-divisor packages and transcendence towers for function fields

Two bundles of data for the divisor theory of a function field F over a base field K, in the project's framework where a place v of F/K is a proper valuation subring containing K whose ring is a principal ideal domain, \mathrm{Divisor}\,K\,F is the free abelian group on places, v.\mathrm{ord} is the normalised valuation, \deg is \sum_v D(v)\,[\kappa(v):K], and LSpace D is the space of f with \mathrm{ord}_v f \ge -D(v) for all v.

PoleDivisorPackage K F carries: an element x \in F; an effective divisor B \ge 0 with x \in L(B); a positive natural number n with \deg B = n; a natural number c; a family u_1,\dots,u_n \in L(cB); and, as a field of the structure, the assertion that the doubly indexed family (x^{j}u_i)_{j \in \mathbb{N},\, i \le n} is K-linearly independent. Note that n is tied to \deg B only, not to [F:K(x)], and the transcendence of x is encoded implicitly in the independence field. HasPoleDivisorPackage is its nonemptiness.

TranscendenceTower K E F, for a tower K \subseteq E \subseteq F, carries x \in E whose powers (x^{j})_{j \in \mathbb{N}} are K-linearly independent, together with a place v of E/K with \deg v = 1, \mathrm{ord}_v x = -1, and \mathrm{ord}_u x \ge 0 for every other place u of E/K; so x has a single simple pole, at a rational place. Its poleDivisor is the pullback to F (a sum over places above v weighted by the ramification indices, defined as the least positive value of \mathrm{ord}_w on E^{\times}) of the divisor 1\cdot v, available under separability of F/E and the existence of principal divisors on F; xF is the image of x in F, and RegularOutside A T says that every element of a ring A mapping to E lies in the valuation subring of each place u \ne v.

The remaining declarations are predicates on such a tower: IntegralBasisInLSpace (and its nonemptiness HasIntegralBasisInLSpace) asks for some c \in \mathbb{N} and an E-linearly independent family of [F:E] elements of F lying in L(c \cdot \mathrm{poleDivisor}); HasIntegralBasisRegularOutside asks instead for an E-linearly independent family of [F:E] elements regular at every place w of F/K whose restriction to E is not v; and HasRegularFractionSubring asks for a K-subalgebra A \subseteq E with E as fraction field all of whose elements are regular away from v.

Relation to Mathlib

Mathlib has no theory of places and divisors of a function field in this shape; these structures are built on the project's own Place, Divisor, ramification index, pullback and LSpace (the Riemann–Roch space) rather than on Mathlib's Ideal.ramificationIdx and Dedekind-domain machinery.

Where it is used

These data types package the hypotheses used in the project's treatment of Riemann's inequality for a function field — bounding \deg D - \ell(D) and thereby producing the genus and the finiteness of the index of specialty — which underlies the Riemann–Roch theory applied to modular curves.

References

  1. H. Stichtenoth, Algebraic Function Fields and Codes, Graduate Texts in Mathematics 254, Springer, 2009, I.4.12–I.4.14 and I.5.2
  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_PoleDivisorPackage.lean

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_AlgebraicCurve_DivisorPushPull
import Definitions.Def_AlgebraicCurve_AdelicIndex

set_option autoImplicit false

noncomputable section

namespace AlgebraicCurve

structure PoleDivisorPackage (K F : Type*) [Field K] [Field F] [Algebra K F] where

  x : F

  B : Divisor K F

  hB_eff : 0 ≤ B

  hx_mem : x ∈ LSpace B

  n : ℕ

  hn_pos : 0 < n

  degB_eq : Divisor.degree B = n

  c : ℕ

  u : Fin n → F

  hu_mem : ∀ i, u i ∈ LSpace (c • B)

  lin_indep : LinearIndependent K (fun p : ℕ × Fin n => x ^ p.1 * u p.2)

def HasPoleDivisorPackage (K F : Type*) [Field K] [Field F] [Algebra K F] : Prop :=
  Nonempty (PoleDivisorPackage K F)

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

structure TranscendenceTower (K E F : Type*) [Field K] [Field E] [Field F]
    [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F] where

  x : E

  hx_indep : LinearIndependent K (fun j : ℕ => x ^ j)

  v : Place K E

  hvdeg : v.deg = 1

  hxv : v.ord x = -1

  hxreg : ∀ u : Place K E, u ≠ v → 0 ≤ u.ord x

namespace TranscendenceTower

variable (T : TranscendenceTower K E F)

abbrev xF : F := algebraMap E F T.x

def poleDivisor [Algebra.IsSeparable E F] [HasPrincipalDivisors K F] : Divisor K F :=
  Divisor.pullback F (Finsupp.single T.v 1)

def RegularOutside (A : Type*) [CommRing A] [Algebra A E] (T : TranscendenceTower K E F) : Prop :=
  ∀ u : Place K E, u ≠ T.v → ∀ a : A, algebraMap A E a ∈ u.toValuationSubring

end TranscendenceTower

structure IntegralBasisInLSpace [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]
    (T : TranscendenceTower K E F) where

  c : ℕ

  u : Fin (Module.finrank E F) → F

  hu_indep : LinearIndependent E u

  hu_mem : ∀ i, u i ∈ LSpace (c • T.poleDivisor)

variable (K E F) in

def HasIntegralBasisInLSpace [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]
    (T : TranscendenceTower K E F) : Prop :=
  Nonempty (IntegralBasisInLSpace T)

variable (K E F) in

def HasIntegralBasisRegularOutside [Algebra.IsSeparable E F] (T : TranscendenceTower K E F) : Prop :=
  ∃ u : Fin (Module.finrank E F) → F, LinearIndependent E u ∧
    ∀ i, ∀ w : Place K F, w.restrict E ≠ T.v → 0 ≤ w.ord (u i)

variable (K E F) in

def HasRegularFractionSubring (T : TranscendenceTower K E F) : Prop :=
  ∃ (A : Subalgebra K E), IsFractionRing A E ∧
    ∀ u : Place K E, u ≠ T.v → ∀ a ∈ A, a ∈ u.toValuationSubring

end AlgebraicCurve

end

Statements phrased using this module (17)