Changing the base point in the abstract Abel-Jacobi class

This file adds the base-point-change calculus for the formal divisor-class shadow of the Abel-Jacobi map from TauCeti.AlgebraicGeometry.WeilDivisor.AbelJacobi.Basic.

For a weight w : X → ℤ, a weight-one base point x₀, and another weight-one base point y₀, the degree-corrected point divisors satisfy

[x] - w(x)[y₀] = ([x] - w(x)[x₀]) + w(x)([x₀] - [y₀]).

Passing to divisor classes gives the corresponding formula in the abstract Pic⁰ subgroup: changing the Abel-Jacobi base point translates the class by the weight w x times the degree-zero class [x₀] - [y₀]. For the geometric weight by residue-field degree, this is translation by the degree of the point. In the unweighted/algebraically closed specialization, this is the familiar identity

AJ_{y₀}(x) = AJ_{x₀}(x) + AJ_{y₀}(x₀).

This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer A (Pic⁰ X = ker deg) and is a direct formal prerequisite for Layer F's normalized Abel-Jacobi morphism aj : X ⟶ Jac X, where choosing a rational base point forces x₀ ↦ 0 and changing that choice should be a translation. No external mathematics is vendored; the proofs use only the existing WeilDivisor, OrderSystem.divisorClass, and abstract Abel-Jacobi API.

Class-level base-point changes

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

The degree-zero class [x₀] - [y₀] measuring the translation between two equal-weight base points.

Equations

• S.weightedBasepointChangeClass w hdeg hxy = ⟨S.divisorClass (TauCeti.AlgebraicGeometry.WeilDivisor.pointDifference x₀ y₀), ⋯⟩

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.coe_weightedBasepointChangeClass {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (hdeg : S.IsWeightedDegreeZero w) {x₀ y₀ : X} (hxy : w x₀ = w y₀) : ↑(S.weightedBasepointChangeClass w hdeg hxy) = S.divisorClass (pointDifference x₀ y₀)

@[simp]

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

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedBasepointChangeClass_swap {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (hdeg : S.IsWeightedDegreeZero w) {x₀ y₀ : X} (hxy : w x₀ = w y₀) : S.weightedBasepointChangeClass w hdeg ⋯ = -S.weightedBasepointChangeClass w hdeg hxy

Reversing the two base points negates the base-point-change class.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedBasepointChangeClass_add {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (hdeg : S.IsWeightedDegreeZero w) {x₀ y₀ z₀ : X} (hxy : w x₀ = w y₀) (hyz : w y₀ = w z₀) : S.weightedBasepointChangeClass w hdeg hxy + S.weightedBasepointChangeClass w hdeg hyz = S.weightedBasepointChangeClass w hdeg ⋯

Base-point-change classes compose: the translation from x₀ to z₀ is the sum of the translations from x₀ to y₀ and from y₀ to z₀.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedAbelJacobiClass_change_base {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (hdeg : S.IsWeightedDegreeZero w) {x₀ y₀ : X} (hx₀ : w x₀ = 1) (hy₀ : w y₀ = 1) (x : X) : S.weightedAbelJacobiClass w hdeg hy₀ x = S.weightedAbelJacobiClass w hdeg hx₀ x + w x • S.weightedBasepointChangeClass w hdeg ⋯

Changing the Abel-Jacobi base point from x₀ to y₀ adds w x times the class [x₀] - [y₀]. For the geometric specialization, w x is the residue-field degree.

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

The base-point-change class is the Abel-Jacobi class of the old base point with respect to the new base point.

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

The base-point-change class equals the Abel-Jacobi class of the old base point with respect to the new base point.

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

In the class group, the difference between two weighted Abel-Jacobi classes with different base points is w(x) times the class [x₀] - [y₀].

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

The difference between two weighted Abel-Jacobi classes with the same base point is the class [x] - [y] when the two points have equal weight.