Abel-Jacobi classes and the degree splitting

This file records how the abstract Abel-Jacobi divisor class from TauCeti.AlgebraicGeometry.WeilDivisor.AbelJacobi.Basic interacts with the class-group splitting from TauCeti.AlgebraicGeometry.WeilDivisor.Degree.Splitting.

For an order system whose principal divisors have weighted degree zero, a weight-one base point x₀ splits the divisor class group as

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

Under this splitting, the class of a point divisor [x] has Pic⁰ component equal to the weighted Abel-Jacobi class of x, and degree component w x. Equivalently, the degree-corrected class [x] - w(x)[x₀] maps to the Abel-Jacobi class together with degree 0.

This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer A, the "Pic⁰ X = ker deg (as an abstract group)" item and the rational-point degree splitting used by the later normalized Abel-Jacobi morphism. No external mathematics is vendored; the proofs combine Tau Ceti's existing OrderSystem.picZero, weightedAbelJacobiClass, and classGroupAddEquivPicZeroProdInt APIs.

Degree correction of point classes

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.degreeCorrection_divisorClass_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.degreeCorrection w h x₀) (S.divisorClass (ofPoint x)) = ↑(S.weightedAbelJacobiClass w h hx₀ x)

Correcting the degree of the point class [x] by the base point x₀ gives exactly the class-group representative of the weighted Abel-Jacobi class of x.

Weighted splitting formulas

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.classGroupAddEquivPicZeroProdInt_divisorClass_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.classGroupAddEquivPicZeroProdInt w h hx₀) (S.divisorClass (ofPoint x)) = (S.weightedAbelJacobiClass w h hx₀ x, w x)

Under the splitting Cl(X) ≃+ Pic⁰ × ℤ, the class of the point divisor [x] has Pic⁰ component the weighted Abel-Jacobi class of x, and degree component w x.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.classGroupAddEquivPicZeroProdInt_coe_weightedAbelJacobiClass {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.classGroupAddEquivPicZeroProdInt w h hx₀) ↑(S.weightedAbelJacobiClass w h hx₀ x) = (S.weightedAbelJacobiClass w h hx₀ x, 0)

Under the splitting Cl(X) ≃+ Pic⁰ × ℤ, a coerced weighted Abel-Jacobi class has degree zero and Pic⁰ component itself.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.classGroupAddEquivPicZeroProdInt_divisorClass_weightedPointBaseDifference {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.classGroupAddEquivPicZeroProdInt w h hx₀) (S.divisorClass (weightedPointBaseDifference w x₀ x)) = (S.weightedAbelJacobiClass w h hx₀ x, 0)

The degree-corrected point divisor [x] - w(x)[x₀] maps to the weighted Abel-Jacobi class and degree 0 under the splitting Cl(X) ≃+ Pic⁰ × ℤ.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.classGroupAddEquivPicZeroProdInt_symm_weightedAbelJacobiClass {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.classGroupAddEquivPicZeroProdInt w h hx₀).symm (S.weightedAbelJacobiClass w h hx₀ x, w x) = S.divisorClass (ofPoint x)

The inverse splitting reconstructs the point class [x] from its weighted Abel-Jacobi component and its degree w x.