Module

Index.lean

Nyll.AlgebraicCurves.Cohomology.Adelic.Index

68 declarations indexed from sourceView source ↗

Module documentation

Adelic spaces, indices of specialty and Weil differentials. Valuation bounds and global functions define the quotients and genus conditions.

Imports1

Nyll.AlgebraicCurves.Cohomology.Adelic.Repartitions

Imported by242

abbrev

LSpace

L29 ↗

AlgebraicCurve.LSpace

Documentation

The Riemann--Roch subspace of functions bounded by a divisor.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

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

abbrev

ell

L32 ↗

AlgebraicCurve.ell

Documentation

The dimension of the Riemann--Roch space of a divisor.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

abbrev ell (D : Divisor K F) : ℕ

theorem

mem_lSpace_iff

L36 ↗

AlgebraicCurve.mem_lSpace_iff

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}

Lean source · statement

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

theorem

mem_lSpace_iff_ord

L39 ↗

AlgebraicCurve.mem_lSpace_iff_ord

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}

Lean source · statement

theorem mem_lSpace_iff_ord {f : F} :
    f ∈ LSpace D ↔ f = 0 ∨ ∀ v : Place K F, -D v ≤ v.ord f

theorem

lSpace_mono

L50 ↗

AlgebraicCurve.lSpace_mono

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}

Lean source · statement

theorem lSpace_mono (hDE : D ≤ E) : LSpace D ≤ LSpace E

theorem

algebraMap_mem_lSpace_zero

L53 ↗

AlgebraicCurve.algebraMap_mem_lSpace_zero

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}

Lean source · statement

theorem algebraMap_mem_lSpace_zero (c : K) :
    algebraMap K F c ∈ LSpace (0 : Divisor K F)

theorem

one_mem_lSpace_zero

L58 ↗

AlgebraicCurve.one_mem_lSpace_zero

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}

Lean source · statement

theorem one_mem_lSpace_zero : (1 : F) ∈ LSpace (0 : Divisor K F)

def

ConstantsAreBase

L62 ↗

AlgebraicCurve.ConstantsAreBase

Documentation

The functions bounded by the zero divisor are exactly the base-field constants.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}

Lean source · statement

def ConstantsAreBase (K F : Type*) [Field K] [Field F] [Algebra K F] : Prop

theorem

ell_zero_eq_one_of_constantsAreBase

L65 ↗

AlgebraicCurve.ell_zero_eq_one_of_constantsAreBase

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}

Lean source · statement

theorem ell_zero_eq_one_of_constantsAreBase (h : ConstantsAreBase K F) :
    ell (0 : Divisor K F) = 1

def

adeleBdd

L71 ↗

AlgebraicCurve.adeleBdd

Documentation

The submodule of place-indexed families bounded by a divisor.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}

Lean source · full declaration

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

theorem

mem_adeleBdd

L86 ↗

AlgebraicCurve.mem_adeleBdd

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}

Lean source · statement

theorem mem_adeleBdd {α : Place K F → F} :
    α ∈ adeleBdd D ↔ ∀ v : Place K F, v.adicValuation (α v) ≤ WithZero.exp (D v)

theorem

adeleBdd_mono

L89 ↗

AlgebraicCurve.adeleBdd_mono

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}

Lean source · statement

theorem adeleBdd_mono (hDE : D ≤ E) : adeleBdd D ≤ adeleBdd E

def

diagonalHom

L94 ↗

AlgebraicCurve.diagonalHom

Documentation

The linear map sending a function to its constant family at all places.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in

Lean source · full declaration

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

theorem

diagonalHom_apply

L99 ↗

AlgebraicCurve.diagonalHom_apply

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in

Lean source · statement

theorem diagonalHom_apply (f : F) (v : Place K F) : diagonalHom K F f v = f

theorem

diagonalHom_injective

L101 ↗

AlgebraicCurve.diagonalHom_injective

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in

Lean source · statement

theorem diagonalHom_injective [Nonempty (Place K F)] :
    Function.Injective (diagonalHom K F)

theorem

diagonal_mem_adeleBdd_iff

L105 ↗

AlgebraicCurve.diagonal_mem_adeleBdd_iff

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in

Lean source · statement

theorem diagonal_mem_adeleBdd_iff {f : F} :
    diagonalHom K F f ∈ adeleBdd D ↔ f ∈ LSpace D

def

adeleSpace

L111 ↗

AlgebraicCurve.adeleSpace

Documentation

The union of the submodules bounded by divisors.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in

Lean source · statement

def adeleSpace : Submodule K (Place K F → F)

theorem

adeleBdd_le_adeleSpace

L113 ↗

AlgebraicCurve.adeleBdd_le_adeleSpace

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in

Lean source · statement

theorem adeleBdd_le_adeleSpace : adeleBdd D ≤ adeleSpace K F

theorem

diagonal_mem_adeleSpace

L115 ↗

AlgebraicCurve.diagonal_mem_adeleSpace

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in

Lean source · statement

theorem diagonal_mem_adeleSpace [HasPrincipalDivisors K F] (f : F) :
    diagonalHom K F f ∈ adeleSpace K F

def

globalSub

L128 ↗

AlgebraicCurve.globalSub

Documentation

The submodule of constant families arising from global functions.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in

Lean source · statement

def globalSub : Submodule K (Place K F → F)

theorem

diagonal_mem_globalSub

L130 ↗

AlgebraicCurve.diagonal_mem_globalSub

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in

Lean source · statement

theorem diagonal_mem_globalSub (f : F) : diagonalHom K F f ∈ globalSub K F

theorem

map_diagonal_lSpace

L133 ↗

AlgebraicCurve.map_diagonal_lSpace

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in

Lean source · statement

theorem map_diagonal_lSpace (D : Divisor K F) :
    (LSpace D).map (diagonalHom K F) = adeleBdd D ⊓ globalSub K F

def

lSpaceEquivAdeleBddInfGlobal

L145 ↗

AlgebraicCurve.lSpaceEquivAdeleBddInfGlobal

Documentation

Identify bounded global families with the corresponding Riemann--Roch space.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in

Lean source · statement

def lSpaceEquivAdeleBddInfGlobal [Nonempty (Place K F)] (D : Divisor K F) :
    LSpace D ≃ₗ[K] (adeleBdd D ⊓ globalSub K F : Submodule K (Place K F → F))

theorem

finrank_adeleBdd_inf_global_eq_ell

L150 ↗

AlgebraicCurve.finrank_adeleBdd_inf_global_eq_ell

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in

Lean source · statement

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

def

indexOfSpecialty

L155 ↗

AlgebraicCurve.indexOfSpecialty

Documentation

The dimension of the adelic quotient by bounded families and global functions.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in

Lean source · statement

def indexOfSpecialty (D : Divisor K F) : ℕ

theorem

adeleBdd_directed

L161 ↗

AlgebraicCurve.adeleBdd_directed

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in

Lean source · statement

theorem adeleBdd_directed :
    Directed (· ≤ ·) (adeleBdd (K := K) (F := F))

theorem

mem_adeleSpace_iff

L165 ↗

AlgebraicCurve.mem_adeleSpace_iff

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in

Lean source · statement

theorem mem_adeleSpace_iff {α : Place K F → F} :
    α ∈ adeleSpace K F ↔ ∃ D : Divisor K F, α ∈ adeleBdd D

abbrev

adeleBddPrincipal

L172 ↗

AlgebraicCurve.adeleBddPrincipal

Documentation

The sum of bounded families and global functions inside the adelic space.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in

Lean source · statement

abbrev adeleBddPrincipal (D : Divisor K F) : Submodule K (adeleSpace K F)

theorem

indexOfSpecialty_eq

L176 ↗

AlgebraicCurve.indexOfSpecialty_eq

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in

Lean source · statement

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

def

omegaSpace

L180 ↗

AlgebraicCurve.omegaSpace

Documentation

The annihilator of bounded families and global functions in the adelic dual.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in

Lean source · statement

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

theorem

omegaSpace_vanishBdd

L183 ↗

AlgebraicCurve.omegaSpace_vanishBdd

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in

Lean source · statement

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

theorem

omegaSpace_vanishGlobal

L188 ↗

AlgebraicCurve.omegaSpace_vanishGlobal

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in

Lean source · statement

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

theorem

omegaSpace_antitone

L193 ↗

AlgebraicCurve.omegaSpace_antitone

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in

Lean source · statement

theorem omegaSpace_antitone {D E : Divisor K F} (hDE : D ≤ E) :
    omegaSpace E ≤ omegaSpace D

def

omegaSpaceEquivIndexDual

L199 ↗

AlgebraicCurve.omegaSpaceEquivIndexDual

Documentation

Identify the annihilator with the dual of the corresponding adelic quotient.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in

Lean source · statement

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

theorem

finrank_omegaSpace_eq_indexOfSpecialty

L203 ↗

AlgebraicCurve.finrank_omegaSpace_eq_indexOfSpecialty

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in

Lean source · statement

theorem finrank_omegaSpace_eq_indexOfSpecialty (D : Divisor K F) :
    Module.finrank K (omegaSpace D) = indexOfSpecialty D

def

weilDifferentialModule

L210 ↗

AlgebraicCurve.weilDifferentialModule

Documentation

The union of the differential spaces bounded by divisors.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in

Lean source · statement

def weilDifferentialModule : Submodule K (Module.Dual K (adeleSpace K F))

theorem

omegaSpace_le_weilDifferentialModule

L213 ↗

AlgebraicCurve.omegaSpace_le_weilDifferentialModule

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in

Lean source · statement

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

theorem

omegaSpace_directed

L216 ↗

AlgebraicCurve.omegaSpace_directed

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in

Lean source · statement

theorem omegaSpace_directed :
    Directed (· ≤ ·) (omegaSpace (K := K) (F := F))

theorem

mem_weilDifferentialModule_iff

L220 ↗

AlgebraicCurve.mem_weilDifferentialModule_iff

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in

Lean source · statement

theorem mem_weilDifferentialModule_iff {φ : Module.Dual K (adeleSpace K F)} :
    φ ∈ weilDifferentialModule K F ↔ ∃ D : Divisor K F, φ ∈ omegaSpace D

def

mulAdele

L227 ↗

AlgebraicCurve.mulAdele

Documentation

The linear map multiplying every component of a family by a fixed function.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K) in

Lean source · full declaration

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

theorem

mulAdele_apply

L233 ↗

AlgebraicCurve.mulAdele_apply

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K) in

Lean source · statement

theorem mulAdele_apply (f : F) (α : Place K F → F) (v : Place K F) :
    mulAdele K f α v = f * α v

theorem

mulAdele_one

L236 ↗

AlgebraicCurve.mulAdele_one

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K) in

Lean source · statement

theorem mulAdele_one : mulAdele K (1 : F) = LinearMap.id

theorem

mulAdele_mul

L239 ↗

AlgebraicCurve.mulAdele_mul

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K) in

Lean source · statement

theorem mulAdele_mul (f g : F) :
    mulAdele K (f * g) = (mulAdele K f).comp (mulAdele K g)

theorem

mulAdele_mem_adeleBdd_sub

L243 ↗

AlgebraicCurve.mulAdele_mem_adeleBdd_sub

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K) in

Lean source · statement

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)

theorem

mulAdele_globalSub_le

L254 ↗

AlgebraicCurve.mulAdele_globalSub_le

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K) in

Lean source · statement

theorem mulAdele_globalSub_le (f : F) :
    (globalSub K F).map (mulAdele K f) ≤ globalSub K F

theorem

mulAdele_mem_adeleSpace

L259 ↗

AlgebraicCurve.mulAdele_mem_adeleSpace

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K) in

Lean source · statement

theorem mulAdele_mem_adeleSpace [HasPrincipalDivisors K F] (f : F) {α : Place K F → F}
    (hα : α ∈ adeleSpace K F) : mulAdele K f α ∈ adeleSpace K F

def

adeleSpaceMul

L270 ↗

AlgebraicCurve.adeleSpaceMul

Documentation

Componentwise multiplication by a function restricted to the adelic space.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K) in
variable (K F) in

Lean source · statement

def adeleSpaceMul [HasPrincipalDivisors K F] (f : F) :
    adeleSpace K F →ₗ[K] adeleSpace K F

theorem

adeleSpaceMul_coe

L274 ↗

AlgebraicCurve.adeleSpaceMul_coe

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K) in
variable (K F) in

Lean source · statement

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)

def

weilSmul

L279 ↗

AlgebraicCurve.weilSmul

Documentation

The action of a function on the adelic dual by precomposition with multiplication.

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K) in
variable (K F) in
variable (K F) in

Lean source · statement

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

theorem

weilSmul_apply

L283 ↗

AlgebraicCurve.weilSmul_apply

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K) in
variable (K F) in
variable (K F) in

Lean source · statement

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 α)

theorem

adeleSpaceMul_one

L287 ↗

AlgebraicCurve.adeleSpaceMul_one

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K) in
variable (K F) in
variable (K F) in

Lean source · statement

theorem adeleSpaceMul_one [HasPrincipalDivisors K F] :
    adeleSpaceMul K F (1 : F) = LinearMap.id

theorem

adeleSpaceMul_mul

L293 ↗

AlgebraicCurve.adeleSpaceMul_mul

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K) in
variable (K F) in
variable (K F) in

Lean source · statement

theorem adeleSpaceMul_mul [HasPrincipalDivisors K F] (f g : F) :
    adeleSpaceMul K F (f * g) = (adeleSpaceMul K F f).comp (adeleSpaceMul K F g)

theorem

weilSmul_one

L299 ↗

AlgebraicCurve.weilSmul_one

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K) in
variable (K F) in
variable (K F) in

Lean source · statement

theorem weilSmul_one [HasPrincipalDivisors K F] :
    weilSmul K F (1 : F) = LinearMap.id

theorem

weilSmul_mul

L303 ↗

AlgebraicCurve.weilSmul_mul

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K) in
variable (K F) in
variable (K F) in

Lean source · statement

theorem weilSmul_mul [HasPrincipalDivisors K F] (f g : F) :
    weilSmul K F (f * g) = (weilSmul K F g).comp (weilSmul K F f)

theorem

weilSmul_injective

L307 ↗

AlgebraicCurve.weilSmul_injective

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K) in
variable (K F) in
variable (K F) in

Lean source · statement

theorem weilSmul_injective [HasPrincipalDivisors K F] {f : F} (hf : f ≠ 0) :
    Function.Injective (weilSmul K F f)

theorem

weilSmul_mem_omegaSpace_add

L314 ↗

AlgebraicCurve.weilSmul_mem_omegaSpace_add

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K) in
variable (K F) in
variable (K F) in

Lean source · statement

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)

theorem

weilSmul_mem_omegaSpace_of_mem_lSpace

L330 ↗

AlgebraicCurve.weilSmul_mem_omegaSpace_of_mem_lSpace

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K) in
variable (K F) in
variable (K F) in

Lean source · statement

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

def

residuePairing

L352 ↗

AlgebraicCurve.residuePairing

Documentation

Pair a bounded function with a Weil differential to obtain a bounded differential.

Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K) in
variable (K F) in
variable (K F) in
variable (K F) in

Lean source · full declaration

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 ?_
    change 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 ?_
    change 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)

theorem

residuePairing_apply_coe

L370 ↗

AlgebraicCurve.residuePairing_apply_coe

Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K) in
variable (K F) in
variable (K F) in
variable (K F) in

Lean source · statement

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) φ

theorem

residuePairing_injective

L375 ↗

AlgebraicCurve.residuePairing_injective

Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K) in
variable (K F) in
variable (K F) in
variable (K F) in

Lean source · statement

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φ)

theorem

ell_sub_le_indexOfSpecialty

L395 ↗

AlgebraicCurve.ell_sub_le_indexOfSpecialty

Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K) in
variable (K F) in
variable (K F) in
variable (K F) in

Lean source · statement

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

def

WeilDifferentialRankOne

L405 ↗

AlgebraicCurve.WeilDifferentialRankOne

Documentation

Every nonzero Weil differential uniquely generates all Weil differentials by functions.

Source context 16 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F)

Lean source · statement

def WeilDifferentialRankOne [HasPrincipalDivisors K F] : Prop

def

HasWeilCanonicalDivisor

L411 ↗

AlgebraicCurve.HasWeilCanonicalDivisor

Documentation

Every nonzero Weil differential has a largest divisor bound.

Source context 16 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F)

Lean source · statement

def HasWeilCanonicalDivisor : Prop

structure

RiemannGenusReachedAt

L418 ↗

AlgebraicCurve.RiemannGenusReachedAt

Documentation

A divisor attains the maximal degree-minus-dimension value specified by a genus.

Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F)
variable {K F}

Lean source · full declaration

structure RiemannGenusReachedAt (γ : ℤ) (D₀ : Divisor K F) : Prop where
  /-- The Riemann--Roch space of the attaining divisor is finite-dimensional. -/
  finite : FiniteDimensional K (LSpace D₀)
  /-- The attaining divisor has degree minus dimension equal to the genus minus one. -/
  eq : Divisor.degree D₀ - (ell D₀ : ℤ) = γ - 1
  /-- All divisors satisfy the same upper bound for degree minus dimension. -/
  isMax : ∀ D : Divisor K F, Divisor.degree D - (ell D : ℤ) ≤ γ - 1

def

RiemannGenusReached

L428 ↗

AlgebraicCurve.RiemannGenusReached

Documentation

The genus bound is attained and the zero-divisor space is finite-dimensional.

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F)
variable {K F}
variable (K F) in

Lean source · statement

def RiemannGenusReached (γ : ℤ) : Prop

def

StichtenothGenusExists

L434 ↗

AlgebraicCurve.StichtenothGenusExists

Documentation

Some integer genus bound is attained, with a finite-dimensional zero-divisor space.

Source context 19 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F)
variable {K F}
variable (K F) in
variable (K F) in

Lean source · statement

def StichtenothGenusExists : Prop

def

RiemannGenusBounded

L440 ↗

AlgebraicCurve.RiemannGenusBounded

Documentation

Degree minus Riemann--Roch dimension is bounded above over all divisors.

Source context 20 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F)
variable {K F}
variable (K F) in
variable (K F) in
variable (K F) in

Lean source · statement

def RiemannGenusBounded : Prop

def

IndexOfSpecialtyFinite

L445 ↗

AlgebraicCurve.IndexOfSpecialtyFinite

Documentation

Some bounded adelic quotient is a finite module over the base field.

Source context 21 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain WithZero Module
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D E : Divisor K F}
variable {D E : Divisor K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K) in
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F)
variable {K F}
variable (K F) in
variable (K F) in
variable (K F) in
variable (K F) in

Lean source · statement

def IndexOfSpecialtyFinite : Prop

Module documentation

Declarations