Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AlgebraicCurve_AdelicIndex.lean

definition module

Adelic vocabulary for Riemann–Roch: L-spaces, Weil differentials

Throughout, F/K is an extension of fields, with Place K F the project's places of F/K (valuation subrings of F containing the image of K, proper and principal), v.\mathrm{ord} the associated normalised order function, and Divisor K F the finitely supported \mathbb{Z}-valued functions on places. LSpace D abbreviates the project's riemannRochSpace D, the K-subspace \{f \in F : v(f) \le \exp(D(v))\ \forall v\}, equivalently f = 0 or \mathrm{ord}_v f \ge -D(v) for all v; ell D is its K-dimension. It is monotone in D and contains the image of K; ConstantsAreBase K F is the predicate L(0) = \operatorname{range}(K \to F), under which \ell(0)=1.

On the full product \prod_v F the module defines \mathbb{A}(D) = adeleBdd D, the K-submodule of families \alpha with v(\alpha_v) \le \exp(D(v)) for all v, the diagonal map diagonalHom, the adèle space adeleSpace K F = \bigsqcup_D \mathbb{A}(D) (a supremum, shown directed, so membership means lying in some \mathbb{A}(D)), and globalSub K F, the range of the diagonal. Then L(D) \cong \mathbb{A}(D) \cap F as K-spaces, adeleBddPrincipal K F D is the sum of the preimages of \mathbb{A}(D) and of F inside the adèle space, and indexOfSpecialty D is the K-dimension of the quotient by it. omegaSpace D is the annihilator of that sum in the K-dual of the adèle space, so a Weil differential of D is a functional vanishing on \mathbb{A}(D) and on diagonal elements; its dimension equals the index of specialty, and weilDifferentialModule K F is the (directed) supremum over D. Multiplication by f \in F acts componentwise (mulAdele, adeleSpaceMul under HasPrincipalDivisors), and weilSmul is the dual action, multiplicative in the contravariant sense and injective for f \ne 0; it carries \Omega(W) into \Omega(D) whenever g \in L(W-D), giving the injective residuePairing L(W-D) \to \Omega(D) and the inequality \ell(W-D) \le i(D).

Finally, WeilDifferentialRankOne (every Weil differential is uniquely f \cdot \varphi for a fixed nonzero \varphi), HasWeilCanonicalDivisor (each nonzero Weil differential lies in \Omega(W) for a largest W), the structure RiemannGenusReachedAt γ D₀ (carrying finite-dimensionality of L(D_0), the equality \deg D_0 - \ell(D_0) = \gamma - 1 and maximality of this quantity over all divisors), and the predicates RiemannGenusReached, StichtenothGenusExists, RiemannGenusBounded, IndexOfSpecialtyFinite are named hypotheses; nothing about their validity is asserted here.

Relation to Mathlib

The adèle-type objects are built directly as K-submodules of the product \prod_v F over the project's Place K F, not from Mathlib's finite adèle ring; places, divisors and riemannRochSpace are the project's own notions, and LSpace is an abbreviation for the latter.

Where it is used

This module fixes the vocabulary in which Riemann–Roch for the function field of a curve is stated and proved adelically: L-spaces and their dimensions, the adèle space with its bounded pieces, the index of specialty, Weil differentials with the multiplication action of F, and named genus hypotheses. It is imported widely by the curve-theoretic part of the development.

References

  1. H. Stichtenoth, Algebraic Function Fields and Codes, Universitext, Springer, 1993, Chapter I
  2. J.-P. Serre, Groupes algébriques et corps de classes, Hermann, 1959, Chapter II
  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_AdelicIndex.lean

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_AlgebraicCurve_Repartitions

set_option autoImplicit false

noncomputable section

open IsDedekindDomain WithZero Module

namespace AlgebraicCurve

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

abbrev LSpace (D : Divisor K F) : Submodule K F := riemannRochSpace D

abbrev ell (D : Divisor K F) : ℕ := Module.finrank K (LSpace D)

variable {D E : Divisor K F}

theorem mem_lSpace_iff {f : F} :
    f ∈ LSpace D ↔ ∀ v : Place K F, v.adicValuation f ≤ WithZero.exp (D v) := Iff.rfl

theorem mem_lSpace_iff_ord {f : F} :
    f ∈ LSpace D ↔ f = 0 ∨ ∀ v : Place K F, -D v ≤ v.ord f := by
  rcases eq_or_ne f 0 with rfl | hf
  · exact ⟨fun _ => Or.inl rfl, fun _ => (LSpace D).zero_mem⟩
  · refine Iff.trans ?_ (or_iff_right hf).symm
    refine forall_congr' fun v => ?_
    have hne : v.adicValuation f ≠ 0 := v.adicValuation_ne_zero hf
    rw [show v.adicValuation f = WithZero.exp (-v.ord f) by
          rw [Place.ord, neg_neg, WithZero.exp_log hne],
      WithZero.exp_le_exp, neg_le]

theorem lSpace_mono (hDE : D ≤ E) : LSpace D ≤ LSpace E := fun _ hf v =>
  (hf v).trans (WithZero.exp_le_exp.mpr (hDE v))

theorem algebraMap_mem_lSpace_zero (c : K) :
    algebraMap K F c ∈ LSpace (0 : Divisor K F) := fun v => by
  rw [Finsupp.coe_zero, Pi.zero_apply, WithZero.exp_zero]
  exact v.adicValuation_algebraMap_le_one c

theorem one_mem_lSpace_zero : (1 : F) ∈ LSpace (0 : Divisor K F) := by
  simpa using algebraMap_mem_lSpace_zero (K := K) (F := F) 1

def ConstantsAreBase (K F : Type*) [Field K] [Field F] [Algebra K F] : Prop :=
  LSpace (0 : Divisor K F) = LinearMap.range (Algebra.linearMap K F)

theorem ell_zero_eq_one_of_constantsAreBase (h : ConstantsAreBase K F) :
    ell (0 : Divisor K F) = 1 := by
  rw [ell, h, LinearMap.finrank_range_of_inj (f := Algebra.linearMap K F)
    (algebraMap K F).injective, Module.finrank_self]

def adeleBdd (D : Divisor K F) : Submodule K (Place K F → F) where
  carrier := {α | ∀ v : Place K F, v.adicValuation (α v) ≤ WithZero.exp (D v)}
  add_mem' := fun {α β} hα hβ v =>
    (v.adicValuation.map_add (α v) (β v)).trans (max_le (hα v) (hβ v))
  zero_mem' := fun v => by rw [Pi.zero_apply, Valuation.map_zero]; exact zero_le'
  smul_mem' := fun c α hα v => by
    rw [Pi.smul_apply, Algebra.smul_def, Valuation.map_mul]
    calc v.adicValuation (algebraMap K F c) * v.adicValuation (α v)
        ≤ 1 * v.adicValuation (α v) := by gcongr; exact v.adicValuation_algebraMap_le_one c
      _ = v.adicValuation (α v) := one_mul _
      _ ≤ WithZero.exp (D v) := hα v

variable {D E : Divisor K F}

@[simp]
theorem mem_adeleBdd {α : Place K F → F} :
    α ∈ adeleBdd D ↔ ∀ v : Place K F, v.adicValuation (α v) ≤ WithZero.exp (D v) := Iff.rfl

theorem adeleBdd_mono (hDE : D ≤ E) : adeleBdd D ≤ adeleBdd E := fun _ hα v =>
  (hα v).trans (WithZero.exp_le_exp.mpr (hDE v))

variable (K F) in

def diagonalHom : F →ₗ[K] (Place K F → F) where
  toFun f := fun _ => f
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

@[simp]
theorem diagonalHom_apply (f : F) (v : Place K F) : diagonalHom K F f v = f := rfl

theorem diagonalHom_injective [Nonempty (Place K F)] :
    Function.Injective (diagonalHom K F) := fun f g h => by
  simpa using congrFun h (Classical.arbitrary (Place K F))

theorem diagonal_mem_adeleBdd_iff {f : F} :
    diagonalHom K F f ∈ adeleBdd D ↔ f ∈ LSpace D := by
  simp only [mem_adeleBdd, diagonalHom_apply, mem_lSpace_iff]

variable (K F) in

def adeleSpace : Submodule K (Place K F → F) := ⨆ D : Divisor K F, adeleBdd D

theorem adeleBdd_le_adeleSpace : adeleBdd D ≤ adeleSpace K F := le_iSup adeleBdd D

theorem diagonal_mem_adeleSpace [HasPrincipalDivisors K F] (f : F) :
    diagonalHom K F f ∈ adeleSpace K F := by
  rcases eq_or_ne f 0 with rfl | hf
  · rw [map_zero]; exact (adeleSpace K F).zero_mem
  · obtain ⟨P, hPord, _⟩ := HasPrincipalDivisors.exists_divisor (K := K) f hf
    refine adeleBdd_le_adeleSpace (D := -P) ?_
    intro v
    rw [diagonalHom_apply,
      show ((-P : Divisor K F) v) = -v.ord f by rw [Finsupp.neg_apply, hPord v]]
    exact le_of_eq (by rw [Place.ord, neg_neg, WithZero.exp_log (v.adicValuation_ne_zero hf)])

variable (K F) in

def globalSub : Submodule K (Place K F → F) := LinearMap.range (diagonalHom K F)

theorem diagonal_mem_globalSub (f : F) : diagonalHom K F f ∈ globalSub K F :=
  LinearMap.mem_range_self _ f

theorem map_diagonal_lSpace (D : Divisor K F) :
    (LSpace D).map (diagonalHom K F) = adeleBdd D ⊓ globalSub K F := by
  ext α
  rw [Submodule.mem_map, Submodule.mem_inf]
  constructor
  · rintro ⟨f, hf, rfl⟩
    exact ⟨diagonal_mem_adeleBdd_iff.mpr hf, diagonal_mem_globalSub f⟩
  · rintro ⟨hbdd, hglob⟩
    obtain ⟨f, hf⟩ := LinearMap.mem_range.mp hglob
    exact ⟨f, diagonal_mem_adeleBdd_iff.mp (by rw [hf]; exact hbdd), hf⟩

def lSpaceEquivAdeleBddInfGlobal [Nonempty (Place K F)] (D : Divisor K F) :
    LSpace D ≃ₗ[K] (adeleBdd D ⊓ globalSub K F : Submodule K (Place K F → F)) :=
  (Submodule.equivMapOfInjective (diagonalHom K F) diagonalHom_injective (LSpace D)).trans
    (LinearEquiv.ofEq _ _ (map_diagonal_lSpace D))

theorem finrank_adeleBdd_inf_global_eq_ell [Nonempty (Place K F)] (D : Divisor K F) :
    Module.finrank K (adeleBdd D ⊓ globalSub K F : Submodule K (Place K F → F)) = ell D :=
  ((lSpaceEquivAdeleBddInfGlobal D).finrank_eq).symm

def indexOfSpecialty (D : Divisor K F) : ℕ :=
  Module.finrank K
    ((adeleSpace K F) ⧸
      ((adeleBdd D).comap (adeleSpace K F).subtype ⊔
        (globalSub K F).comap (adeleSpace K F).subtype))

theorem adeleBdd_directed :
    Directed (· ≤ ·) (adeleBdd (K := K) (F := F)) := fun D E =>
  ⟨D ⊔ E, adeleBdd_mono le_sup_left, adeleBdd_mono le_sup_right⟩

theorem mem_adeleSpace_iff {α : Place K F → F} :
    α ∈ adeleSpace K F ↔ ∃ D : Divisor K F, α ∈ adeleBdd D := by
  unfold adeleSpace
  exact Submodule.mem_iSup_of_directed _ adeleBdd_directed

variable (K F) in

abbrev adeleBddPrincipal (D : Divisor K F) : Submodule K (adeleSpace K F) :=
  (adeleBdd D).comap (adeleSpace K F).subtype ⊔
    (globalSub K F).comap (adeleSpace K F).subtype

theorem indexOfSpecialty_eq (D : Divisor K F) :
    indexOfSpecialty D = Module.finrank K (adeleSpace K F ⧸ adeleBddPrincipal K F D) := rfl

def omegaSpace (D : Divisor K F) : Submodule K (Module.Dual K (adeleSpace K F)) :=
  (adeleBddPrincipal K F D).dualAnnihilator

theorem omegaSpace_vanishBdd {D : Divisor K F} {φ : Module.Dual K (adeleSpace K F)}
    (hφ : φ ∈ omegaSpace D) {α : adeleSpace K F} (hα : (α : Place K F → F) ∈ adeleBdd D) :
    φ α = 0 :=
  (Submodule.mem_dualAnnihilator φ).mp hφ α (Submodule.mem_sup_left hα)

theorem omegaSpace_vanishGlobal {D : Divisor K F} {φ : Module.Dual K (adeleSpace K F)}
    (hφ : φ ∈ omegaSpace D) {α : adeleSpace K F} (hα : (α : Place K F → F) ∈ globalSub K F) :
    φ α = 0 :=
  (Submodule.mem_dualAnnihilator φ).mp hφ α (Submodule.mem_sup_right hα)

theorem omegaSpace_antitone {D E : Divisor K F} (hDE : D ≤ E) :
    omegaSpace E ≤ omegaSpace D :=
  Submodule.dualAnnihilator_anti
    (sup_le_sup_right (Submodule.comap_mono (adeleBdd_mono hDE)) _)

def omegaSpaceEquivIndexDual (D : Divisor K F) :
    omegaSpace D ≃ₗ[K] Module.Dual K (adeleSpace K F ⧸ adeleBddPrincipal K F D) :=
  (Submodule.dualQuotEquivDualAnnihilator (adeleBddPrincipal K F D)).symm

theorem finrank_omegaSpace_eq_indexOfSpecialty (D : Divisor K F) :
    Module.finrank K (omegaSpace D) = indexOfSpecialty D := by
  rw [indexOfSpecialty_eq, (omegaSpaceEquivIndexDual D).finrank_eq,
    Subspace.dual_finrank_eq]

variable (K F) in

def weilDifferentialModule : Submodule K (Module.Dual K (adeleSpace K F)) :=
  ⨆ D : Divisor K F, omegaSpace D

theorem omegaSpace_le_weilDifferentialModule (D : Divisor K F) :
    omegaSpace D ≤ weilDifferentialModule K F := le_iSup omegaSpace D

theorem omegaSpace_directed :
    Directed (· ≤ ·) (omegaSpace (K := K) (F := F)) := fun D E =>
  ⟨D ⊓ E, omegaSpace_antitone inf_le_left, omegaSpace_antitone inf_le_right⟩

theorem mem_weilDifferentialModule_iff {φ : Module.Dual K (adeleSpace K F)} :
    φ ∈ weilDifferentialModule K F ↔ ∃ D : Divisor K F, φ ∈ omegaSpace D := by
  unfold weilDifferentialModule
  exact Submodule.mem_iSup_of_directed _ omegaSpace_directed

variable (K) in

def mulAdele (f : F) : (Place K F → F) →ₗ[K] (Place K F → F) where
  toFun α := fun v => f * α v
  map_add' α β := funext fun v => mul_add f (α v) (β v)
  map_smul' c α := funext fun v => by
    simp only [Pi.smul_apply, Algebra.smul_def, RingHom.id_apply]; ring

@[simp]
theorem mulAdele_apply (f : F) (α : Place K F → F) (v : Place K F) :
    mulAdele K f α v = f * α v := rfl

@[simp]
theorem mulAdele_one : mulAdele K (1 : F) = LinearMap.id :=
  LinearMap.ext fun α => funext fun v => one_mul (α v)

theorem mulAdele_mul (f g : F) :
    mulAdele K (f * g) = (mulAdele K f).comp (mulAdele K g) :=
  LinearMap.ext fun α => funext fun v => mul_assoc f g (α v)

theorem mulAdele_mem_adeleBdd_sub {f : F} (hf : f ≠ 0) {P : Divisor K F}
    (hP : ∀ v, P v = v.ord f) {D : Divisor K F} {α : Place K F → F}
    (hα : α ∈ adeleBdd D) : mulAdele K f α ∈ adeleBdd (D - P) := by
  intro v
  rw [mulAdele_apply, Valuation.map_mul, Finsupp.sub_apply, hP v,
    show v.adicValuation f = WithZero.exp (-v.ord f) by
      rw [Place.ord, neg_neg, WithZero.exp_log (v.adicValuation_ne_zero hf)]]
  calc WithZero.exp (-v.ord f) * v.adicValuation (α v)
      ≤ WithZero.exp (-v.ord f) * WithZero.exp (D v) := by gcongr; exact hα v
    _ = WithZero.exp (D v - v.ord f) := by rw [← WithZero.exp_add]; ring_nf

theorem mulAdele_globalSub_le (f : F) :
    (globalSub K F).map (mulAdele K f) ≤ globalSub K F := by
  rintro _ ⟨α, ⟨g, rfl⟩, rfl⟩
  exact ⟨f * g, funext fun v => by simp⟩

theorem mulAdele_mem_adeleSpace [HasPrincipalDivisors K F] (f : F) {α : Place K F → F}
    (hα : α ∈ adeleSpace K F) : mulAdele K f α ∈ adeleSpace K F := by
  rcases eq_or_ne f 0 with rfl | hf
  · have h0 : mulAdele K (0 : F) α = 0 := funext fun v => by simp
    rw [h0]; exact (adeleSpace K F).zero_mem
  · obtain ⟨D, hD⟩ := mem_adeleSpace_iff.mp hα
    obtain ⟨P, hP, _⟩ := HasPrincipalDivisors.exists_divisor (K := K) f hf
    exact adeleBdd_le_adeleSpace (D := D - P) (mulAdele_mem_adeleBdd_sub hf hP hD)

variable (K F) in

def adeleSpaceMul [HasPrincipalDivisors K F] (f : F) :
    adeleSpace K F →ₗ[K] adeleSpace K F :=
  (mulAdele K f).restrict fun _ => mulAdele_mem_adeleSpace f

@[simp]
theorem adeleSpaceMul_coe [HasPrincipalDivisors K F] (f : F) (α : adeleSpace K F) :
    (adeleSpaceMul K F f α : Place K F → F) = mulAdele K f (α : Place K F → F) := rfl

variable (K F) in

def weilSmul [HasPrincipalDivisors K F] (f : F) :
    Module.Dual K (adeleSpace K F) →ₗ[K] Module.Dual K (adeleSpace K F) :=
  (adeleSpaceMul K F f).dualMap

@[simp]
theorem weilSmul_apply [HasPrincipalDivisors K F] (f : F)
    (φ : Module.Dual K (adeleSpace K F)) (α : adeleSpace K F) :
    weilSmul K F f φ α = φ (adeleSpaceMul K F f α) := rfl

theorem adeleSpaceMul_one [HasPrincipalDivisors K F] :
    adeleSpaceMul K F (1 : F) = LinearMap.id := by
  refine LinearMap.ext fun α => Subtype.ext ?_
  show mulAdele K (1 : F) (α : Place K F → F) = (α : Place K F → F)
  rw [mulAdele_one, LinearMap.id_apply]

theorem adeleSpaceMul_mul [HasPrincipalDivisors K F] (f g : F) :
    adeleSpaceMul K F (f * g) = (adeleSpaceMul K F f).comp (adeleSpaceMul K F g) := by
  refine LinearMap.ext fun α => Subtype.ext ?_
  show mulAdele K (f * g) (α : Place K F → F) = mulAdele K f (mulAdele K g (α : Place K F → F))
  rw [mulAdele_mul, LinearMap.comp_apply]

@[simp]
theorem weilSmul_one [HasPrincipalDivisors K F] :
    weilSmul K F (1 : F) = LinearMap.id := by
  unfold weilSmul; rw [adeleSpaceMul_one]; ext; simp

theorem weilSmul_mul [HasPrincipalDivisors K F] (f g : F) :
    weilSmul K F (f * g) = (weilSmul K F g).comp (weilSmul K F f) := by
  unfold weilSmul; rw [adeleSpaceMul_mul, LinearMap.dualMap_comp_dualMap]

theorem weilSmul_injective [HasPrincipalDivisors K F] {f : F} (hf : f ≠ 0) :
    Function.Injective (weilSmul K F f) := by
  apply Function.LeftInverse.injective (g := weilSmul K F f⁻¹)
  intro φ
  rw [← LinearMap.comp_apply, ← weilSmul_mul, mul_inv_cancel₀ hf, weilSmul_one,
    LinearMap.id_apply]

theorem weilSmul_mem_omegaSpace_add [HasPrincipalDivisors K F] {f : F} (hf : f ≠ 0)
    {P : Divisor K F} (hP : ∀ v, P v = v.ord f) {D : Divisor K F}
    {φ : Module.Dual K (adeleSpace K F)} (hφ : φ ∈ omegaSpace D) :
    weilSmul K F f φ ∈ omegaSpace (D + P) := by
  rw [omegaSpace, Submodule.mem_dualAnnihilator]

  intro α hα
  obtain ⟨β, hβ, γ, hγ, rfl⟩ := Submodule.mem_sup.mp hα
  rw [map_add, weilSmul_apply, weilSmul_apply]

  have hβ' : (adeleSpaceMul K F f β : Place K F → F) ∈ adeleBdd D := by
    rw [adeleSpaceMul_coe]
    have h := mulAdele_mem_adeleBdd_sub hf hP (D := D + P) (Submodule.mem_comap.mp hβ)
    rwa [add_sub_cancel_right] at h

  have hγ' : (adeleSpaceMul K F f γ : Place K F → F) ∈ globalSub K F :=
    mulAdele_globalSub_le f ⟨_, Submodule.mem_comap.mp hγ, rfl⟩
  rw [omegaSpace_vanishBdd hφ hβ', omegaSpace_vanishGlobal hφ hγ', add_zero]

theorem weilSmul_mem_omegaSpace_of_mem_lSpace [HasPrincipalDivisors K F]
    {W D : Divisor K F} {φ : Module.Dual K (adeleSpace K F)} (hφ : φ ∈ omegaSpace W)
    {g : F} (hg : g ∈ LSpace (W - D)) :
    weilSmul K F g φ ∈ omegaSpace D := by
  rcases eq_or_ne g 0 with rfl | hg0
  ·
    have h0 : weilSmul K F (0 : F) φ = 0 := by
      ext α; simp only [weilSmul_apply]
      refine omegaSpace_vanishBdd hφ ?_
      intro v
      simp only [adeleSpaceMul_coe, mulAdele_apply, zero_mul, Valuation.map_zero]
      exact zero_le'
    rw [h0]; exact (omegaSpace D).zero_mem
  ·
    obtain ⟨P, hPord, _⟩ := HasPrincipalDivisors.exists_divisor (K := K) g hg0
    refine omegaSpace_antitone ?_ (weilSmul_mem_omegaSpace_add hg0 hPord hφ)

    intro v
    rw [Finsupp.add_apply, hPord v]
    have hgL := (mem_lSpace_iff_ord.mp hg).resolve_left hg0 v
    rw [Finsupp.sub_apply] at hgL
    linarith

variable (K F) in

def residuePairing [HasPrincipalDivisors K F] (W D : Divisor K F)
    {φ : Module.Dual K (adeleSpace K F)} (hφ : φ ∈ omegaSpace W) :
    LSpace (W - D) →ₗ[K] omegaSpace D where
  toFun g := ⟨weilSmul K F (g : F) φ, weilSmul_mem_omegaSpace_of_mem_lSpace hφ g.2⟩
  map_add' g₁ g₂ := by
    refine Subtype.ext ?_
    show weilSmul K F ((g₁ : F) + (g₂ : F)) φ
      = weilSmul K F (g₁ : F) φ + weilSmul K F (g₂ : F) φ
    ext α; simp only [weilSmul_apply, LinearMap.add_apply]
    rw [← map_add]; congr 1
    exact Subtype.ext (funext fun v => by simp [add_mul])
  map_smul' c g := by
    refine Subtype.ext ?_
    show weilSmul K F (c • (g : F)) φ = c • weilSmul K F (g : F) φ
    ext α; simp only [weilSmul_apply, LinearMap.smul_apply]
    rw [← map_smul]; congr 1
    exact Subtype.ext (funext fun v => by simp [Algebra.smul_def]; ring)

@[simp]
theorem residuePairing_apply_coe [HasPrincipalDivisors K F] (W D : Divisor K F)
    {φ : Module.Dual K (adeleSpace K F)} (hφ : φ ∈ omegaSpace W) (g : LSpace (W - D)) :
    (residuePairing K F W D hφ g : Module.Dual K (adeleSpace K F))
      = weilSmul K F (g : F) φ := rfl

theorem residuePairing_injective [HasPrincipalDivisors K F] (W D : Divisor K F)
    {φ : Module.Dual K (adeleSpace K F)} (hφ : φ ∈ omegaSpace W) (hφ0 : φ ≠ 0) :
    Function.Injective (residuePairing K F W D hφ) := by
  have hsub : ∀ g₁ g₂ : F, adeleSpaceMul K F (g₁ - g₂)
      = adeleSpaceMul K F g₁ - adeleSpaceMul K F g₂ := fun g₁ g₂ => by
    refine LinearMap.ext fun α => Subtype.ext (funext fun v => ?_)
    simp only [adeleSpaceMul_coe, mulAdele_apply, LinearMap.sub_apply,
      Submodule.coe_sub, Pi.sub_apply, sub_mul]
  intro g₁ g₂ hg
  have hg' : weilSmul K F ((g₁ : F) - (g₂ : F)) φ = 0 := by
    have h := congrArg Subtype.val hg
    simp only [residuePairing_apply_coe] at h
    ext α
    simp only [weilSmul_apply, hsub, LinearMap.sub_apply, map_sub, LinearMap.zero_apply,
      sub_eq_zero]
    exact LinearMap.congr_fun h α
  rcases eq_or_ne ((g₁ : F) - (g₂ : F)) 0 with hd | hd
  · exact Subtype.ext (sub_eq_zero.mp hd)
  · exact absurd (weilSmul_injective hd (by rw [hg', map_zero])) hφ0

theorem ell_sub_le_indexOfSpecialty [HasPrincipalDivisors K F] (W D : Divisor K F)
    {φ : Module.Dual K (adeleSpace K F)} (hφ : φ ∈ omegaSpace W) (hφ0 : φ ≠ 0)
    [Module.Finite K (omegaSpace (K := K) (F := F) D)] :
    ell (W - D) ≤ indexOfSpecialty D := by
  rw [← finrank_omegaSpace_eq_indexOfSpecialty]
  exact LinearMap.finrank_le_finrank_of_injective (residuePairing_injective W D hφ hφ0)

variable (K F)

def WeilDifferentialRankOne [HasPrincipalDivisors K F] : Prop :=
  ∀ {φ : Module.Dual K (adeleSpace K F)}, φ ∈ weilDifferentialModule K F → φ ≠ 0 →
    ∀ {μ : Module.Dual K (adeleSpace K F)}, μ ∈ weilDifferentialModule K F →
      ∃! f : F, μ = weilSmul K F f φ

def HasWeilCanonicalDivisor : Prop :=
  ∀ {φ : Module.Dual K (adeleSpace K F)}, φ ∈ weilDifferentialModule K F → φ ≠ 0 →
    ∃ W : Divisor K F, φ ∈ omegaSpace W ∧ ∀ D : Divisor K F, φ ∈ omegaSpace D → D ≤ W

variable {K F}

structure RiemannGenusReachedAt (γ : ℤ) (D₀ : Divisor K F) : Prop where
  finite : FiniteDimensional K (LSpace D₀)
  eq : Divisor.degree D₀ - (ell D₀ : ℤ) = γ - 1
  isMax : ∀ D : Divisor K F, Divisor.degree D - (ell D : ℤ) ≤ γ - 1

variable (K F) in

def RiemannGenusReached (γ : ℤ) : Prop :=
  Nonempty (Place K F) ∧ FiniteDimensional K (LSpace (0 : Divisor K F)) ∧
    ∃ D₀ : Divisor K F, RiemannGenusReachedAt γ D₀

variable (K F) in

def StichtenothGenusExists : Prop :=
  Nonempty (Place K F) ∧ FiniteDimensional K (LSpace (0 : Divisor K F)) ∧
    ∃ (γ : ℤ) (D₀ : Divisor K F), RiemannGenusReachedAt γ D₀

variable (K F) in

def RiemannGenusBounded : Prop :=
  ∃ γ : ℤ, ∀ D : Divisor K F, Divisor.degree D - (ell D : ℤ) ≤ γ

variable (K F) in

def IndexOfSpecialtyFinite : Prop :=
  ∃ D₀ : Divisor K F, Module.Finite K (adeleSpace K F ⧸ adeleBddPrincipal K F D₀)

end AlgebraicCurve

end

Statements phrased using this module (278)

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