Abel-Jacobi sums through the weighted-degree-zero quotient

This file connects two existing Layer A models in the Jacobian roadmap. The file WeilDivisor.AbelJacobiSum defines the formal Abel-Jacobi sum of a divisor as an element of the abstract Pic⁰, while WeilDivisor.PicZeroQuotient identifies Pic⁰ with weighted-degree-zero divisors modulo principal divisors of weighted degree zero. Here we record the corresponding quotient representative:

D ↦ [D - weightedDegree w D • x₀] in (weighted-degree-zero divisors) / (principal divisors).

Under the quotient equivalence, this representative maps to the existing Abel-Jacobi divisor class. For point divisors this recovers the point Abel-Jacobi class. This is the quotient-level form of the Abel map D ↦ 𝒪_X(D - d·x₀) used later for symmetric powers in the construction of the Jacobian, with the ordinary degree formula recovered from the constant-weight-one specialization.

This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer A, specifically the "Pic⁰ X = ker deg (as an abstract group)" item and the Layer D/F Abel-map prerequisite D ↦ 𝒪_X(D - d·x₀). No external mathematics is vendored; the proofs reuse Tau Ceti's existing weightedAbelJacobiDivisorClass and quotient equivalence weightedDegreeZeroQuotientEquivPicZero.

Weighted quotient representatives

noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedAbelJacobiQuotientClass {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) {x₀ : X} (hx₀ : w x₀ = 1) : WeilDivisor X →+ ↥(weightedDegreeZeroSubgroup w) ⧸ S.principalSubgroupOfWeightedDegreeZero w

The quotient class of the degree-corrected representative D - weightedDegree(D) • [x₀].

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedAbelJacobiQuotientClass_mk {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) {x₀ : X} (hx₀ : w x₀ = 1) (D : WeilDivisor X) : (S.weightedAbelJacobiQuotientClass w hx₀) D = ↑(weightedAbelJacobiDegreeZeroDivisor w hx₀ D)

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

The quotient Abel-Jacobi representative of a sum is the sum of the quotient representatives.

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

The quotient Abel-Jacobi representative of an integral multiple is the corresponding multiple of the quotient representative.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedDegreeZeroQuotientEquivPicZero_weightedAbelJacobiQuotientClass {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.weightedDegreeZeroQuotientEquivPicZero w h) ((S.weightedAbelJacobiQuotientClass w hx₀) D) = (S.weightedAbelJacobiDivisorClass w h hx₀) D

The quotient representative maps to the weighted Abel-Jacobi divisor class under the degree-zero quotient equivalence.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedDegreeZeroQuotientEquivPicZero_weightedAbelJacobiQuotientClass_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.weightedDegreeZeroQuotientEquivPicZero w h) ((S.weightedAbelJacobiQuotientClass w hx₀) (ofPoint x)) = S.weightedAbelJacobiClass w h hx₀ x

For point divisors, the quotient representative maps to the point Abel-Jacobi class.

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

The quotient Abel-Jacobi representative of a finitely supported formal divisor is the finite sum of the quotient representatives of its point divisors.

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

The base-point divisor represents zero in the degree-zero quotient.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedAbelJacobiQuotientClass_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.weightedAbelJacobiQuotientClass w hx₀) (S.principalDivisor g) = 0

A principal divisor has zero weighted quotient Abel-Jacobi representative.

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

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

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

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