Changing the base point in Abel-Jacobi divisor sums

This file combines the point-level base-point-change API for the abstract Abel-Jacobi class with the divisor-level Abel-Jacobi sum.

For an order system whose principal divisors have weighted degree zero, and two weight-one base points x₀ and y₀, the divisor-level Abel-Jacobi sums satisfy

AJ_{y₀}(D) = AJ_{x₀}(D) + deg(D) • ([x₀] - [y₀]).

Here deg(D) is the weighted degree for the chosen weight w. The unweighted specialization is the same formula with the ordinary degree. This is the formal divisor-class bookkeeping behind the later Abel maps D ↦ 𝒪_X(D - d·x₀) used in the Jacobian roadmap: changing the normalizing base point translates the degree-d Abel map by d times the class of [x₀] - [y₀].

This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer A, "Pic⁰ X = ker deg (as an abstract group)", and supplies a direct prerequisite for the Layer D/F Abel-map lane D ↦ 𝒪_X(D - d·x₀). No external mathematics is vendored; the proofs reuse Tau Ceti's existing weightedAbelJacobiDivisorClass, weightedBasepointChangeClass, and divisor-class API.

Weighted base-point change for divisor sums

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedAbelJacobiDivisorClass_change_base {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) {x₀ y₀ : X} (hx₀ : w x₀ = 1) (hy₀ : w y₀ = 1) (D : WeilDivisor X) : (S.weightedAbelJacobiDivisorClass w h hy₀) D = (S.weightedAbelJacobiDivisorClass w h hx₀) D + (weightedDegree w) D • S.weightedBasepointChangeClass w h ⋯

Changing the base point in the weighted Abel-Jacobi sum adds the weighted degree times the base-point-change class.

Geometrically, for the residue-degree weight and rational base points x₀, y₀, this is the formal divisor-class identity [D - deg(D)y₀] = [D - deg(D)x₀] + deg(D)[x₀ - y₀] in Pic⁰.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedAbelJacobiDivisorClass_sub_change_base_coe {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) {x₀ y₀ : X} (hx₀ : w x₀ = 1) (hy₀ : w y₀ = 1) (D : WeilDivisor X) : ↑((S.weightedAbelJacobiDivisorClass w h hy₀) D) - ↑((S.weightedAbelJacobiDivisorClass w h hx₀) D) = (weightedDegree w) D • S.divisorClass (pointDifference x₀ y₀)

In the class group, the difference between weighted Abel-Jacobi divisor sums with two base points is the weighted degree times the class [x₀] - [y₀].

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedAbelJacobiDivisorClass_eq_of_weightedDegree_eq_zero {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) {x₀ y₀ : X} (hx₀ : w x₀ = 1) (hy₀ : w y₀ = 1) {D : WeilDivisor X} (hD : (weightedDegree w) D = 0) : (S.weightedAbelJacobiDivisorClass w h hx₀) D = (S.weightedAbelJacobiDivisorClass w h hy₀) D

If a divisor has weighted degree zero, its weighted Abel-Jacobi sum is independent of the choice of weight-one base point.