NYLL
Module

Basic.lean

Nyll.AlgebraicCurves.Differentials.Residues.Basic
36 declarations indexed from sourceView source ↗

Module documentation

Differentials, residues, and divisor correspondences

Local residue data, traced differential residues, and residue functionals on adeles.

Imports3
Imported by46

Declarations

structure

LocalResidueData

L37 ↗
AlgebraicCurve.Place.LocalResidueData
Documentation

A linear local residue map that vanishes on integral functions and computes residues of simple poles.

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
Lean source · full declaration
structure LocalResidueData where
  /-- The local residue map to the residue field. -/
  res : F →ₗ[K] v.ResidueField
  /-- Integral functions have zero local residue. -/
  res_of_mem : ∀ f : F, f ∈ v.toValuationSubring → res f = 0
  /-- For a simple pole, the residue is the reduction of the product with the uniformizer. -/
  res_simplePole : ∀ (f : F) (hf : v.uniformizer * f ∈ v.toValuationSubring),
    res f = IsLocalRing.residue _ ⟨v.uniformizer * f, hf⟩
structure

CanonicalLocalResidueDataK

L47 ↗
AlgebraicCurve.Place.CanonicalLocalResidueDataK
Documentation

Local residue data whose higher inverse uniformizer monomials have zero residue.

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
Lean source · full declaration
structure CanonicalLocalResidueDataK extends v.LocalResidueData where
  /-- Inverse uniformizer powers of pole order at least two have zero residue. -/
  res_higherPoleMonomial : ∀ (n : ℕ), 1 ≤ n → res (v.uniformizer ^ (n + 1))⁻¹ = 0
class

HasLocalResidue

L55 ↗
AlgebraicCurve.HasLocalResidue
Documentation

Local residue data exists at every place.

Source context 5 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
Lean source · full declaration
class HasLocalResidue : Prop where
  /-- Every place admits a local residue map with the prescribed integral and simple-pole
  laws. -/
  exists_data : ∀ v : Place K F, Nonempty v.LocalResidueData
class

HasCanonicalLocalResidueK

L62 ↗
AlgebraicCurve.HasCanonicalLocalResidueK
Documentation

Canonical local residue data exists at every place.

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
Lean source · full declaration
class HasCanonicalLocalResidueK : Prop where
  /-- Every place admits canonical local residue data. -/
  exists_data : ∀ v : Place K F, Nonempty v.CanonicalLocalResidueDataK
instance

instHasLocalResidue_of_hasCanonicalLocalResidueK

L66 ↗
AlgebraicCurve.instHasLocalResidue_of_hasCanonicalLocalResidueK
Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
Lean source · statement
instance (priority := 100) instHasLocalResidue_of_hasCanonicalLocalResidueK
    [HasCanonicalLocalResidueK K F] : HasLocalResidue K F
class

HasCanonicalLocalResidueKStar

L72 ↗
AlgebraicCurve.HasCanonicalLocalResidueKStar
Documentation

A specified family of canonical local residue maps at all places.

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
Lean source · full declaration
class HasCanonicalLocalResidueKStar where
  /-- The canonical local residue data chosen for each place. -/
  dataKStar : ∀ v : Place K F, v.CanonicalLocalResidueDataK
instance

instHasCanonicalLocalResidueK_of_hasCanonicalLocalResidueKStar

L76 ↗
AlgebraicCurve.instHasCanonicalLocalResidueK_of_hasCanonicalLocalResidueKStar
Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
Lean source · statement
instance (priority := 100) instHasCanonicalLocalResidueK_of_hasCanonicalLocalResidueKStar
    [HasCanonicalLocalResidueKStar K F] : HasCanonicalLocalResidueK K F
theorem

mem_of_ord_nonneg_localResidueAux

L84 ↗
AlgebraicCurve.Place.mem_of_ord_nonneg_localResidueAux
Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
namespace Place
variable (v : Place K F)
Lean source · statement
theorem mem_of_ord_nonneg_localResidueAux {f : F} (hf : f ≠ 0) (h : 0 ≤ v.ord f) :
    f ∈ v.toValuationSubring
def

localResidue

L93 ↗
AlgebraicCurve.Place.localResidue
Documentation

The local residue map from the specified canonical residue family.

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
namespace Place
variable (v : Place K F)
Lean source · statement
def localResidue [HasCanonicalLocalResidueKStar K F] :
    F →ₗ[K] v.ResidueField
theorem

localResidue_of_mem

L97 ↗
AlgebraicCurve.Place.localResidue_of_mem
Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
namespace Place
variable (v : Place K F)
Lean source · statement
theorem localResidue_of_mem [HasCanonicalLocalResidueKStar K F] {f : F}
    (hf : f ∈ v.toValuationSubring) :
    v.localResidue f = 0
theorem

localResidue_simplePole

L102 ↗
AlgebraicCurve.Place.localResidue_simplePole
Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
namespace Place
variable (v : Place K F)
Lean source · statement
theorem localResidue_simplePole [HasCanonicalLocalResidueKStar K F] (f : F)
    (hf : v.uniformizer * f ∈ v.toValuationSubring) :
    v.localResidue f = IsLocalRing.residue _ ⟨v.uniformizer * f, hf⟩
theorem

localResidue_higherPoleMonomial

L107 ↗
AlgebraicCurve.Place.localResidue_higherPoleMonomial
Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
namespace Place
variable (v : Place K F)
Lean source · statement
theorem localResidue_higherPoleMonomial [HasCanonicalLocalResidueKStar K F]
    (n : ℕ) (hn : 1 ≤ n) :
    v.localResidue (v.uniformizer ^ (n + 1))⁻¹ = 0
theorem

localResidue_eq_zero_of_ord_nonneg

L112 ↗
AlgebraicCurve.Place.localResidue_eq_zero_of_ord_nonneg
Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
namespace Place
variable (v : Place K F)
Lean source · statement
theorem localResidue_eq_zero_of_ord_nonneg [HasCanonicalLocalResidueKStar K F] {f : F}
    (hf : f = 0 ∨ 0 ≤ v.ord f) : v.localResidue f = 0
theorem

gate_localResidue_uniformizer_inv

L120 ↗
AlgebraicCurve.Place.gate_localResidue_uniformizer_inv
Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
namespace Place
variable (v : Place K F)
Lean source · statement
theorem gate_localResidue_uniformizer_inv [HasCanonicalLocalResidueKStar K F] :
    v.localResidue v.uniformizer⁻¹ = 1
def

kaehlerResidueTerm

L135 ↗
AlgebraicCurve.kaehlerResidueTerm
Documentation

The base-field trace of the local residue of the function times the differential coefficient.

Source context 8 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
variable [HasCanonicalLocalResidueKStar K F]
Lean source · statement
def kaehlerResidueTerm (ω : Ω[F⁄K]) (α : Place K F → F) (v : Place K F) : K
theorem

kaehlerResidueTerm_eq_zero_of_ord_nonneg

L138 ↗
AlgebraicCurve.kaehlerResidueTerm_eq_zero_of_ord_nonneg
Source context 8 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
variable [HasCanonicalLocalResidueKStar K F]
Lean source · statement
theorem kaehlerResidueTerm_eq_zero_of_ord_nonneg {ω : Ω[F⁄K]} {α : Place K F → F}
    {v : Place K F} (h : α v * v.differentialCoeff ω = 0 ∨
      0 ≤ v.ord (α v * v.differentialCoeff ω)) :
    kaehlerResidueTerm ω α v = 0
theorem

differentialCoeff_ne_zero

L146 ↗
AlgebraicCurve.Place.differentialCoeff_ne_zero
Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
variable [HasCanonicalLocalResidueKStar K F]
omit [HasCanonicalLocalResidueKStar K F] in
Lean source · statement
theorem Place.differentialCoeff_ne_zero (v : Place K F) [v.DCoordGenerates]
    {ω : Ω[F⁄K]} (hω : ω ≠ 0) : v.differentialCoeff ω ≠ 0
theorem

res_eq_zero_of_ord_nonneg

L153 ↗
AlgebraicCurve.Place.LocalResidueData.res_eq_zero_of_ord_nonneg
Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
variable [HasCanonicalLocalResidueKStar K F]
namespace Place
omit [HasCanonicalLocalResidueKStar K F] in
Lean source · statement
theorem LocalResidueData.res_eq_zero_of_ord_nonneg {v : Place K F} (R : v.LocalResidueData)
    {f : F} (hf : f = 0 ∨ 0 ≤ v.ord f) : R.res f = 0
theorem

res_eq_zero_of_ord_nonneg

L162 ↗
AlgebraicCurve.Place.CanonicalLocalResidueDataK.res_eq_zero_of_ord_nonneg
Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
variable [HasCanonicalLocalResidueKStar K F]
namespace Place
omit [HasCanonicalLocalResidueKStar K F] in
Lean source · statement
theorem CanonicalLocalResidueDataK.res_eq_zero_of_ord_nonneg {v : Place K F}
    (R : v.CanonicalLocalResidueDataK) {f : F} (hf : f = 0 ∨ 0 ≤ v.ord f) : R.res f = 0
theorem

single_mem_adeleBdd

L172 ↗
AlgebraicCurve.single_mem_adeleBdd
Source context 11 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
variable [HasCanonicalLocalResidueKStar K F]
section Single
open scoped Classical in
omit [HasCanonicalLocalResidueKStar K F] in
Lean source · statement
theorem single_mem_adeleBdd (v : Place K F) (g : F) (D : Divisor K F)
    (hg : v.adicValuation g ≤ WithZero.exp (D v)) :
    Pi.single v g ∈ adeleBdd D
theorem

single_mem_adeleSpace

L182 ↗
AlgebraicCurve.single_mem_adeleSpace
Source context 11 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
variable [HasCanonicalLocalResidueKStar K F]
section Single
open scoped Classical in
omit [HasCanonicalLocalResidueKStar K F] in
Lean source · statement
theorem single_mem_adeleSpace (v : Place K F) (g : F) :
    Pi.single v g ∈ adeleSpace K F
def

adeleSingle

L192 ↗
AlgebraicCurve.adeleSingle
Documentation

The adele supported at the specified place with the specified function value.

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
variable [HasCanonicalLocalResidueKStar K F]
section Single
open scoped Classical in
Lean source · statement
def adeleSingle (v : Place K F) (g : F) : adeleSpace K F
theorem

adeleSingle_coe

L198 ↗
AlgebraicCurve.adeleSingle_coe
Source context 11 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
variable [HasCanonicalLocalResidueKStar K F]
section Single
open scoped Classical in
omit [HasCanonicalLocalResidueKStar K F] in
Lean source · statement
theorem adeleSingle_coe (v : Place K F) (g : F) :
    (adeleSingle v g : Place K F → F) = Pi.single v g
class

HasSeparableResidue

L205 ↗
AlgebraicCurve.HasSeparableResidue
Documentation

The residue-field trace to the base field is nonzero at every place.

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
variable [HasCanonicalLocalResidueKStar K F]
variable (K F) in
Lean source · full declaration
class HasSeparableResidue : Prop where
  /-- Every residue-field trace is a nonzero linear map. -/
  trace_ne_zero : ∀ v : Place K F, (Algebra.trace K v.ResidueField : _ →ₗ[K] K) ≠ 0
def

kaehlerResidueTermK

L215 ↗
AlgebraicCurve.Place.kaehlerResidueTermK
Documentation

The traced residue of a function times the differential coefficient, using explicit local residue data.

Source context 11 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
variable [HasCanonicalLocalResidueKStar K F]
variable (K F) in
section CanonicalKResidueTerm
variable {K F : Type*} [Field K] [Field F] [Algebra K F] [HasCanonicalLocalResidueKStar K F]
Lean source · statement
def Place.kaehlerResidueTermK (v : Place K F) (R : v.CanonicalLocalResidueDataK)
    (ω : Ω[F⁄K]) (f : F) : K
def

kaehlerResidueTermKFam

L220 ↗
AlgebraicCurve.kaehlerResidueTermKFam
Documentation

The traced residue term using an explicit family of local residue data.

Source context 11 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
variable [HasCanonicalLocalResidueKStar K F]
variable (K F) in
section CanonicalKResidueTerm
variable {K F : Type*} [Field K] [Field F] [Algebra K F] [HasCanonicalLocalResidueKStar K F]
Lean source · statement
def kaehlerResidueTermKFam (Rfam : ∀ v : Place K F, v.CanonicalLocalResidueDataK)
    (ω : Ω[F⁄K]) (α : Place K F → F) (v : Place K F) : K
theorem

kaehlerResidueTermKFam_apply

L226 ↗
AlgebraicCurve.kaehlerResidueTermKFam_apply
Source context 12 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
variable [HasCanonicalLocalResidueKStar K F]
variable (K F) in
section CanonicalKResidueTerm
variable {K F : Type*} [Field K] [Field F] [Algebra K F] [HasCanonicalLocalResidueKStar K F]
omit [HasCanonicalLocalResidueKStar K F] in
Lean source · statement
theorem kaehlerResidueTermKFam_apply (Rfam : ∀ v : Place K F, v.CanonicalLocalResidueDataK)
    (ω : Ω[F⁄K]) (α : Place K F → F) (v : Place K F) :
    kaehlerResidueTermKFam Rfam ω α v
      = Algebra.trace K v.ResidueField ((Rfam v).res (α v * v.differentialCoeff ω))
theorem

kaehlerResidueTermKFam_eq_zero_of_ord_nonneg

L232 ↗
AlgebraicCurve.kaehlerResidueTermKFam_eq_zero_of_ord_nonneg
Source context 12 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
variable [HasCanonicalLocalResidueKStar K F]
variable (K F) in
section CanonicalKResidueTerm
variable {K F : Type*} [Field K] [Field F] [Algebra K F] [HasCanonicalLocalResidueKStar K F]
omit [HasCanonicalLocalResidueKStar K F] in
Lean source · statement
theorem kaehlerResidueTermKFam_eq_zero_of_ord_nonneg
    (Rfam : ∀ v : Place K F, v.CanonicalLocalResidueDataK) {ω : Ω[F⁄K]}
    {α : Place K F → F} {v : Place K F}
    (h : α v * v.differentialCoeff ω = 0 ∨ 0 ≤ v.ord (α v * v.differentialCoeff ω)) :
    kaehlerResidueTermKFam Rfam ω α v = 0
theorem

kaehlerResidueTermKFam_eq_zero_of_adeleBdd_canonical

L244 ↗
AlgebraicCurve.kaehlerResidueTermKFam_eq_zero_of_adeleBdd_canonical
Source context 14 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
variable [HasCanonicalLocalResidueKStar K F]
variable (K F) in
section CanonicalKResidueTerm
variable {K F : Type*} [Field K] [Field F] [Algebra K F] [HasCanonicalLocalResidueKStar K F]
section SupportMachinery
variable [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
omit [HasCanonicalLocalResidueKStar K F] in
Lean source · statement
theorem kaehlerResidueTermKFam_eq_zero_of_adeleBdd_canonical
    (Rfam : ∀ v : Place K F, v.CanonicalLocalResidueDataK) {ω : Ω[F⁄K]} (hω : ω ≠ 0)
    {α : Place K F → F} (hα : α ∈ adeleBdd (canonicalDivisorOf hω)) (v : Place K F) :
    kaehlerResidueTermKFam Rfam ω α v = 0
theorem

kaehlerResidueTermKFam_support_subset

L262 ↗
AlgebraicCurve.kaehlerResidueTermKFam_support_subset
Source context 14 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
variable [HasCanonicalLocalResidueKStar K F]
variable (K F) in
section CanonicalKResidueTerm
variable {K F : Type*} [Field K] [Field F] [Algebra K F] [HasCanonicalLocalResidueKStar K F]
section SupportMachinery
variable [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
omit [HasCanonicalLocalResidueKStar K F] in
Lean source · statement
theorem kaehlerResidueTermKFam_support_subset
    (Rfam : ∀ v : Place K F, v.CanonicalLocalResidueDataK) {ω : Ω[F⁄K]} (hω : ω ≠ 0)
    {D : Divisor K F} {α : Place K F → F} (hα : α ∈ adeleBdd D) :
    Function.support (kaehlerResidueTermKFam Rfam ω α)
      ⊆ ↑(D - canonicalDivisorOf hω).support
theorem

kaehlerResidueTermKFam_support_finite

L285 ↗
AlgebraicCurve.kaehlerResidueTermKFam_support_finite
Source context 14 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
variable [HasCanonicalLocalResidueKStar K F]
variable (K F) in
section CanonicalKResidueTerm
variable {K F : Type*} [Field K] [Field F] [Algebra K F] [HasCanonicalLocalResidueKStar K F]
section SupportMachinery
variable [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
omit [HasCanonicalLocalResidueKStar K F] in
Lean source · statement
theorem kaehlerResidueTermKFam_support_finite
    (Rfam : ∀ v : Place K F, v.CanonicalLocalResidueDataK) {ω : Ω[F⁄K]} (hω : ω ≠ 0)
    {D : Divisor K F} {α : Place K F → F} (hα : α ∈ adeleBdd D) :
    (Function.support (kaehlerResidueTermKFam Rfam ω α)).Finite
theorem

kaehlerResidueTermKFam_support_finite_of_adeleSpace

L293 ↗
AlgebraicCurve.kaehlerResidueTermKFam_support_finite_of_adeleSpace
Source context 14 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
variable [HasCanonicalLocalResidueKStar K F]
variable (K F) in
section CanonicalKResidueTerm
variable {K F : Type*} [Field K] [Field F] [Algebra K F] [HasCanonicalLocalResidueKStar K F]
section SupportMachinery
variable [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
omit [HasCanonicalLocalResidueKStar K F] in
Lean source · statement
theorem kaehlerResidueTermKFam_support_finite_of_adeleSpace
    (Rfam : ∀ v : Place K F, v.CanonicalLocalResidueDataK) {ω : Ω[F⁄K]} (hω : ω ≠ 0)
    {α : Place K F → F} (hα : α ∈ adeleSpace K F) :
    (Function.support (kaehlerResidueTermKFam Rfam ω α)).Finite
def

weilOfKaehlerK

L302 ↗
AlgebraicCurve.weilOfKaehlerK
Documentation

The adele linear functional obtained by summing residue terms from an explicit canonical residue family.

Source context 13 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
variable [HasCanonicalLocalResidueKStar K F]
variable (K F) in
section CanonicalKResidueTerm
variable {K F : Type*} [Field K] [Field F] [Algebra K F] [HasCanonicalLocalResidueKStar K F]
section SupportMachinery
variable [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
Lean source · full declaration
def weilOfKaehlerK (Rfam : ∀ v : Place K F, v.CanonicalLocalResidueDataK)
    {ω : Ω[F⁄K]} (hω : ω ≠ 0) : Module.Dual K (adeleSpace K F) where
  toFun α := ∑ᶠ v, kaehlerResidueTermKFam Rfam ω (α : Place K F → F) v
  map_add' α β := by
    have hsupα := kaehlerResidueTermKFam_support_finite_of_adeleSpace Rfam hω α.2
    have hsupβ := kaehlerResidueTermKFam_support_finite_of_adeleSpace Rfam hω β.2
    rw [← finsum_add_distrib hsupα hsupβ]
    refine finsum_congr fun v => ?_
    simp only [kaehlerResidueTermKFam_apply]
    rw [Submodule.coe_add, Pi.add_apply, add_mul, map_add, map_add]
  map_smul' c α := by
    simp only [RingHom.id_apply]
    rw [smul_finsum]
    refine finsum_congr fun v => ?_
    simp only [kaehlerResidueTermKFam_apply]
    rw [Submodule.coe_smul, Pi.smul_apply, Algebra.smul_def, mul_assoc,
      ← Algebra.smul_def, map_smul, map_smul]
theorem

weilOfKaehlerK_apply

L321 ↗
AlgebraicCurve.weilOfKaehlerK_apply
Source context 14 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
variable [HasCanonicalLocalResidueKStar K F]
variable (K F) in
section CanonicalKResidueTerm
variable {K F : Type*} [Field K] [Field F] [Algebra K F] [HasCanonicalLocalResidueKStar K F]
section SupportMachinery
variable [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
omit [HasCanonicalLocalResidueKStar K F] in
Lean source · statement
theorem weilOfKaehlerK_apply (Rfam : ∀ v : Place K F, v.CanonicalLocalResidueDataK)
    {ω : Ω[F⁄K]} (hω : ω ≠ 0) (α : adeleSpace K F) :
    weilOfKaehlerK Rfam hω α
      = ∑ᶠ v, kaehlerResidueTermKFam Rfam ω (α : Place K F → F) v
theorem

weilOfKaehlerK_vanish_adeleBdd_canonical

L327 ↗
AlgebraicCurve.weilOfKaehlerK_vanish_adeleBdd_canonical
Source context 14 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
variable [HasCanonicalLocalResidueKStar K F]
variable (K F) in
section CanonicalKResidueTerm
variable {K F : Type*} [Field K] [Field F] [Algebra K F] [HasCanonicalLocalResidueKStar K F]
section SupportMachinery
variable [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
omit [HasCanonicalLocalResidueKStar K F] in
Lean source · statement
theorem weilOfKaehlerK_vanish_adeleBdd_canonical
    (Rfam : ∀ v : Place K F, v.CanonicalLocalResidueDataK) {ω : Ω[F⁄K]} (hω : ω ≠ 0)
    {α : adeleSpace K F} (hα : (α : Place K F → F) ∈ adeleBdd (canonicalDivisorOf hω)) :
    weilOfKaehlerK Rfam hω α = 0
def

ResidueTheoremK

L339 ↗
AlgebraicCurve.ResidueTheoremK
Documentation

Every explicit canonical residue family gives a differential residue functional that vanishes on diagonal functions.

Source context 14 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
variable (K F) in
variable [HasCanonicalLocalResidueKStar K F]
variable (K F) in
section CanonicalKResidueTerm
variable {K F : Type*} [Field K] [Field F] [Algebra K F] [HasCanonicalLocalResidueKStar K F]
section SupportMachinery
variable [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
variable (K F)
Lean source · statement
def ResidueTheoremK : Prop

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.