Divisor correspondences along explicit function-field embeddings #

Definition: AlgebraicCurve_Correspondence (3c0e42ff-ff90-5f68-a698-ffc9f304ba5a), by Claude, 2026-09-05.

Throughout, $K$ is a field and $F$, $F'$ are fields with $K$-algebra structures; all divisor-theoretic notions ($\mathrm{Place}\,K\,F$, $\mathrm{Divisor}\,K\,F$, $\mathrm{Pic}^0$, Place.restrict, ramification index, inertia degree, fibre, Divisor.pullback, Divisor.pushforward, and the hypothesis classes FundamentalIdentity, PushforwardNormFormula, HasPrincipalDivisors) are taken from the project's own earlier modules. The point of this module is to restate that calculus along an explicitly given $K$-algebra map $\varphi : F \to_{\mathrm{alg}[K]} F'$ rather than along an ambient [Algebra F F'] instance, so that two such maps between the same pair of fields can coexist. algebraAlong φ is the algebra structure $\varphi_*$ on $F'$ over $F$ obtained from the underlying ring homomorphism; it is an abbreviation, never an instance, and isScalarTower_along, isIntegral_along supply the tower and integrality facts for it. Against this the instance-free predicates FundamentalIdentityAlong K φ hφ, FiniteAlong K φ, NormFormulaAlong K φ hfin, SeparableAlong K φ and the number finrankAlong K φ are by definition the corresponding instance-form statements evaluated at algebraAlong φ (with integrality of $\varphi$ as a hypothesis hφ where needed), and Divisor.pullbackAlong φ hφ, Divisor.pushforwardAlong φ hφ are the group homomorphisms Divisor.pullback, Divisor.pushforward taken there.

For a pair $\varphi, \psi : F \to_{\mathrm{alg}[K]} F'$ of integral maps, Divisor.correspondence φ ψ hφ hψ is the additive endomorphism $\psi_* \circ \varphi^*$ of $\mathrm{Divisor}\,K\,F$: pull back along $\varphi$, push forward along $\psi$. Its degree satisfies $\deg = (\operatorname{finrankAlong} K\,\varphi)\cdot\deg$ under the fundamental identity along the pull-back leg; it preserves degree-zero divisors under the same hypothesis, and preserves principal divisors given finiteness and the norm formula along the push-forward leg. Combining these, Pic0.degZeroCorrespondence restricts it to degree-zero divisors and Pic0.correspondence φ ψ hφ hψ hFI hfin hN descends it to an additive endomorphism of $\mathrm{Pic}^0\,K\,F$; note the hypothesis split, the fundamental identity on $\varphi$ and finiteness plus norm formula on $\psi$. The remaining declarations are the place calculus along $\varphi$ (Place.restrictAlong, ramificationIndexAlong, inertiaDegAlong, fiberAlong, the valuation identity $\operatorname{ord}_w(\varphi f) = e_w \cdot \operatorname{ord}_{w|_F}(f)$, and the single-place formulas for pull-back and push-forward), plus SemilinearAut.IntertwinesAlong ι g g', the predicate $g'(\iota x) = \iota(g x)$ for all $x$, together with its closure under inversion, identity and multiplication.

Relation to Mathlib. algebraAlong is Mathlib's RingHom.toAlgebra applied to the underlying ring homomorphism, deliberately kept as a non-instance abbreviation; the divisor, place and $\mathrm{Pic}^0$ notions it is applied to, and the correspondence operator $\psi_*\circ\varphi^*$, are the project's own and have no Mathlib counterpart.

Where it is used. Applied to the two degeneracy maps of a modular curve, the correspondence $\psi_*\circ\varphi^*$ gives the Hecke operators acting on $J_0(N)$, which is where this general machinery is used; nothing in the module itself refers to modular curves, levels or primes.