Fixed-degree compatibility for Abel-Jacobi divisor classes

This file records fixed-degree effective-divisor and symmetric-power compatibility for the formal Abel-Jacobi divisor class map. For an effective divisor D, the underlying weighted divisor-level map sends

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

At the constant weight 1 this specializes to D ↦ [D - deg(D) • [x₀]] ∈ Pic⁰, and for ordinary degree-d divisors therefore models the divisor-class shadow of the Abel map on symmetric powers Symᵈ X → Pic⁰ X, D ↦ 𝒪_X(D - d·x₀).

The file does not introduce a parallel fixed-degree Abel-map API. It states the required fixed-degree and Sym.append facts directly in terms of the existing divisor-level homomorphism weightedAbelJacobiDivisorClass.

This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer C/D, "Relative effective Cartier divisors and symmetric powers Symᵈ X" and the Abel-map lane D ↦ 𝒪_X(D - d·x₀), using the existing abstract Pic⁰ quotient before the Picard scheme exists. No external mathematics is vendored.

Weighted fixed-degree Abel-Jacobi classes

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedAbelJacobiDivisorClass_cast {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 : ℕ} (hde : d = e) (D : EffectiveDivisorOfDegree X d) : (S.weightedAbelJacobiDivisorClass w h hx₀) ↑((EffectiveDivisorOfDegree.cast hde) D) = (S.weightedAbelJacobiDivisorClass w h hx₀) ↑D

Changing only the degree index of a fixed-degree divisor does not change its weighted Abel-Jacobi class.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedAbelJacobiDivisorClass_effectiveDivisorOfDegree_zero {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₀) ↑(EffectiveDivisorOfDegree.zero X) = 0

The weighted Abel-Jacobi class of the zero effective divisor is zero.

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

Adding fixed-degree effective divisors sends their weighted Abel-Jacobi class to the sum of the two classes.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedAbelJacobiDivisorClass_ofSym_append {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {d e : ℕ} (w : X → ℤ) (h : S.IsWeightedDegreeZero w) {x₀ : X} (hx₀ : w x₀ = 1) (s : Sym X d) (t : Sym X e) : (S.weightedAbelJacobiDivisorClass w h hx₀) ↑(EffectiveDivisorOfDegree.ofSym (s.append t)) = (S.weightedAbelJacobiDivisorClass w h hx₀) ↑(EffectiveDivisorOfDegree.ofSym s) + (S.weightedAbelJacobiDivisorClass w h hx₀) ↑(EffectiveDivisorOfDegree.ofSym t)

Appending symmetric-power divisors sends their weighted Abel-Jacobi class to the sum of the two classes.