Finite sums of point divisors

This file adds an API for the effective Weil divisors represented by finitely supported natural-number multiplicities and by named finite-set constructors. These are the formal Layer A divisor objects that later receive geometric restrictions from symmetric powers and relative effective divisors: before any scheme-level construction exists, a finite collection of points gives the divisor Σ nₓ[x].

The API records the coefficient, support, degree, weighted degree, pushforward, and degree-zero normal forms needed by the existing Abel-Jacobi and linear-system files.

This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer A, "Divisors on a curve: Weil divisors ⊕_x ℤ" and "Degree", and supplies a clean formal prerequisite for the Layer C/D Abel-map lane D ↦ 𝒪_X(D - d·x₀) from symmetric powers. No external mathematics is vendored; the proofs use Tau Ceti's WeilDivisor.ofPoint, degree, weightedDegree, and pushforward API together with Mathlib's finite-sum lemmas.

Finitely supported multiplicities

theorem TauCeti.AlgebraicGeometry.WeilDivisor.eq_sum_coeff_smul_ofPoint {X : Type u_1} (D : WeilDivisor X) : D = ∑ x ∈ D.support, D.coeff x • ofPoint x

Every Weil divisor is the finite sum of its coefficients times point divisors over its support.

noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.ofFinsupp {X : Type u_1} (m : X →₀ ℕ) : WeilDivisor X

The Weil divisor associated to finitely supported natural-number multiplicities.

Equations

• TauCeti.AlgebraicGeometry.WeilDivisor.ofFinsupp m = Finsupp.mapRange (fun (n : ℕ) => ↑n) TauCeti.AlgebraicGeometry.WeilDivisor.ofFinsupp._proof_1✝ m

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.coeff_ofFinsupp {X : Type u_1} (m : X →₀ ℕ) (x : X) : (ofFinsupp m).coeff x = ↑(m x)

Coefficients of the divisor from finitely supported natural multiplicities are the multiplicities.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.isEffective_ofFinsupp {X : Type u_1} (m : X →₀ ℕ) : (ofFinsupp m).IsEffective

Finitely supported natural multiplicities give effective divisors.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.support_ofFinsupp {X : Type u_1} (m : X →₀ ℕ) : (ofFinsupp m).support = m.support

The support of a divisor from finitely supported natural multiplicities is the support of those multiplicities.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.ofFinsupp_eq_sum {X : Type u_1} (m : X →₀ ℕ) : ofFinsupp m = ∑ x ∈ m.support, ↑(m x) • ofPoint x

A divisor from finitely supported multiplicities is the corresponding sum of point divisors over the support.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.degree_ofFinsupp {X : Type u_1} (m : X →₀ ℕ) : degree (ofFinsupp m) = ∑ x ∈ m.support, ↑(m x)

The degree of a divisor from finitely supported multiplicities is the sum over the support.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.weightedDegree_ofFinsupp {X : Type u_1} (w : X → ℤ) (m : X →₀ ℕ) : (weightedDegree w) (ofFinsupp m) = ∑ x ∈ m.support, ↑(m x) * w x

The weighted degree of a divisor from finitely supported multiplicities is the weighted sum over the support.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.pushforward_ofFinsupp {X : Type u_1} {Y : Type u_2} (f : X → Y) (m : X →₀ ℕ) : (pushforward f) (ofFinsupp m) = ∑ x ∈ m.support, ↑(m x) • ofPoint (f x)

Pushing forward a divisor from finitely supported multiplicities applies the map to each point in the support sum.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.weightedDegree_ofFinsupp_eq_zero_iff_of_pos {X : Type u_1} (m : X →₀ ℕ) {w : X → ℤ} (hw : ∀ x ∈ m.support, 0 < w x) : (weightedDegree w) (ofFinsupp m) = 0 ↔ m = 0

With positive weights on the support, a divisor from finitely supported multiplicities has weighted degree zero exactly when all multiplicities vanish.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.ofFinsupp_mem_weightedDegreeZeroSubgroup_iff_of_pos {X : Type u_1} (m : X →₀ ℕ) {w : X → ℤ} (hw : ∀ x ∈ m.support, 0 < w x) : ofFinsupp m ∈ weightedDegreeZeroSubgroup w ↔ m = 0

With positive weights on the support, a divisor from finitely supported multiplicities lies in the weighted degree-zero subgroup exactly when all multiplicities vanish.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.ofFinsupp_mem_degreeZeroSubgroup_iff {X : Type u_1} (m : X →₀ ℕ) : ofFinsupp m ∈ degreeZeroSubgroup X ↔ m = 0

A divisor from finitely supported multiplicities has unweighted degree zero exactly when all multiplicities vanish.

Named finite-set constructors

noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.ofFinsetWithMultiplicity {X : Type u_1} (s : Finset X) (m : X → ℕ) : WeilDivisor X

The Weil divisor supported on a finite set with prescribed natural multiplicities.

Equations

• TauCeti.AlgebraicGeometry.WeilDivisor.ofFinsetWithMultiplicity s m = Finsupp.indicator s fun (x : X) (x_1 : x ∈ s) => ↑(m x)

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.coeff_ofFinsetWithMultiplicity {X : Type u_1} [DecidableEq X] (s : Finset X) (m : X → ℕ) (x : X) : (ofFinsetWithMultiplicity s m).coeff x = ↑(if x ∈ s then m x else 0)

Coefficients of the named finite-set divisor with prescribed multiplicities.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.ofFinsetWithMultiplicity_eq_sum {X : Type u_1} (s : Finset X) (m : X → ℕ) : ofFinsetWithMultiplicity s m = ∑ x ∈ s, ↑(m x) • ofPoint x

The named finite-set divisor with multiplicities is the corresponding finite sum of point divisors.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.ofFinsetWithMultiplicity_empty {X : Type u_1} (m : X → ℕ) : ofFinsetWithMultiplicity ∅ m = 0

The named finite-set divisor with multiplicities over the empty set is zero.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.ofFinsetWithMultiplicity_insert {X : Type u_1} [DecidableEq X] {s : Finset X} {x : X} (hx : x ∉ s) (m : X → ℕ) : ofFinsetWithMultiplicity (insert x s) m = ↑(m x) • ofPoint x + ofFinsetWithMultiplicity s m

Inserting a new point in a named finite-set divisor splits off its weighted point divisor.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.isEffective_ofFinsetWithMultiplicity {X : Type u_1} (s : Finset X) (m : X → ℕ) : (ofFinsetWithMultiplicity s m).IsEffective

A named finite-set divisor with natural multiplicities is effective.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.ofFinsetWithMultiplicity_mem_effectiveSubmonoid {X : Type u_1} (s : Finset X) (m : X → ℕ) : ofFinsetWithMultiplicity s m ∈ effectiveSubmonoid X

A named finite-set divisor with natural multiplicities belongs to the effective divisor submonoid.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.support_ofFinsetWithMultiplicity_subset {X : Type u_1} (s : Finset X) (m : X → ℕ) : (ofFinsetWithMultiplicity s m).support ⊆ s

The support of a named finite-set divisor with multiplicities is contained in the chosen finite set. Points in the set whose multiplicity is zero may drop out of the support.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.mem_support_ofFinsetWithMultiplicity_iff {X : Type u_1} {s : Finset X} {m : X → ℕ} {x : X} : x ∈ (ofFinsetWithMultiplicity s m).support ↔ x ∈ s ∧ m x ≠ 0

A point is in the support of a named finite-set divisor with multiplicities exactly when it is selected and has nonzero multiplicity.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.degree_ofFinsetWithMultiplicity {X : Type u_1} (s : Finset X) (m : X → ℕ) : degree (ofFinsetWithMultiplicity s m) = ∑ x ∈ s, ↑(m x)

The degree of a named finite-set divisor with multiplicities is the sum of the multiplicities.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.weightedDegree_ofFinsetWithMultiplicity {X : Type u_1} (w : X → ℤ) (s : Finset X) (m : X → ℕ) : (weightedDegree w) (ofFinsetWithMultiplicity s m) = ∑ x ∈ s, ↑(m x) * w x

The weighted degree of a named finite-set divisor with multiplicities is the corresponding weighted finite sum.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.pushforward_ofFinsetWithMultiplicity {X : Type u_1} {Y : Type u_2} (f : X → Y) (s : Finset X) (m : X → ℕ) : (pushforward f) (ofFinsetWithMultiplicity s m) = ∑ x ∈ s, ↑(m x) • ofPoint (f x)

Pushing forward a named finite-set divisor with multiplicities applies the map to each point in the finite sum.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.weightedDegree_ofFinsetWithMultiplicity_eq_zero_iff_of_pos {X : Type u_1} (s : Finset X) {w : X → ℤ} (m : X → ℕ) (hw : ∀ x ∈ s, m x ≠ 0 → 0 < w x) : (weightedDegree w) (ofFinsetWithMultiplicity s m) = 0 ↔ ∀ x ∈ s, m x = 0

With positive weights at selected points with nonzero multiplicity, a named finite-set divisor has weighted degree zero exactly when every selected multiplicity vanishes.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.ofFinsetWithMultiplicity_mem_weightedDegreeZeroSubgroup_iff_of_pos {X : Type u_1} (s : Finset X) {w : X → ℤ} (m : X → ℕ) (hw : ∀ x ∈ s, m x ≠ 0 → 0 < w x) : ofFinsetWithMultiplicity s m ∈ weightedDegreeZeroSubgroup w ↔ ∀ x ∈ s, m x = 0

With positive weights at selected points with nonzero multiplicity, a named finite-set divisor lies in the weighted degree-zero subgroup exactly when all selected multiplicities vanish.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.ofFinsetWithMultiplicity_mem_degreeZeroSubgroup_iff {X : Type u_1} (s : Finset X) (m : X → ℕ) : ofFinsetWithMultiplicity s m ∈ degreeZeroSubgroup X ↔ ∀ x ∈ s, m x = 0

A named finite-set divisor with multiplicities has unweighted degree zero exactly when every selected multiplicity vanishes.

Named coefficient-one finite-set constructors

noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.ofFinset {X : Type u_1} (s : Finset X) : WeilDivisor X

The Weil divisor with coefficient 1 on each point of a finite set.

Equations

• TauCeti.AlgebraicGeometry.WeilDivisor.ofFinset s = TauCeti.AlgebraicGeometry.WeilDivisor.ofFinsetWithMultiplicity s fun (x : X) => 1

theorem TauCeti.AlgebraicGeometry.WeilDivisor.ofFinset_eq_sum {X : Type u_1} (s : Finset X) : ofFinset s = ∑ x ∈ s, ofPoint x

The named coefficient-one finite-set divisor is the corresponding finite sum of point divisors.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.ofFinset_empty {X : Type u_1} : ofFinset ∅ = 0

The named coefficient-one finite-set divisor over the empty set is zero.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.ofFinset_insert {X : Type u_1} [DecidableEq X] {s : Finset X} {x : X} (hx : x ∉ s) : ofFinset (insert x s) = ofPoint x + ofFinset s

Inserting a new point in a named coefficient-one finite-set divisor splits off its point divisor.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.coeff_ofFinset {X : Type u_1} [DecidableEq X] (s : Finset X) (x : X) : (ofFinset s).coeff x = if x ∈ s then 1 else 0

Coefficients of the named coefficient-one finite-set divisor are 1 on the set and 0 off it.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.isEffective_ofFinset {X : Type u_1} (s : Finset X) : (ofFinset s).IsEffective

The named coefficient-one finite-set divisor is effective.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.ofFinset_mem_effectiveSubmonoid {X : Type u_1} (s : Finset X) : ofFinset s ∈ effectiveSubmonoid X

The named coefficient-one finite-set divisor belongs to the effective divisor submonoid.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.support_ofFinset {X : Type u_1} (s : Finset X) : (ofFinset s).support = s

The support of the named coefficient-one finite-set divisor is exactly the chosen finite set.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.degree_ofFinset {X : Type u_1} (s : Finset X) : degree (ofFinset s) = ↑s.card

The degree of the named coefficient-one finite-set divisor is the finite set's cardinality.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.weightedDegree_ofFinset {X : Type u_1} (w : X → ℤ) (s : Finset X) : (weightedDegree w) (ofFinset s) = ∑ x ∈ s, w x

The weighted degree of the named coefficient-one finite-set divisor is the sum of weights on it.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.pushforward_ofFinset {X : Type u_1} {Y : Type u_2} (f : X → Y) (s : Finset X) : (pushforward f) (ofFinset s) = ∑ x ∈ s, ofPoint (f x)

Pushing forward the named coefficient-one finite-set divisor applies the map to each point.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.ofFinset_mem_weightedDegreeZeroSubgroup_iff_of_pos {X : Type u_1} (s : Finset X) {w : X → ℤ} (hw : ∀ x ∈ s, 0 < w x) : ofFinset s ∈ weightedDegreeZeroSubgroup w ↔ s = ∅

For positive weights, a named coefficient-one finite-set divisor lies in the weighted degree-zero subgroup exactly when the finite set is empty.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.ofFinset_mem_degreeZeroSubgroup_iff {X : Type u_1} (s : Finset X) : ofFinset s ∈ degreeZeroSubgroup X ↔ s = ∅

A named coefficient-one finite-set divisor has unweighted degree zero exactly when the set is empty.