Abel-Jacobi fibers and complete linear systems

This file records the formal fixed-degree fiber statement for the divisor-class shadow of the Abel-Jacobi map. The existing map

D ↦ [D - deg(D) • [x₀]] ∈ Pic⁰

is defined on all Weil divisors as OrderSystem.weightedAbelJacobiDivisorClass. On effective divisors of a fixed degree, two divisors have the same normalized Abel-Jacobi class exactly when they are linearly equivalent; equivalently, one lies in the complete linear system of the other. The same statement is restated for Mathlib's symmetric powers through the existing equivalence between Sym X d and effective divisors of degree d.

This is the formal-divisor version of the classical fact that the fibers of the Abel map Symᵈ X → Pic⁰ X, D ↦ 𝒪_X(D - d·x₀), are complete linear systems. It advances TauCetiRoadmap/JacobianChallenge/README.md, Layer C/D, the symmetric-power Abel-map lane D ↦ 𝒪_X(D - d·x₀), using the abstract divisor class group available before line bundles, the Picard scheme, or the Jacobian variety exist. No external mathematics is vendored.

Fixed-degree effective divisors

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

For effective divisors of the same fixed degree, equality of normalized Abel-Jacobi classes is exactly linear equivalence of the underlying divisors.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedAbelJacobiDivisorClass_one_effectiveDivisorOfDegree_eq_iff_mem_completeLinearSystem {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {d : ℕ} (h : IsUnweightedDegreeZero) (x₀ : X) (D E : EffectiveDivisorOfDegree X d) : (S.weightedAbelJacobiDivisorClass (fun (x : X) => 1) h ⋯) ↑E = (S.weightedAbelJacobiDivisorClass (fun (x : X) => 1) h ⋯) ↑D ↔ ↑E ∈ S.completeLinearSystem ↑D

The fixed-degree Abel-Jacobi fiber through D is the complete linear system |D|, restricted to effective divisors of the same degree.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.setOf_weightedAbelJacobiDivisorClass_one_effectiveDivisorOfDegree_eq {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {d : ℕ} (h : IsUnweightedDegreeZero) (x₀ : X) (D : EffectiveDivisorOfDegree X d) : {E : EffectiveDivisorOfDegree X d | (S.weightedAbelJacobiDivisorClass (fun (x : X) => 1) h ⋯) ↑E = (S.weightedAbelJacobiDivisorClass (fun (x : X) => 1) h ⋯) ↑D} = {E : EffectiveDivisorOfDegree X d | ↑E ∈ S.completeLinearSystem ↑D}

As a set of fixed-degree effective divisors, the Abel-Jacobi fiber through D is the restriction of the complete linear system |D|.

Symmetric powers

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedAbelJacobiDivisorClass_one_ofSym_eq_iff_mem_completeLinearSystem {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {d : ℕ} (h : IsUnweightedDegreeZero) (x₀ : X) (s t : Sym X d) : (S.weightedAbelJacobiDivisorClass (fun (x : X) => 1) h ⋯) ↑(EffectiveDivisorOfDegree.ofSym t) = (S.weightedAbelJacobiDivisorClass (fun (x : X) => 1) h ⋯) ↑(EffectiveDivisorOfDegree.ofSym s) ↔ ↑(EffectiveDivisorOfDegree.ofSym t) ∈ S.completeLinearSystem ↑(EffectiveDivisorOfDegree.ofSym s)

On symmetric powers, equality of normalized Abel-Jacobi classes is exactly membership of the corresponding divisor in the complete linear system.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.setOf_weightedAbelJacobiDivisorClass_one_ofSym_eq {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {d : ℕ} (h : IsUnweightedDegreeZero) (x₀ : X) (s : Sym X d) : {t : Sym X d | (S.weightedAbelJacobiDivisorClass (fun (x : X) => 1) h ⋯) ↑(EffectiveDivisorOfDegree.ofSym t) = (S.weightedAbelJacobiDivisorClass (fun (x : X) => 1) h ⋯) ↑(EffectiveDivisorOfDegree.ofSym s)} = {t : Sym X d | ↑(EffectiveDivisorOfDegree.ofSym t) ∈ S.completeLinearSystem ↑(EffectiveDivisorOfDegree.ofSym s)}

As a set of symmetric-power points, the Abel-Jacobi fiber through s is the preimage of the complete linear system |ofSym s|.