Restriction of places, ramification and inertia, divisor pull-back and push-forward #

Definition: AlgebraicCurve_DivisorPushPull (cf383033-9d83-5afb-a5cf-a6a5732a3fd7), by Claude, 2026-09-05.

Throughout, $K \subseteq F \subseteq F'$ is a tower of fields (Algebra K F, Algebra K F', Algebra F F', IsScalarTower K F F'), with Place, Divisor, degree, IsPrincipal, Pic0, HasPrincipalDivisors taken from the project's divisor-class-group module; a place carries a valuation subring together with the conditions recorded there, and ord, deg and ResidueField are its associated order function, degree and residue field. For a place $w$ of $F'$, Place.restrict F w is the place of $F$ whose valuation subring is the preimage $\mathcal O_w \cap F$ (ValuationSubring.comap), the properness and discreteness conditions being verified from [Algebra.IsIntegral F F'] and integral closedness. Place.ramificationIndex F w is defined as the natural-number infimum of $\{n>0 : n = \operatorname{ord}_w(\iota f)\ \text{for some } f \in F^\times\}$; under integrality it is positive, divides every $\operatorname{ord}_w(\iota f)$, and ord_restrict gives $\operatorname{ord}_w(\iota f) = e\cdot \operatorname{ord}_{w|_F}(f)$. Place.restrictInclusion and Place.restrictResidueMap (a local homomorphism and the induced map of residue fields, with algebra and scalar-tower instances) make $\kappa(w)$ an extension of $\kappa(w|_F)$, and Place.inertiaDeg F w is its finrank, so that deg_restrict_mul_inertiaDeg is the tower formula $\deg(w|_F)\cdot f = \deg w$. Assuming HasPrincipalDivisors K F', Place.fiber F' v is the finite set of places above $v$. On divisors: Divisor.mapRestrict is the bare relabelling $w \mapsto w|_F$; Divisor.pushforward F sends $w \mapsto f(w)\, w|_F$ and preserves degree; Divisor.pullback F' sends $v \mapsto \sum_{w \mid v} e(w)\,w$, takes $\operatorname{div}_F f$ to $\operatorname{div}_{F'}(\iota f)$ and principal divisors to principal divisors. Two classes state ramification identities as hypotheses: SumRamificationInertia ($\sum_{w\mid v} e f = [F':F]$) and FundamentalIdentity ($\sum_{w\mid v} e \deg w = [F':F]\deg v$), the former implying the latter; under the latter, pull-back multiplies degrees by $[F':F]$ and descends to Pic0.pullbackHom. Norm compatibility is the project's proposition Divisor.PushforwardNormFormula K F F': for every $f \in (F')^\times$, every divisor $D$ with $D(w) = \operatorname{ord}_w f$ for all $w$, and every $v$, $(\pi_* D)(v) = \operatorname{ord}_v(N_{F'/F} f)$; it is passed as an explicit argument to Pic0.pushforwardHom (which also needs Module.Finite F F').

Relation to Mathlib. Mathlib's ramification index and inertia degree are defined for ideals in extensions of Dedekind domains (Ideal.ramificationIdx, Ideal.inertiaDeg); here both are redefined directly for the project's own Place, the ramification index as an infimum of positive orders and the inertia degree as a residue-field finrank. The fundamental identity and the norm formula are not proved in this module but appear as the project's hypothesis classes SumRamificationInertia, FundamentalIdentity and the proposition Divisor.PushforwardNormFormula.

Where it is used. These maps supply the functoriality of degree-zero divisor classes along a finite extension of function fields, so that a correspondence between curves acts on $\mathrm{Pic}^0$ by push-forward after pull-back along its two projections; this is the form in which Hecke operators act on the Jacobians of modular curves in the modularity part of the argument.