Pushforward norm formula along a finite separable K-morphism #
Theorem statement: AlgebraicCurve.normFormulaAlong (0a836ca9-bde8-5a32-b34d-1f0bf43c2174), by
Claude, 2026-09-05.
Proof: submission 9c76cc3b-ad4f-5f4a-9873-dbbcc0897fb8, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $K$, $F$, $F'$ be fields, with $F$ and $F'$ algebras over $K$ and $F$ of characteristic zero,
and let $\varphi : F \to F'$ be a $K$-algebra homomorphism. Assume $F'$ has principal divisors over
$K$, i.e. every nonzero $f \in F'$ admits a divisor $D$ (a finitely supported $\mathbb{Z}$-valued
function on the places of $F'$ over $K$, a place being a valuation subring containing the image of
$K$, distinct from the whole field, and a principal ideal ring) with $D(w) = \operatorname{ord}_w f$
at every place $w$ and $\deg D = 0$. Assume further that, when $F'$ is regarded as an $F$-algebra
through $\varphi$, it is a finite $F$-module (FiniteAlong) and a separable $F$-algebra
(SeparableAlong). The conclusion is NormFormulaAlong K φ hfin, which unfolds to the assertion
that, with respect to this $F$-algebra structure on $F'$, for every nonzero $f \in F'$, every
divisor $D$ on $F'$ satisfying $D(w) = \operatorname{ord}_w f$ at all places $w$ of $F'$, and every
place $v$ of $F$, the pushforward of $D$ to the divisors of $F$ takes at $v$ the value
$\operatorname{ord}_v\bigl(N_{F'/F}(f)\bigr)$.
This is the compatibility of the divisor pushforward with the field norm, $\varphi_*(\operatorname{div} f) = \operatorname{div}(N_{F'/F} f)$, in the form required for a morphism of curves presented as an explicit $K$-algebra map rather than by an ambient tower of algebras. It supplies the norm-formula hypothesis used in the construction of correspondences and their action on Picard groups and Tate modules.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_AlgebraicCurve_normFormulaAlong.lean
<!-- Generated by add_prove2me_provenance.py -->