Residues at rational places define evaluation of functions and products along divisors, together with the Weil reciprocity condition.
The residue field of the place is generated by the base field.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)def IsRational : PropSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)theorem algebraMap_residueField_injective :
Function.Injective (algebraMap K v.ResidueField)An inverse function for the map from the base field to the residue field.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)def residueInv : v.ResidueField → KSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)theorem algebraMap_residueInv (hv : v.IsRational) (x : v.ResidueField) :
algebraMap K v.ResidueField (v.residueInv x) = xSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)theorem residueInv_algebraMap (a : K) : v.residueInv (algebraMap K v.ResidueField a) = aResidue evaluation at an integral function, with value zero outside the valuation subring.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
open Classical indef evalAt (f : F) : KSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)theorem evalAt_of_mem {f : F} (hf : f ∈ v.toValuationSubring) :
v.evalAt f = v.residueInv (residue v.toValuationSubring ⟨f, hf⟩)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)theorem algebraMap_evalAt (hv : v.IsRational) {f : F} (hf : f ∈ v.toValuationSubring) :
algebraMap K v.ResidueField (v.evalAt f)
= residue v.toValuationSubring (⟨f, hf⟩ : v.toValuationSubring)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)theorem evalAt_one : v.evalAt (1 : F) = 1The product of residue evaluations with exponents given by the divisor coefficients.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Divisordef evalFun (f : F) (D : Divisor K F) : KSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Divisortheorem evalFun_def (f : F) (D : Divisor K F) :
evalFun f D = ∏ v ∈ D.support, v.evalAt f ^ D vSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Divisortheorem evalFun_zero (f : F) : evalFun f (0 : Divisor K F) = 1Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Divisortheorem evalFun_single (f : F) (v : Place K F) (n : ℤ) :
evalFun f (Finsupp.single v n) = v.evalAt f ^ nThe equality of divisor evaluations for two nonzero functions with disjoint divisors.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) indef WeilReciprocity : Prop