Abel-Jacobi sums of Weil divisors

This file extends the formal Layer A Abel-Jacobi API from points to arbitrary Weil divisors. Given an order system whose principal divisors have weighted degree zero and a weight-one base point x₀, the degree splitting

Cl(X) ≃+ Pic⁰(X) × ℤ

has first component c ↦ c - (weightedDegreeClass w h c) · [x₀]. Composing this component with the divisor-class map gives the additive Abel-Jacobi sum of a formal divisor:

D ↦ [D - weightedDegree w D · x₀] ∈ Pic⁰.

For a divisor D = ∑ nₓ[x], this is the finite sum ∑ nₓ AJ(x). This is the formal divisor-class shadow of the Abel maps D ↦ 𝒪_X(D - d x₀) used later to construct the Jacobian from symmetric powers.

This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer A, the "Pic⁰ X = ker deg (as an abstract group)" item and the Layer D/F Abel-map prerequisite D ↦ 𝒪_X(D - d·x₀). It reuses Tau Ceti's existing WeilDivisor, OrderSystem.picZero, degreeCorrection, and weightedAbelJacobiClass APIs; no external mathematics is vendored.

Weighted Abel-Jacobi sums

noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedAbelJacobiDivisorClass {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) {x₀ : X} (hx₀ : w x₀ = 1) : WeilDivisor X →+ ↥(picZero w h)

The additive Abel-Jacobi sum of a Weil divisor.

For a divisor D, this is the class of D - weightedDegree w D • [x₀] in the abstract weighted-degree-zero Picard group. On point divisors it recovers weightedAbelJacobiClass, and on finite sums it is the corresponding sum of point Abel-Jacobi classes.

Equations

• S.weightedAbelJacobiDivisorClass w h hx₀ = ((S.degreeCorrection w h x₀).comp S.divisorClass).codRestrict (TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.picZero w h) ⋯

@[simp]

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

Coercing the weighted Abel-Jacobi sum to the class group gives the divisor class of D - weightedDegree w D • [x₀]. This is the canonical class-group form of the construction.

@[simp]

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

The weighted Abel-Jacobi sum is zero on the base-point divisor.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedAbelJacobiDivisorClass_ofPoint {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) {x₀ : X} (hx₀ : w x₀ = 1) (x : X) : (S.weightedAbelJacobiDivisorClass w h hx₀) (ofPoint x) = S.weightedAbelJacobiClass w h hx₀ x

On a point divisor, the Abel-Jacobi sum is the point Abel-Jacobi class.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedAbelJacobiDivisorClass_add {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) {x₀ : X} (hx₀ : w x₀ = 1) (D E : WeilDivisor X) : (S.weightedAbelJacobiDivisorClass w h hx₀) (D + E) = (S.weightedAbelJacobiDivisorClass w h hx₀) D + (S.weightedAbelJacobiDivisorClass w h hx₀) E

The Abel-Jacobi sum of a sum of divisors is the sum of their Abel-Jacobi sums.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedAbelJacobiDivisorClass_zsmul {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) {x₀ : X} (hx₀ : w x₀ = 1) (n : ℤ) (D : WeilDivisor X) : (S.weightedAbelJacobiDivisorClass w h hx₀) (n • D) = n • (S.weightedAbelJacobiDivisorClass w h hx₀) D

The Abel-Jacobi sum of an integral multiple of a divisor is the corresponding multiple of the Abel-Jacobi sum.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedAbelJacobiDivisorClass_eq_sum {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) {x₀ : X} (hx₀ : w x₀ = 1) (D : WeilDivisor X) : (S.weightedAbelJacobiDivisorClass w h hx₀) D = Finsupp.sum D fun (x : X) (n : ℤ) => n • S.weightedAbelJacobiClass w h hx₀ x

The Abel-Jacobi sum of a finitely supported formal divisor is the finite sum of the point Abel-Jacobi classes weighted by the divisor coefficients.

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

Equality of weighted Abel-Jacobi sums is equality of the corresponding degree-corrected divisor classes.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedAbelJacobiDivisorClass_eq_iff_linearlyEquivalent {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) {x₀ : X} (hx₀ : w x₀ = 1) {D E : WeilDivisor X} : (S.weightedAbelJacobiDivisorClass w h hx₀) D = (S.weightedAbelJacobiDivisorClass w h hx₀) E ↔ S.LinearlyEquivalent (D - (weightedDegree w) D • ofPoint x₀) (E - (weightedDegree w) E • ofPoint x₀)

Equality of weighted Abel-Jacobi sums is linear equivalence of the corresponding degree-corrected divisors.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedAbelJacobiDivisorClass_eq_iff_linearlyEquivalent_of_weightedDegree_eq {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) {x₀ : X} (hx₀ : w x₀ = 1) {D E : WeilDivisor X} (hDE : (weightedDegree w) D = (weightedDegree w) E) : (S.weightedAbelJacobiDivisorClass w h hx₀) D = (S.weightedAbelJacobiDivisorClass w h hx₀) E ↔ S.LinearlyEquivalent D E

If two divisors have the same weighted degree, equality of their weighted Abel-Jacobi classes is exactly linear equivalence of the original divisors.

The equal-degree hypothesis is essential: the Abel-Jacobi class only records the Pic⁰ component of the divisor class after subtracting the same degree from the chosen base point.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedAbelJacobiDivisorClass_one_eq_iff_linearlyEquivalent_of_degree_eq {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (h : IsUnweightedDegreeZero) (x₀ : X) {D E : WeilDivisor X} (hDE : degree D = degree E) : (S.weightedAbelJacobiDivisorClass (fun (x : X) => 1) h ⋯) D = (S.weightedAbelJacobiDivisorClass (fun (x : X) => 1) h ⋯) E ↔ S.LinearlyEquivalent D E

In the unweighted theory, equal-degree divisors have the same Abel-Jacobi class exactly when they are linearly equivalent.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedAbelJacobiDivisorClass_eq_of_linearlyEquivalent {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) {x₀ : X} (hx₀ : w x₀ = 1) {D E : WeilDivisor X} (hlin : S.LinearlyEquivalent D E) : (S.weightedAbelJacobiDivisorClass w h hx₀) D = (S.weightedAbelJacobiDivisorClass w h hx₀) E

The Abel-Jacobi sum is invariant under linear equivalence of divisors with the same weighted degree.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.classGroupAddEquivPicZeroProdInt_divisorClass {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) {x₀ : X} (hx₀ : w x₀ = 1) (D : WeilDivisor X) : (S.classGroupAddEquivPicZeroProdInt w h hx₀) (S.divisorClass D) = ((S.weightedAbelJacobiDivisorClass w h hx₀) D, (weightedDegree w) D)

Under the splitting Cl(X) ≃+ Pic⁰ × ℤ, the class of a divisor has Pic⁰ component its weighted Abel-Jacobi sum and degree component its weighted degree.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.classGroupAddEquivPicZeroProdInt_symm_weightedAbelJacobiDivisorClass {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) {x₀ : X} (hx₀ : w x₀ = 1) (D : WeilDivisor X) : (S.classGroupAddEquivPicZeroProdInt w h hx₀).symm ((S.weightedAbelJacobiDivisorClass w h hx₀) D, (weightedDegree w) D) = S.divisorClass D

The inverse splitting reconstructs the divisor class from its weighted Abel-Jacobi sum and weighted degree.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedAbelJacobiDivisorClass_principalDivisor {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) {x₀ : X} (hx₀ : w x₀ = 1) (g : G) : (S.weightedAbelJacobiDivisorClass w h hx₀) (S.principalDivisor g) = 0

A principal divisor has zero Abel-Jacobi sum.