Point differences generate the degree-zero divisor group

For a fixed base point x₀, this file proves that the degree-zero Weil divisors are exactly the integer combinations of the point differences [x] - [x₀], and records the underlying closed form: every divisor D satisfies

D - (degree D) • [x₀] = Σ_x D(x) • ([x] - [x₀]),

so a divisor of degree zero is Σ_x D(x) • ([x] - [x₀]). Taking the subgroup generated by the point differences, this says

degreeZeroSubgroup X = AddSubgroup.closure { [x] - [x₀] | x }.

The weighted analogue, using the degree-corrected point divisors [x] - w(x) • [x₀] of WeilDivisor.weightedPointBaseDifference, holds whenever the base point has weight one:

weightedDegreeZeroSubgroup w = AddSubgroup.closure { [x] - w(x) • [x₀] | x }.

The weighted statements are the general form; the unweighted API is derived from it by specializing to the constant weight w = fun _ => 1, where weightedPointBaseDifference collapses to pointDifference and weightedDegree to degree.

This is the formal-divisor shadow of the geometric fact that, over a field with a chosen rational point x₀, the Abel-Jacobi map on symmetric powers surjects onto Pic⁰: a degree-zero divisor class is a sum of the classes of [x] - [x₀]. It is the combinatorial input to that surjectivity, available at the free Weil-divisor level before line bundles, principal divisors, the Picard scheme, or the Jacobian variety exist.

This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer A, "Divisors on a curve: Weil divisors ⊕_x ℤ", "Degree", and "Pic⁰ X = ker deg (as an abstract group)", and feeds the Layer D/F Abel-map prerequisite D ↦ 𝒪_X(D - d·x₀). No external mathematics is vendored; the proofs reuse Tau Ceti's WeilDivisor API and Mathlib's finitely-supported induction and subgroup closure machinery.

Weighted version

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.sum_zsmul_weightedPointBaseDifference {X : Type u_1} (w : X → ℤ) (x₀ : X) (D : WeilDivisor X) : (Finsupp.sum D fun (x : X) (n : ℤ) => n • weightedPointBaseDifference w x₀ x) = D - (weightedDegree w) D • ofPoint x₀

The weighted closed form: subtracting (weightedDegree w D) • [x₀] from D expresses it as the finite sum of the degree-corrected point divisors D(x) • ([x] - w(x) • [x₀]).

theorem TauCeti.AlgebraicGeometry.WeilDivisor.eq_sum_zsmul_weightedPointBaseDifference {X : Type u_1} (w : X → ℤ) {D : WeilDivisor X} (hD : (weightedDegree w) D = 0) (x₀ : X) : D = Finsupp.sum D fun (x : X) (n : ℤ) => n • weightedPointBaseDifference w x₀ x

A divisor of weighted degree zero is the finite integer combination Σ_x D(x) • ([x] - w(x) • [x₀]) of degree-corrected point divisors based at x₀.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.weightedDegreeZeroSubgroup_eq_closure_weightedPointBaseDifference {X : Type u_1} (w : X → ℤ) {x₀ : X} (hx₀ : w x₀ = 1) : weightedDegreeZeroSubgroup w = AddSubgroup.closure (Set.range fun (x : X) => weightedPointBaseDifference w x₀ x)

The weighted degree-zero divisors are generated by the degree-corrected point divisors [x] - w(x) • [x₀]. When the base point has weight one (the residue-field degree of a k-rational point is one), the weighted degree-zero subgroup is generated by all the weightedPointBaseDifference w x₀ x. The weight-one hypothesis is what puts the generators inside the subgroup; without it the generators need not have weighted degree zero.

Unweighted version

The unweighted statements are the constant-weight w = fun _ => 1 specialization of the weighted API above, where weightedPointBaseDifference (fun _ => 1) x₀ x = pointDifference x x₀ and weightedDegree (fun _ => 1) = degree.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.sum_zsmul_pointDifference {X : Type u_1} (x₀ : X) (D : WeilDivisor X) : (Finsupp.sum D fun (x : X) (n : ℤ) => n • pointDifference x x₀) = D - degree D • ofPoint x₀

The closed form for the base-point correction: subtracting (degree D) • [x₀] from D expresses it as the finite sum of D(x) • ([x] - [x₀]). Because the coefficients of D sum to degree D, the base-point contributions collapse to a single (degree D) • [x₀] term.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.eq_sum_zsmul_pointDifference {X : Type u_1} {D : WeilDivisor X} (hD : degree D = 0) (x₀ : X) : D = Finsupp.sum D fun (x : X) (n : ℤ) => n • pointDifference x x₀

A divisor of degree zero is the finite integer combination Σ_x D(x) • ([x] - [x₀]) of point differences based at x₀. This is the closed form of the Abel-Jacobi expansion of a degree-zero divisor.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.degreeZeroSubgroup_eq_closure_pointDifference {X : Type u_1} (x₀ : X) : degreeZeroSubgroup X = AddSubgroup.closure (Set.range fun (x : X) => pointDifference x x₀)

The degree-zero divisors are generated by the point differences [x] - [x₀]. For any base point x₀, the unweighted degree-zero subgroup is the subgroup generated by all point differences based at x₀. This is the formal-divisor form of Abel-Jacobi surjectivity onto the degree-zero Picard group.