Pic⁰ pushforward along function-field maps; isogeny data on points #

Definition: Isogeny_ConditionalCurrency (6adae51b-807c-5e9f-ae0b-da141c66671a), by Claude, 2026-09-05.

The first part descends the divisor pushforward along an integral $K$-algebra map $\varphi : F \to F'$ of fields to divisor classes. AlgebraicCurve.Pic0.pushforwardAlongDegZero restricts Divisor.pushforwardAlong φ hφ (on places: $w \mapsto f(w)\,[w|_F]$, where $w|_F$ is the restriction of the valuation subring and $f(w)$ the residue-extension degree) to the degree-zero subgroups, which is legitimate because pushforward preserves degree; pushforwardAlongHom then quotients by principal divisors, using two extra explicit hypotheses: hfin : FiniteAlong K φ, i.e. $F'$ is a finite $F$-module via $\varphi$, and hN : NormFormulaAlong K φ hfin, the project's predicate asserting that for every $f \in F'^\times$ the pushforward of $\mathrm{div}(f)$ is $\mathrm{div}(N_{F'/F}f)$ — a hypothesis, not a theorem. Place.deg_restrictAlong_mul_inertiaDegAlong records $\deg(w|_F)\cdot f(w) = \deg(w)$.

The second part fixes an algebraically closed field $F$ of characteristic zero, elliptic $V,W$ in affine Weierstrass form carrying the classes GenusOnePlaceGate (data: a bijection $W(F) \simeq$ places of $F(W)$, all residue degrees $1$) and AbelTheorem (a degree-zero divisor is principal iff its image under divisorSum vanishes), and an integral $F$-algebra map $\iota : F(V) \to F(W)$. Since all residue degrees are $1$, all inertia degrees are $1$ and pushforward carries $n[w]$ to $n[w|_{F(V)}]$. Conjugating pushforwardAlongHom by the Abel–Jacobi isomorphisms genusOnePic0Equiv gives pointMapOfPushforward : W.Point →+ V.Point. A group of three lemmas in a common shape says that any map $g$ of point sets with $g(0)=0$ which matches $\iota$ on places, $(\mathrm{place}\,P)|_{F(V)} = \mathrm{place}\,g(P)$, equals this homomorphism, hence is additive, and that $g(P)=0$ exactly when the class of $(P)-(0)$ pushes forward to zero. Finally IsogenyEndDatum W and IsogenyHomDatum V₀ V₁ bundle $(\iota,\ \text{integrality},\ \text{finiteness})$ — note the contravariance: the latter has $\iota : F(V_1) \to F(V_0)$ and yields pointHom : V₀.Point →+ V₁.Point; isogenyEndSubring is the subring of AddMonoid.End W.Point generated by all pointEnd, given norm-formula witnesses for every datum.

Relation to Mathlib. Places, divisors, principal divisors and $\mathrm{Pic}^0$ of a function field in this valuation-subring formulation are the project's own; Mathlib supplies the ambient algebra (Finsupp, QuotientAddGroup, AddMonoid.End, Subring.closure, Algebra.norm, residue fields of local rings) and WeierstrassCurve.Affine with its group of points, but no divisor-class theory for curves and no isogeny-induced maps of this kind.

Where it is used. This is the mechanism by which an inclusion of function fields of elliptic curves is turned into an additive map of point groups, so that endomorphism rings and isogeny-induced homomorphisms can be manipulated group-theoretically. The GenusOnePlaceGate datum is an arbitrary point–place bijection with all residue degrees one, so statements identifying these maps with named geometric maps require further hypotheses pinning the dictionary.