Splitting the divisor class group along the degree at a rational point

This file records the structural consequence of having a weight-one base point for the abstract divisor class group of an order system, continuing the Jacobian roadmap's Layer A.

For an OrderSystem S on a type of points X whose principal divisors have weighted degree zero, WeilDivisor.Principal builds the descended weighted degree weightedDegreeClass on the class group Cl(X) and its kernel picZero, the abstract Pic⁰. Here we add the missing structural fact: a base point x₀ with weight w x₀ = 1 (the residue-field degree of a k-rational point is 1) makes the descended weighted degree map split.

Concretely the class [x₀] provides a degree-one element, so n ↦ n • [x₀] is a group-theoretic section degreeSection of weightedDegreeClass w h. The descended weighted degree map is therefore surjective, and the class group decomposes as the internal direct sum of picZero and the line spanned by [x₀]:

Cl(X) ≃+ picZero × ℤ.

This is the abstract shadow of the geometric statement that, once a k-rational point is chosen, the full Picard group Pic(X) of a smooth proper curve splits as Pic⁰(X) ⊕ ℤ by the degree. Without a rational point the weighted degree map need not be surjective (its image is d·ℤ for the index d of the residue degrees), so the weight-one hypothesis is essential and the construction is non-vacuous.

This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer A, "Pic⁰ X = ker deg (as an abstract group)", by exhibiting Cl(X) as an extension of ℤ by Pic⁰ that the rational point splits, the form in which the degree-zero part is used downstream. It reuses Tau Ceti's WeilDivisor and OrderSystem API and Mathlib's zmultiplesHom and AddMonoidHom/AddEquiv machinery; no external mathematics is vendored.

The degree section at a base point

noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.degreeSection {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (x₀ : X) : ℤ →+ S.ClassGroup

The homomorphism n ↦ n • [x₀], sending an integer n to the class of n copies of the base point x₀. When w x₀ = 1, it is a right inverse of weightedDegreeClass, splitting the degree map.

Equations

• S.degreeSection x₀ = (zmultiplesHom S.ClassGroup) (S.divisorClass (TauCeti.AlgebraicGeometry.WeilDivisor.ofPoint x₀))

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.degreeSection_apply {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (x₀ : X) (n : ℤ) : (S.degreeSection x₀) n = n • S.divisorClass (ofPoint x₀)

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.degreeSection_one {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (x₀ : X) : (S.degreeSection x₀) 1 = S.divisorClass (ofPoint x₀)

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedDegreeClass_divisorClass_ofPoint {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) (x₀ : X) : (weightedDegreeClass w h) (S.divisorClass (ofPoint x₀)) = w x₀

The descended weighted degree of the base-point class is the weight of the base point.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedDegreeClass_degreeSection {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) (x₀ : X) (n : ℤ) : (weightedDegreeClass w h) ((S.degreeSection x₀) n) = n * w x₀

The descended weighted degree of the degree section at n is n * w x₀.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedDegreeClass_comp_degreeSection {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) : (weightedDegreeClass w h).comp (S.degreeSection x₀) = AddMonoidHom.id ℤ

With a weight-one base point, the degree section is a right inverse of the descended weighted degree: weightedDegreeClass ∘ degreeSection = id.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedDegreeClass_degreeSection_of_weight_one {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) (n : ℤ) : (weightedDegreeClass w h) ((S.degreeSection x₀) n) = n

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedDegreeClass_surjective {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) : Function.Surjective ⇑(weightedDegreeClass w h)

With a weight-one base point, the descended weighted degree is surjective onto ℤ.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.degreeSection_injective {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) : Function.Injective ⇑(S.degreeSection x₀)

With a weight-one base point, the degree section is injective.

The product decomposition

noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.degreeCorrection {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) (x₀ : X) : S.ClassGroup →+ S.ClassGroup

The degree-correction homomorphism c ↦ c - (weightedDegreeClass w h c) • [x₀]. With a weight-one base point its image lands in picZero, and together with degreeSection it splits the class group as picZero × ℤ.

Equations

• S.degreeCorrection w h x₀ = AddMonoidHom.id S.ClassGroup - (S.degreeSection x₀).comp (TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedDegreeClass w h)

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.degreeCorrection_apply {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) (x₀ : X) (c : S.ClassGroup) : (S.degreeCorrection w h x₀) c = c - (weightedDegreeClass w h) c • S.divisorClass (ofPoint x₀)

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.degreeCorrection_change_base {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) (x₀ y₀ : X) (c : S.ClassGroup) : (S.degreeCorrection w h y₀) c = (S.degreeCorrection w h x₀) c + (weightedDegreeClass w h) c • S.divisorClass (pointDifference x₀ y₀)

Changing the base point in the class-group degree correction adds the weighted degree of the class times the base-point-change divisor class.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.degreeCorrection_mem_picZero {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) (c : S.ClassGroup) : (S.degreeCorrection w h x₀) c ∈ picZero w h

The degree correction lands in picZero: the degree-corrected class has weighted degree zero, provided the base point has weight one.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.degreeCorrection_divisorClass {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) (x₀ : X) (D : WeilDivisor X) : (S.degreeCorrection w h x₀) (S.divisorClass D) = S.divisorClass (D - (weightedDegree w) D • ofPoint x₀)

Degree correction acts on a divisor class by subtracting the base-point divisor scaled by the weighted degree of any representative.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.degreeCorrection_eq_self_of_mem_picZero {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) (x₀ : X) {c : S.ClassGroup} (hc : c ∈ picZero w h) : (S.degreeCorrection w h x₀) c = c

A class already in picZero is unchanged by degree correction.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.degreeCorrection_coe_picZero {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) (x₀ : X) (p : ↥(picZero w h)) : (S.degreeCorrection w h x₀) ↑p = ↑p

The degree correction of a coerced picZero class is the same class in the ambient class group.

noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.degreeSplitForward {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.ClassGroup →+ ↥(picZero w h) × ℤ

The forward map c ↦ (c - (weightedDegreeClass w h c) • [x₀], weightedDegreeClass w h c) of the degree splitting at a weight-one base point x₀: the first component is the weighted-degree-corrected class, which lands in picZero, and the second is the descended weighted degree. Together with degreeSplitInverse this assembles the product decomposition classGroupAddEquivPicZeroProdInt.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.degreeSplitInverse {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) (x₀ : X) : ↥(picZero w h) × ℤ →+ S.ClassGroup

The inverse map (p, n) ↦ p + n • [x₀] of the degree splitting at a base point x₀: add n copies of the base-point class to a class of weighted degree zero.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.degreeSplitInverse_degreeSplitForward {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) (c : S.ClassGroup) : (S.degreeSplitInverse w h x₀) ((S.degreeSplitForward w h hx₀) c) = c

noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.classGroupAddEquivPicZeroProdInt {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.ClassGroup ≃+ ↥(picZero w h) × ℤ

The class group of an order system with weighted-degree-zero principal divisors and a weight-one base point splits as the direct product of the abstract Pic⁰ and ℤ.

The forward map sends a class c to its weighted-degree-corrected part c - (weightedDegreeClass w h c) • [x₀] in picZero together with weightedDegreeClass w h c; the inverse sends (p, n) to p + n • [x₀]. This is the abstract form of the splitting Pic(X) ≃ Pic⁰(X) ⊕ ℤ of a smooth proper curve with a rational point.

Equations

• S.classGroupAddEquivPicZeroProdInt w h hx₀ = (S.degreeSplitForward w h hx₀).toAddEquiv (S.degreeSplitInverse w h x₀) ⋯ ⋯

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.classGroupAddEquivPicZeroProdInt_apply {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) (c : S.ClassGroup) : (S.classGroupAddEquivPicZeroProdInt w h hx₀) c = (⟨(S.degreeCorrection w h x₀) c, ⋯⟩, (weightedDegreeClass w h) c)

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.classGroupAddEquivPicZeroProdInt_symm_apply {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) (p : ↥(picZero w h)) (n : ℤ) : (S.classGroupAddEquivPicZeroProdInt w h hx₀).symm (p, n) = ↑p + n • S.divisorClass (ofPoint x₀)

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.classGroupAddEquivPicZeroProdInt_coe_picZero {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) (p : ↥(picZero w h)) : (S.classGroupAddEquivPicZeroProdInt w h hx₀) ↑p = (p, 0)

Under the splitting Cl(X) ≃+ picZero × ℤ, a coerced picZero class has Pic⁰ component itself and degree component 0.