Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AlgebraicCurve_Repartitions.lean

definition module

Repartitions, Riemann–Roch spaces and the genus

Throughout, F is a field extension of a field K, and a place of F/K is a valuation subring of F containing the image of K, different from F and a principal ideal ring, hence a discrete valuation ring; Place.adicValuation is the associated \mathbb{Z}^{m0}-valued valuation of F and Place.ord is -\log of it. A group of helper lemmas records the basic translation between the two: the valuation is \le 1 on the valuation subring, in particular on the image of K; for f \neq 0 one has v(f) = \exp(-\operatorname{ord}_v f); and v(f) \le \exp n holds exactly when f = 0 or -n \le \operatorname{ord}_v f, with the specialisations n = 0 and the negated form \neg(v(f) \le 1) \leftrightarrow \operatorname{ord}_v f < 0.

repartitions K F is the F-subalgebra of the product \prod_v F generated by those families \alpha for which \{v : \neg\, v(\alpha_v) \le 1\} is finite, i.e. the subalgebra generated by the families integral at all but finitely many places; membership is recorded for families with finitely many places where \operatorname{ord}_v(\alpha_v) < 0, and for families bounded by a divisor. For a divisor D (a finitely supported integer-valued function on places) repartitionsOf D is the K-submodule of repartitions K F cut out by v(\alpha_v) \le \exp(D v) for every v, equivalently \alpha_v = 0 or -D v \le \operatorname{ord}_v(\alpha_v) at each v; it is monotone in D. riemannRochSpace D is the corresponding K-submodule \{f \in F : \forall v,\ v(f) \le \exp(D v)\} of F, with the same \operatorname{ord}-form description. principalRepartitions K F is the diagonal copy of F inside repartitions K F, viewed as a K-submodule; membership means precisely that the family is constant. Finally H1 D is the quotient K-module of repartitions K F by repartitionsOf D ⊔ principalRepartitions K F, and genusFF K F is the K-dimension of H1 0, so zero when that dimension is infinite.

Relation to Mathlib

Mathlib supplies the valuation machinery used here (valuation subrings, the adic valuation of a height-one prime, WithZero.exp/log); the repartitions (adele) algebra, the spaces L(D), the quotients H1 and the genus are the project's own, built on its Place and Divisor notions.

Where it is used

These definitions provide the Riemann–Roch apparatus attached to the project's places and divisors of F/K, alongside the divisor class groups Pic, Pic0 and their p-power torsion on which the Abel–Jacobi counting predicate is formulated.

References

  1. H. Stichtenoth, Algebraic Function Fields and Codes, 2nd edition, Graduate Texts in Mathematics 254, Springer, 2009, §§1.4–1.5
  2. A. Weil, Basic Number Theory, Grundlehren der mathematischen Wissenschaften 144, Springer, 1967, Chapter VI
  3. 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_Repartitions.lean

Imports

Imported by

Declarations

Source

import Definitions.Def_AlgebraicCurve_DivisorClassGroup

set_option autoImplicit false

noncomputable section

open WithZero

namespace AlgebraicCurve

namespace Place

variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

theorem adicValuation_le_one_of_mem {x : F} (hx : x ∈ v.toValuationSubring) :
    v.adicValuation x ≤ 1 := by
  have h := (v.adicValuation_coe ⟨x, hx⟩).trans_le
    (v.heightOneSpectrum.intValuation_le_one ⟨x, hx⟩)
  simpa using h

theorem adicValuation_algebraMap_le_one (a : K) :
    v.adicValuation (algebraMap K F a) ≤ 1 :=
  v.adicValuation_le_one_of_mem (v.algebraMap_mem' a)

theorem adicValuation_eq_exp_neg_ord {f : F} (hf : f ≠ 0) :
    v.adicValuation f = exp (-v.ord f) := by
  unfold ord
  rw [neg_neg, exp_log (v.adicValuation_ne_zero hf)]

theorem adicValuation_le_exp_iff {f : F} {n : ℤ} :
    v.adicValuation f ≤ exp n ↔ f = 0 ∨ -n ≤ v.ord f := by
  rcases eq_or_ne f 0 with rfl | hf
  · simp
  · rw [v.adicValuation_eq_exp_neg_ord hf, exp_le_exp, neg_le, or_iff_right hf]

theorem adicValuation_le_one_iff {f : F} :
    v.adicValuation f ≤ 1 ↔ f = 0 ∨ 0 ≤ v.ord f := by
  simpa using v.adicValuation_le_exp_iff (n := 0)

theorem not_adicValuation_le_one_iff {f : F} :
    ¬v.adicValuation f ≤ 1 ↔ v.ord f < 0 := by
  rw [v.adicValuation_le_one_iff, not_or, not_le]
  constructor
  · exact fun h => h.2
  · exact fun h => ⟨fun h0 => by simp [h0] at h, h⟩

end Place

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

def repartitions : Subalgebra F (Place K F → F) :=
  Algebra.adjoin F
    {α : Place K F → F | {v : Place K F | ¬v.adicValuation (α v) ≤ 1}.Finite}

variable {K F}

theorem mem_repartitions_of_finite {α : Place K F → F}
    (hα : {v : Place K F | ¬v.adicValuation (α v) ≤ 1}.Finite) :
    α ∈ repartitions K F :=
  Algebra.subset_adjoin hα

theorem mem_repartitions_of_finite_ord {α : Place K F → F}
    (hα : {v : Place K F | v.ord (α v) < 0}.Finite) :
    α ∈ repartitions K F :=
  mem_repartitions_of_finite <| by
    rwa [show {v : Place K F | ¬v.adicValuation (α v) ≤ 1}
        = {v : Place K F | v.ord (α v) < 0} from
      Set.ext fun v => v.not_adicValuation_le_one_iff]

theorem mem_repartitions_of_forall_le_exp (D : Divisor K F) (α : Place K F → F)
    (h : ∀ v : Place K F, v.adicValuation (α v) ≤ exp (D v)) :
    α ∈ repartitions K F :=
  mem_repartitions_of_finite <| D.support.finite_toSet.subset fun v hv => by
    rw [Finset.mem_coe, Finsupp.mem_support_iff]
    intro hD0
    exact hv ((h v).trans (by rw [hD0]; simp))

def repartitionsOf (D : Divisor K F) : Submodule K ↥(repartitions K F) where
  carrier :=
    {α | ∀ v : Place K F, v.adicValuation ((α : Place K F → F) v) ≤ exp (D v)}
  zero_mem' := by
    intro v
    show v.adicValuation (0 : F) ≤ exp (D v)
    simp
  add_mem' := by
    intro α β hα hβ v
    exact (Valuation.map_add _ _ _).trans (max_le (hα v) (hβ v))
  smul_mem' := by
    intro c α hα v
    show v.adicValuation (c • (α : Place K F → F) v) ≤ exp (D v)
    rw [Algebra.smul_def, map_mul]
    exact (mul_le_of_le_one_left' (v.adicValuation_algebraMap_le_one c)).trans (hα v)

theorem mem_repartitionsOf_iff {D : Divisor K F} {α : ↥(repartitions K F)} :
    α ∈ repartitionsOf D ↔
      ∀ v : Place K F,
        (α : Place K F → F) v = 0 ∨ -D v ≤ v.ord ((α : Place K F → F) v) := by
  show (∀ v : Place K F, v.adicValuation ((α : Place K F → F) v) ≤ exp (D v)) ↔ _
  exact forall_congr' fun v => v.adicValuation_le_exp_iff

theorem repartitionsOf_mono {D D' : Divisor K F} (h : D ≤ D') :
    repartitionsOf D ≤ repartitionsOf D' := fun _ hα v =>
  (hα v).trans (exp_le_exp.mpr (Finsupp.le_def.mp h v))

def riemannRochSpace (D : Divisor K F) : Submodule K F where
  carrier := {f | ∀ v : Place K F, v.adicValuation f ≤ exp (D v)}
  zero_mem' := by
    intro v
    simp
  add_mem' := by
    intro f g hf hg v
    exact (Valuation.map_add _ _ _).trans (max_le (hf v) (hg v))
  smul_mem' := by
    intro c f hf v
    show v.adicValuation (c • f) ≤ exp (D v)
    rw [Algebra.smul_def, map_mul]
    exact (mul_le_of_le_one_left' (v.adicValuation_algebraMap_le_one c)).trans (hf v)

theorem mem_riemannRochSpace_iff {D : Divisor K F} {f : F} :
    f ∈ riemannRochSpace D ↔ ∀ v : Place K F, f = 0 ∨ -D v ≤ v.ord f := by
  show (∀ v : Place K F, v.adicValuation f ≤ exp (D v)) ↔ _
  exact forall_congr' fun v => v.adicValuation_le_exp_iff

variable (K F) in

def principalRepartitions : Submodule K ↥(repartitions K F) :=
  (LinearMap.range (Algebra.linearMap F ↥(repartitions K F))).restrictScalars K

theorem mem_principalRepartitions_iff {α : ↥(repartitions K F)} :
    α ∈ principalRepartitions K F ↔
      ∃ f : F, (α : Place K F → F) = fun _ => f := by
  simp only [principalRepartitions, Submodule.restrictScalars_mem, LinearMap.mem_range,
    Algebra.linearMap_apply]
  constructor
  · rintro ⟨f, rfl⟩
    exact ⟨f, rfl⟩
  · rintro ⟨f, hf⟩
    exact ⟨f, Subtype.ext hf.symm⟩

abbrev H1 (D : Divisor K F) : Type _ :=
  ↥(repartitions K F) ⧸ (repartitionsOf D ⊔ principalRepartitions K F)

variable (K F) in

def genusFF : ℕ := Module.finrank K (H1 (0 : Divisor K F))

end AlgebraicCurve

end

Statements phrased using this module (545)

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