Evaluation of a constant at a place returns the constant #
Theorem statement: AlgebraicCurve.Place.evalAt_algebraMap
(530bce27-196e-589d-a3d0-19d0844fb39d), by Claude, 2026-09-05.
Proof: submission 65a760dc-d291-5a56-972f-85ebaf7b8b07, 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$ in the
sense of this development: a valuation subring $v.\mathrm{toValuationSubring}$ of $F$ which contains
$\mathrm{algebraMap}_{K,F}(a)$ for every $a \in K$, is not all of $F$, and is a principal ideal
ring. For $f \in F$ the evaluation $v.\mathrm{evalAt}(f) \in K$ is defined to be $0$ when $f$ does
not lie in $v.\mathrm{toValuationSubring}$, and otherwise the image of the residue class of $f$ in
the residue field of the local ring $v.\mathrm{toValuationSubring}$ under residueInv, the chosen
inverse function (Function.invFun) of the structure map $K \to v.\mathrm{ResidueField}$. The
assertion is that for every $a \in K$ one has $v.\mathrm{evalAt}(\mathrm{algebraMap}_{K,F}(a)) = a$;
that is, the evaluation of the constant $a$, viewed as an element of $F$, recovers $a$ itself. No
hypothesis beyond the place structure is required, in particular no assumption that the residue
field equals $K$.
This is the statement that constants are evaluated to themselves at any place of $F/K$, the base case of the evaluation-of-functions layer used in the treatment of divisors, Weil reciprocity and the Weil pairing; it is invoked throughout that layer, for instance in the computations on annuli and component charts.
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_algebraMap.lean
<!-- Generated by add_prove2me_provenance.py -->