Principal divisors and the divisor class group of an order system

This file adds the next piece of the Jacobian roadmap's Layer A on top of the formal Weil divisor group: principal divisors, the divisor class group Cl(X), and the abstract degree-zero subgroup Pic⁰.

The geometric input is packaged as an OrderSystem: a family of ℤ-valued order-of-vanishing homomorphisms ord x : G →+ ℤ indexed by the points X, with the finiteness condition that each g : G has nonzero order at only finitely many points. Instantiating G with Additive Kˣ for the multiplicative group of a function field, ord x is the order of vanishing ord_x(f) of a rational function f at the point x, and the principal divisor of f is the finite formal sum Σ_x ord_x(f) · [x]. The finiteness condition is exactly the statement that a rational function has zeros and poles at only finitely many points.

From this data we build:

• OrderSystem.principalDivisor and OrderSystem.principalHom, the principal divisor of a function and its packaging as a homomorphism G →+ WeilDivisor X;
• OrderSystem.principalSubgroup, the subgroup of principal divisors, and OrderSystem.LinearlyEquivalent, the equivalence relation "differ by a principal divisor";
• OrderSystem.ClassGroup, the divisor class group WeilDivisor X ⧸ principal, with its quotient map OrderSystem.divisorClass and the characterization of equal classes;
• OrderSystem.weightedDegreeClass and OrderSystem.picZero: when principal divisors have weighted degree zero (the geometric fact that a rational function has as many zeros as poles, counted with residue-field degrees on a curve over a non-algebraically-closed field, recorded here as the hypothesis IsWeightedDegreeZero), the weighted degree descends to the class group, and Pic⁰ is the kernel of that descended weighted degree.

This advances the Layer A roadmap item "principal divisors" and constructs the abstract "Pic⁰ X = ker deg (as an abstract group, with the geometric degree supplied as a weight)" of TauCetiRoadmap/JacobianChallenge/README.md. It builds only the divisor-class side Cl(X) of the later "Cl(X) ≅ Pic X" comparison: the Picard group and the equivalence to it are not constructed here, but are later geometric work, before the Picard functor and Picard scheme exist. The geometric ord_x (residue-field valuations of a function field) and the proof that a principal divisor has weighted degree zero are later geometric constructions; here both are abstracted to the data of an OrderSystem, a weight function, and the predicate IsWeightedDegreeZero.

No external mathematics is vendored. This reuses Tau Ceti's existing WeilDivisor API and Mathlib's Finsupp.ofSupportFinite (to assemble a finitely supported function from coordinatewise data) and QuotientAddGroup quotient machinery.

structure TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem (X : Type u_1) (G : Type u_2) [AddCommGroup G] : Type (max u_1 u_2)

An order system on a type of points X with values in a group G: a family of ℤ-valued homomorphisms ord x : G →+ ℤ, the orders of vanishing at each point, such that every g : G vanishes to nonzero order at only finitely many points.

Instantiate G with Additive Kˣ for the multiplicative group of a function field K: then ord x is the order of vanishing ord_x(f) of a rational function at the point x, and the finiteness condition records that a rational function has zeros and poles at only finitely many points. The principal divisor of f is Σ_x ord_x(f) · [x].

• ord : X → G →+ ℤ

  The order of vanishing at each point, as a homomorphism G →+ ℤ.

• finite_support (g : G) : (Function.support fun (x : X) => (self.ord x) g).Finite

  Each group element has nonzero order at only finitely many points.

noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.principalDivisor {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (g : G) : WeilDivisor X

The principal divisor Σ_x ord_x(g) · [x] attached to g : G.

Equations

• S.principalDivisor g = Finsupp.ofSupportFinite (fun (x : X) => (S.ord x) g) ⋯

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.coeff_principalDivisor {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (g : G) (x : X) : (S.principalDivisor g).coeff x = (S.ord x) g

noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.principalHom {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) : G →+ WeilDivisor X

Principal divisors as a homomorphism G →+ WeilDivisor X.

Equations

• S.principalHom = { toFun := S.principalDivisor, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.principalHom_apply {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (g : G) : S.principalHom g = S.principalDivisor g

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.principalDivisor_zero {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) : S.principalDivisor 0 = 0

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.principalDivisor_add {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (g₁ g₂ : G) : S.principalDivisor (g₁ + g₂) = S.principalDivisor g₁ + S.principalDivisor g₂

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.principalDivisor_neg {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (g : G) : S.principalDivisor (-g) = -S.principalDivisor g

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.principalDivisor_sub {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (g₁ g₂ : G) : S.principalDivisor (g₁ - g₂) = S.principalDivisor g₁ - S.principalDivisor g₂

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.principalDivisor_eq_of_ord_eq {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {T : OrderSystem X G} (hord : S.ord = T.ord) (g : G) : S.principalDivisor g = T.principalDivisor g

The principal-divisor construction depends only on the family of order homomorphisms, not on the proof that their supports are finite. This is the transport lemma used when a geometric order system is compared with an abstractly supplied one.

noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.principalSubgroup {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) : AddSubgroup (WeilDivisor X)

The subgroup of principal divisors.

Equations

• S.principalSubgroup = S.principalHom.range

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.mem_principalSubgroup {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {D : WeilDivisor X} : D ∈ S.principalSubgroup ↔ ∃ (g : G), S.principalDivisor g = D

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.principalSubgroup_eq_range {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) : S.principalSubgroup = S.principalHom.range

The subgroup of principal divisors is the range of the principal-divisor homomorphism.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.principalDivisor_mem_principalSubgroup {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (g : G) : S.principalDivisor g ∈ S.principalSubgroup

def TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.LinearlyEquivalent {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (D E : WeilDivisor X) : Prop

Two Weil divisors are linearly equivalent with respect to S when their difference is a principal divisor. This is the equivalence relation whose quotient is the divisor class group.

Equations

• S.LinearlyEquivalent D E = (D - E ∈ S.principalSubgroup)

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.linearlyEquivalent_iff {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {D E : WeilDivisor X} : S.LinearlyEquivalent D E ↔ D - E ∈ S.principalSubgroup

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.linearlyEquivalent_iff_exists_principalDivisor {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {D E : WeilDivisor X} : S.LinearlyEquivalent D E ↔ ∃ (g : G), S.principalDivisor g = D - E

Two Weil divisors are linearly equivalent exactly when their difference is the principal divisor of some g : G. This is the direct introduction/elimination form of LinearlyEquivalent, exposing the witnessing function.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.LinearlyEquivalent.refl {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (D : WeilDivisor X) : S.LinearlyEquivalent D D

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.LinearlyEquivalent.symm {X : Type u_1} {G : Type u_2} [AddCommGroup G] {S : OrderSystem X G} {D E : WeilDivisor X} (h : S.LinearlyEquivalent D E) : S.LinearlyEquivalent E D

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.LinearlyEquivalent.trans {X : Type u_1} {G : Type u_2} [AddCommGroup G] {S : OrderSystem X G} {D E F : WeilDivisor X} (h₁ : S.LinearlyEquivalent D E) (h₂ : S.LinearlyEquivalent E F) : S.LinearlyEquivalent D F

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.LinearlyEquivalent.add {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {D D' E E' : WeilDivisor X} (hD : S.LinearlyEquivalent D D') (hE : S.LinearlyEquivalent E E') : S.LinearlyEquivalent (D + E) (D' + E')

Linear equivalence is compatible with adding equivalent divisors on both sides.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.LinearlyEquivalent.add_right {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {D D' : WeilDivisor X} (hD : S.LinearlyEquivalent D D') (E : WeilDivisor X) : S.LinearlyEquivalent (D + E) (D' + E)

Adding the same divisor on the right preserves linear equivalence.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.LinearlyEquivalent.add_left {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {E E' : WeilDivisor X} (hE : S.LinearlyEquivalent E E') (D : WeilDivisor X) : S.LinearlyEquivalent (D + E) (D + E')

Adding the same divisor on the left preserves linear equivalence.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.linearlyEquivalent_add_principalDivisor {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (D : WeilDivisor X) (g : G) : S.LinearlyEquivalent (D + S.principalDivisor g) D

A divisor plus a principal divisor is linearly equivalent to the original divisor.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.linearlyEquivalent_sub_principalDivisor {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (D : WeilDivisor X) (g : G) : S.LinearlyEquivalent (D - S.principalDivisor g) D

Subtracting a principal divisor from a divisor is linearly equivalent to the original divisor.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.equivalence_linearlyEquivalent {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) : Equivalence S.LinearlyEquivalent

@[reducible, inline]

abbrev TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.ClassGroup {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) : Type u_1

The divisor class group Cl(X) = WeilDivisor X ⧸ (principal divisors) of an order system S.

Equations

• S.ClassGroup = (TauCeti.AlgebraicGeometry.WeilDivisor X ⧸ S.principalSubgroup)

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

The divisor class of a Weil divisor in the divisor class group.

Equations

• S.divisorClass = QuotientAddGroup.mk' S.principalSubgroup

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.divisorClass_eq_mk' {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (D : WeilDivisor X) : S.divisorClass D = (QuotientAddGroup.mk' S.principalSubgroup) D

The divisor-class map is the canonical additive quotient projection WeilDivisor X → Cl(X). This is the definitional equation, exposed so that downstream files can rewrite between divisorClass and QuotientAddGroup.mk'.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.divisorClass_surjective {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) : Function.Surjective ⇑S.divisorClass

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.divisorClass_principalDivisor {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (g : G) : S.divisorClass (S.principalDivisor g) = 0

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.divisorClass_eq_iff {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {D E : WeilDivisor X} : S.divisorClass D = S.divisorClass E ↔ S.LinearlyEquivalent D E

Two Weil divisors have the same divisor class exactly when they are linearly equivalent, that is, when their difference is a principal divisor.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.divisorClass_eq_zero_iff {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {D : WeilDivisor X} : S.divisorClass D = 0 ↔ D ∈ S.principalSubgroup

noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.ClassGroup.lift {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {H : Type u_3} [AddCommGroup H] (φ : WeilDivisor X →+ H) (hφ : ∀ (g : G), φ (S.principalDivisor g) = 0) : S.ClassGroup →+ H

The universal property of the divisor class group: a homomorphism φ : WeilDivisor X →+ H that sends every principal divisor to 0 descends to a homomorphism Cl(X) →+ H.

Equations

• TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.ClassGroup.lift S φ hφ = QuotientAddGroup.lift S.principalSubgroup φ ⋯

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.ClassGroup.lift_divisorClass {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {H : Type u_3} [AddCommGroup H] (φ : WeilDivisor X →+ H) (hφ : ∀ (g : G), φ (S.principalDivisor g) = 0) (D : WeilDivisor X) : (lift S φ hφ) (S.divisorClass D) = φ D

def TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.IsWeightedDegreeZero {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) : Prop

An order system has weighted-degree-zero principal divisors for a weight w : X → ℤ when every principal divisor has weighted degree zero.

For a smooth proper curve over a field k, the intended weight is the residue-field degree x ↦ [κ(x) : k]; this is the geometric fact that a rational function has as many zeros as poles, counted with residue-field degrees.

Equations

• S.IsWeightedDegreeZero w = ∀ (g : G), (TauCeti.AlgebraicGeometry.WeilDivisor.weightedDegree w) (S.principalDivisor g) = 0

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.isWeightedDegreeZero_congr_ord {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {T : OrderSystem X G} (hord : S.ord = T.ord) (w : X → ℤ) : S.IsWeightedDegreeZero w ↔ T.IsWeightedDegreeZero w

Weighted-degree-zero principal divisors are invariant under replacing an order system by one with the same order homomorphisms. In particular, an abstract contract can be discharged by the concrete geometric order system without identifying the finite-support proof fields.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.IsWeightedDegreeZero.principalSubgroup_le_weightedDegree_ker {X : Type u_1} {G : Type u_2} [AddCommGroup G] {S : OrderSystem X G} {w : X → ℤ} (h : S.IsWeightedDegreeZero w) : S.principalSubgroup ≤ (weightedDegree w).ker

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

When principal divisors have weighted degree zero, the weighted degree map descends to the divisor class group: linearly equivalent divisors have the same weighted degree.

Equations

• TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedDegreeClass w h = QuotientAddGroup.lift S.principalSubgroup (TauCeti.AlgebraicGeometry.WeilDivisor.weightedDegree w) ⋯

@[simp]

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

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

The weighted-degree-zero part of the divisor class group, the abstract Pic⁰ of the Jacobian roadmap: the kernel of the weighted degree map on divisor classes.

Equations

• TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.picZero w h = (TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedDegreeClass w h).ker

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.mem_picZero {X : Type u_1} {G : Type u_2} [AddCommGroup G] {S : OrderSystem X G} (w : X → ℤ) (h : S.IsWeightedDegreeZero w) {c : S.ClassGroup} : c ∈ picZero w h ↔ (weightedDegreeClass w h) c = 0

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.divisorClass_mem_picZero {X : Type u_1} {G : Type u_2} [AddCommGroup G] {S : OrderSystem X G} (w : X → ℤ) (h : S.IsWeightedDegreeZero w) {D : WeilDivisor X} : S.divisorClass D ∈ picZero w h ↔ (weightedDegree w) D = 0

The class of a Weil divisor lies in picZero exactly when that representative has weighted degree zero; the value is well defined because the weighted degree descends to the class.

def TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.IsUnweightedDegreeZero {X : Type u_1} {G : Type u_2} [AddCommGroup G] {S : OrderSystem X G} : Prop

An order system has unweighted-degree-zero principal divisors when every principal divisor has unweighted degree zero. This is the specialization of IsWeightedDegreeZero to the constant weight 1, appropriate for the algebraically closed/unweighted formal setting.

Equations

• TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.IsUnweightedDegreeZero = S.IsWeightedDegreeZero fun (x : X) => 1

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.IsUnweightedDegreeZero.principalSubgroup_le_ker {X : Type u_1} {G : Type u_2} [AddCommGroup G] {S : OrderSystem X G} (h : IsUnweightedDegreeZero) : S.principalSubgroup ≤ degree.ker

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

The unweighted degree map on divisor classes, for the algebraically closed/unweighted specialization: the descended degree weightedDegreeClass at the constant weight 1. For curves over a general field, use weightedDegreeClass.

Equations

• TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.unweightedDegreeClass h = TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedDegreeClass (fun (x : X) => 1) h

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.unweightedDegreeClass_divisorClass {X : Type u_1} {G : Type u_2} [AddCommGroup G] {S : OrderSystem X G} (h : IsUnweightedDegreeZero) (D : WeilDivisor X) : (unweightedDegreeClass h) (S.divisorClass D) = degree D