Definitions/Def_AlgebraicCurve_FibreResidueIdentityAlong.lean

The module introduces a single Prop-valued predicate, AlgebraicCurve.FibreResidueIdentityAlong, expressing compatibility of local residues with pull-back of differentials and trace along a map of function fields. The context is a field K and two K-algebra fields F, F', with F' equipped with the predicate HasPrincipalDivisors K F' and both F and F' equipped with HasCanonicalLocalResidueKStar, i.e. with a chosen family assigning to each place v a canonical residue datum: a K-linear map \mathrm{res}_v \colon F \to \kappa(v) into the residue field of v that vanishes on the valuation subring of v, sends f with \pi_v f integral to the residue class of \pi_v f, and kills the monomials (\pi_v^{n+1})^{-1} for n \ge 1 (\pi_v the chosen uniformiser). For a K-algebra map \varphi \colon F \to F' together with a proof hφ that the underlying ring homomorphism is integral, FibreResidueIdentityAlong φ hφ asserts: for every place v of F over K, every \omega \in \Omega_{F/K} and every f' \in F', \sum_{w \in \mathrm{fiberAlong}\,\varphi\,v} \mathrm{Tr}_{\kappa(w)/K}\,\mathrm{res}_w\!\big(f' \cdot \partial_w(\varphi^*\omega)\big) \;=\; \mathrm{Tr}_{\kappa(v)/K}\,\mathrm{res}_v\!\big(\mathrm{Tr}_{F'/F}(f') \cdot \partial_v \omega\big), where the sum runs over the finite fibre Place.fiberAlong φ hφ v of places w of F' restricting to v, \varphi^* is Differential.pullbackAlong φ on Kähler differentials, \partial_v \omega denotes v.differentialCoeff ω (the coefficient of \omega relative to the local differential coordinate at v), \mathrm{Tr}_{F'/F} is traceFunAlong φ, the algebra trace for the F-algebra structure on F' induced by \varphi, and each side is a value of kaehlerResidueTerm, whose argument families are the constant (diagonal) families \mathrm{diagonalHom} of f' and of \mathrm{Tr}_{F'/F}(f') respectively. Thus the predicate is a hypothesis about the chosen residue data on F and F', to be assumed where needed rather than established here.