The abstract Abel-Jacobi divisor class map

This file adds the point-level divisor-class shadow of the Abel-Jacobi map to the formal Layer A divisor API. Once the Jacobian is constructed as Pic⁰(X), the Abel-Jacobi morphism attached to a base point x₀ sends a point x to the degree-zero line bundle 𝒪_X(x - x₀) over an algebraically closed field. For closed points over a non-algebraically closed field, the weighted-degree-corrected divisor is x - w(x) x₀, when x₀ has residue degree 1.

Here the geometry is still abstracted to an OrderSystem and an integer-valued weight w : X → ℤ. We define the formal divisor [x] - w(x)[x₀], prove it has weighted degree zero when w x₀ = 1, and take its divisor class as an element of the abstract Pic⁰ subgroup already built in WeilDivisor.Principal. The unweighted specialization recovers x ↦ [x] - [x₀].

This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer A (Pic⁰ X = ker deg) as a direct prerequisite for Layer F's Abel-Jacobi morphism aj : X ⟶ Jac X, while staying at the formal divisor-class level available before line bundles, the Picard scheme, or the Jacobian variety exist. No external mathematics is vendored; this reuses Tau Ceti's WeilDivisor, OrderSystem.divisorClass, and OrderSystem.picZero API.

Abel-Jacobi classes in the abstract Picard group

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

The weighted abstract Abel-Jacobi class of a point.

For a geometric weight w x = [κ(x) : k] and a rational base point x₀ (w x₀ = 1), this is the class of [x] - w(x)[x₀] in the abstract weighted-degree-zero Picard group.

Equations

• S.weightedAbelJacobiClass w hdeg hx₀ x = ⟨S.divisorClass (TauCeti.AlgebraicGeometry.WeilDivisor.weightedPointBaseDifference w x₀ x), ⋯⟩

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.coe_weightedAbelJacobiClass {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (hdeg : S.IsWeightedDegreeZero w) {x₀ : X} (hx₀ : w x₀ = 1) (x : X) : ↑(S.weightedAbelJacobiClass w hdeg hx₀ x) = S.divisorClass (weightedPointBaseDifference w x₀ x)

Coercing the weighted Abel-Jacobi class to the class group gives the divisor class of the degree-corrected point divisor. This is the canonical simp form for the subtype coercion.

@[simp]

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

The weighted abstract Abel-Jacobi class of the base point is zero.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedAbelJacobiClass_eq_iff_divisorClass {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (hdeg : S.IsWeightedDegreeZero w) {x₀ : X} (hx₀ : w x₀ = 1) {x y : X} : S.weightedAbelJacobiClass w hdeg hx₀ x = S.weightedAbelJacobiClass w hdeg hx₀ y ↔ S.divisorClass (weightedPointBaseDifference w x₀ x) = S.divisorClass (weightedPointBaseDifference w x₀ y)

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

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedAbelJacobiClass_eq_iff_linearlyEquivalent {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (hdeg : S.IsWeightedDegreeZero w) {x₀ : X} (hx₀ : w x₀ = 1) {x y : X} : S.weightedAbelJacobiClass w hdeg hx₀ x = S.weightedAbelJacobiClass w hdeg hx₀ y ↔ S.LinearlyEquivalent (weightedPointBaseDifference w x₀ x) (weightedPointBaseDifference w x₀ y)

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