Nonvanishing of the value at a rational place of a function of order zero #
Theorem statement: AlgebraicCurve.Place.evalAt_ne_zero (9189b191-17b0-53c0-9c16-e7bdb3ea4356),
by Claude, 2026-09-05.
Proof: submission ca31e76d-fe15-55fc-8317-e7055379da18, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $K$ and $F$ be fields with $F$ a $K$-algebra, and let $v$ be a place of $F$ over $K$, i.e. a
valuation subring $\mathcal{O}_v =$ v.toValuationSubring of $F$ which contains the image of $K$
under the structure map, is not all of $F$, and is a principal ideal ring. Assume $v$ is rational in
the sense of the predicate IsRational, namely that the induced map from $K$ to the residue field
$\mathcal{O}_v/\mathfrak{m}_v$ is surjective. Let $f \in F$ be nonzero and suppose that
$\operatorname{ord}_v(f) = 0$, where $\operatorname{ord}_v(f)$ is minus the logarithm of the value
of $f$ under the valuation attached to the height one prime of $\mathcal{O}_v$. Then the value
$\operatorname{evalAt}_v(f) \in K$ is nonzero, where $\operatorname{evalAt}_v(f)$ is defined to be a
chosen preimage in $K$, under the map $K \to \mathcal{O}_v/\mathfrak{m}_v$, of the residue class of
$f$ when $f \in \mathcal{O}_v$, and $0$ otherwise (so that the value is, in particular, a genuine
preimage exactly when $v$ is rational and $f$ lies in $\mathcal{O}_v$).
This is the statement that a nonzero function with neither a zero nor a pole at a rational place has
nonzero value there; equivalently, a nonzero element of order zero is a unit of the local ring and
so has nonzero residue. It underlies the evaluation of functions at divisors, $f(D) = \prod_v f(v)^{D(v)}$, being nonzero when the divisor avoids the support of $\operatorname{div} f$, and is
used throughout the evaluation-at-divisors layer, for instance by
[AlgebraicCurve.Divisor.evalFun_algebraMap_pushforward]
(thm.html#AlgebraicCurve.Divisor.evalFun_algebraMap_pushforward).
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_AlgebraicCurve_Place_evalAt_ne_zero.lean
<!-- Generated by add_prove2me_provenance.py -->