Evaluation at rational places and divisors; Weil reciprocity predicate #
Definition: AlgebraicCurve_PlaceEvaluation (d5fccec9-c50a-5b0f-9eb1-08b6be4c96f8), by Claude,
2026-09-05.
The setting is a field extension $K \subseteq F$ (an algebra $F$ over a field $K$, with $F$ a
field), with places, orders and divisors as in the divisor-class-group module: a Place K F is a
valuation subring $\mathcal O_v \subseteq F$ containing the image of $K$, different from $F$ and
with principal ideals (hence a discrete valuation ring), $v.\mathrm{ord}$ is minus the logarithm of
the associated adic valuation, and a divisor is a finitely supported function from places to
$\mathbb Z$. Here a place $v$ is declared IsRational when the structure map $K \to \kappa(v)$ into
the residue field of $\mathcal O_v$ is surjective; since that map is automatically injective, this
says $\kappa(v) = K$, i.e. $\deg v = 1$. The map residueInv is a chosen left inverse of $K \to \kappa(v)$ (the Function.invFun, so it is a genuine inverse exactly when $v$ is rational, and
arbitrary elsewhere), and evalAt sends $f \in F$ to residueInv of the residue class of $f$ when
$f \in \mathcal O_v$, and to $0$ otherwise; thus $f(v) \in K$ is the value of $f$ at $v$ when $v$ is
rational and $f$ has no pole there, with the junk value $0$ at poles. The accompanying lemmas record
the two inversion identities, the defining equation of evalAt on $\mathcal O_v$, the fact that $K \to \kappa(v)$ carries $f(v)$ to the residue of $f$ when $v$ is rational, and $1(v) = 1$.
For a divisor $D$, Divisor.evalFun f D is the finite product $\prod_{v \in \mathrm{supp}\,D} f(v)^{D(v)}$ of integer powers in $K$; it is $1$ on the zero divisor and equals $f(v)^n$ on $n \cdot v$. Finally WeilReciprocity K F is a predicate on the pair $(K,F)$, not a theorem: it asserts that
for all nonzero $f, g \in F$ and all divisors $D_f, D_g$ with $D_f(v) = \mathrm{ord}_v f$ and
$D_g(v) = \mathrm{ord}_v g$ at every place, such that at each place at least one of $\mathrm{ord}_v f$, $\mathrm{ord}_v g$ vanishes and such that every place in the support of $D_f$ or of $D_g$ is
rational, one has $f(D_g) = g(D_f)$.
Relation to Mathlib. Built on Mathlib's ValuationSubring and IsLocalRing.ResidueField, with
residueInv obtained from Function.invFun; the evaluation of a function at a place or at a
divisor, and the Weil reciprocity statement, are the project's own, Mathlib having no such notions.
Where it is used. These definitions underlie the project's treatment of Weil reciprocity for function fields and, through it, the divisor-class description of the Weil pairing $e_n(D_1,D_2) = f_1(D_2)/f_2(D_1)$ on elliptic curves, which feeds into the study of the mod $n$ Galois representations used on the Frey-curve side of the argument.
<!-- Generated by add_prove2me_provenance.py -->
The constant field maps surjectively onto the residue field at the place.
Equations
- v.IsRational = Function.Surjective ⇑(algebraMap K v.ResidueField)
Instances For
A chosen inverse on the image of the constant field in the residue field, used at rational places.
Equations
- v.residueInv = Function.invFun ⇑(algebraMap K v.ResidueField)
Instances For
Evaluation by residue followed by residueInv, with value zero outside the valuation ring.
Equations
- v.evalAt f = if hf : f ∈ v.toValuationSubring then v.residueInv ((IsLocalRing.residue ↥v.toValuationSubring) ⟨f, hf⟩) else 0
Instances For
Evaluation of a function on a divisor, multiplying its values with the divisor's integer exponents.
Equations
- AlgebraicCurve.Divisor.evalFun f D = Finsupp.prod D fun (v : AlgebraicCurve.Place K F) (n : ℤ) => v.evalAt f ^ n