The order on Weil divisors and the positive/negative part decomposition

This file continues the Jacobian roadmap's Layer A formal Weil divisor API (TauCeti.AlgebraicGeometry.WeilDivisor.Basic) by recording the lattice-ordered-group structure of formal divisors and the canonical decomposition of a divisor into its effective positive and negative parts.

The point set X →₀ ℤ already carries the coefficientwise partial order, the lattice operations ⊔/⊓, and (because ℤ is an ordered group) the lattice-ordered-group positive and negative parts D⁺ and D⁻ from Mathlib. The contribution here is to connect that order with the divisor vocabulary already in place: effectivity is nonnegativity, D ≤ E is effectivity of E - D, the pointwise maximum and minimum of effective divisors are effective, and every divisor decomposes as D = D⁺ - D⁻ with D⁺, D⁻ effective of disjoint support. We read off the consequences for the unweighted and weighted degree maps and compute the decomposition of the basic degree-zero divisors [x] - [y].

This reuses Mathlib's lattice-ordered-group posPart/negPart API (Mathlib.Algebra.Order.Group.PosPart) and the coefficientwise order and lattice on finitely supported functions (Mathlib.Order.Preorder.Finsupp, Mathlib.Data.Finsupp.Order); no external mathematics is vendored.

This advances the Tau Ceti Jacobian roadmap, Layer A, "Divisors on a curve: Weil divisors ⊕_x ℤ", "principal divisors", and "Degree".

The coefficientwise order

theorem TauCeti.AlgebraicGeometry.WeilDivisor.le_iff {X : Type u_1} {D E : WeilDivisor X} : D ≤ E ↔ ∀ (x : X), D.coeff x ≤ E.coeff x

One Weil divisor is ≤ another exactly when it is so coefficientwise.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.coeff_le_coeff {X : Type u_1} {D E : WeilDivisor X} (h : D ≤ E) (x : X) : D.coeff x ≤ E.coeff x

The coefficientwise order projects to coefficients: D ≤ E gives coeff D x ≤ coeff E x.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.zsmul_ofPoint_lt_zero {X : Type u_1} (x : X) {n : ℤ} (hn : n < 0) : n • ofPoint x < 0

A negative integer multiple of a point divisor is strictly negative.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.isEffective_iff_zero_le {X : Type u_1} {D : WeilDivisor X} : D.IsEffective ↔ 0 ≤ D

Effectivity is exactly nonnegativity in the coefficientwise order.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.le_add_ofPoint {X : Type u_1} (D : WeilDivisor X) (x : X) : D ≤ D + ofPoint x

Adding a point to a divisor gives a larger divisor.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.mem_effectiveSubmonoid_iff_zero_le {X : Type u_1} {D : WeilDivisor X} : D ∈ effectiveSubmonoid X ↔ 0 ≤ D

Membership in the effective submonoid is nonnegativity in the coefficientwise order.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.le_iff_isEffective_sub {X : Type u_1} {D E : WeilDivisor X} : D ≤ E ↔ (E - D).IsEffective

D ≤ E exactly when the difference E - D is effective.

Lattice operations

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.coeff_sup {X : Type u_1} (D E : WeilDivisor X) (x : X) : (D ⊔ E).coeff x = max (D.coeff x) (E.coeff x)

The coefficient of a pointwise maximum is the maximum of the coefficients.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.coeff_inf {X : Type u_1} (D E : WeilDivisor X) (x : X) : (D ⊓ E).coeff x = min (D.coeff x) (E.coeff x)

The coefficient of a pointwise minimum is the minimum of the coefficients.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.IsEffective.sup {X : Type u_1} {D E : WeilDivisor X} (hD : D.IsEffective) : (D ⊔ E).IsEffective

The pointwise maximum of an effective divisor with any divisor is effective.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.IsEffective.inf {X : Type u_1} {D E : WeilDivisor X} (hD : D.IsEffective) (hE : E.IsEffective) : (D ⊓ E).IsEffective

The pointwise minimum of two effective divisors is effective.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.isEffective_inf_iff {X : Type u_1} {D E : WeilDivisor X} : (D ⊓ E).IsEffective ↔ D.IsEffective ∧ E.IsEffective

A pointwise minimum is effective exactly when both divisors are effective.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.sub_inf_inf_sub_inf_eq_zero {X : Type u_1} (D E : WeilDivisor X) : (D - D ⊓ E) ⊓ (E - D ⊓ E) = 0

Removing the infimum from each of two Weil divisors leaves disjoint residual divisors.

Positive and negative parts

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.coeff_posPart {X : Type u_1} (D : WeilDivisor X) (x : X) : D⁺.coeff x = max (D.coeff x) 0

The coefficient of the positive part is the positive part of the coefficient.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.coeff_negPart {X : Type u_1} (D : WeilDivisor X) (x : X) : D⁻.coeff x = max (-D.coeff x) 0

The coefficient of the negative part is the negative part of the coefficient.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.isEffective_posPart {X : Type u_1} (D : WeilDivisor X) : D⁺.IsEffective

The positive part of a Weil divisor is effective.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.isEffective_negPart {X : Type u_1} (D : WeilDivisor X) : D⁻.IsEffective

The negative part of a Weil divisor is effective.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.support_posPart_disjoint_negPart {X : Type u_1} (D : WeilDivisor X) : Disjoint D⁺.support D⁻.support

The positive and negative parts of a Weil divisor have disjoint supports: no point carries both a positive and a negative coefficient.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.negPart_eq_zero_iff_isEffective {X : Type u_1} {D : WeilDivisor X} : D⁻ = 0 ↔ D.IsEffective

A divisor is effective exactly when its negative part vanishes.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.posPart_eq_self_iff_isEffective {X : Type u_1} {D : WeilDivisor X} : D⁺ = D ↔ D.IsEffective

A divisor is effective exactly when it equals its own positive part.

Degree of the decomposition

theorem TauCeti.AlgebraicGeometry.WeilDivisor.weightedDegree_posPart_sub_weightedDegree_negPart {X : Type u_1} (w : X → ℤ) (D : WeilDivisor X) : (weightedDegree w) D⁺ - (weightedDegree w) D⁻ = (weightedDegree w) D

The weighted degree splits over the positive/negative part decomposition.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.degree_posPart_sub_degree_negPart {X : Type u_1} (D : WeilDivisor X) : degree D⁺ - degree D⁻ = degree D

The unweighted degree splits over the positive/negative part decomposition.

The decomposition of a point difference

theorem TauCeti.AlgebraicGeometry.WeilDivisor.posPart_pointDifference {X : Type u_1} {x y : X} (h : x ≠ y) : (pointDifference x y)⁺ = ofPoint x

For distinct points the positive part of [x] - [y] is the point divisor [x].

theorem TauCeti.AlgebraicGeometry.WeilDivisor.negPart_pointDifference {X : Type u_1} {x y : X} (h : x ≠ y) : (pointDifference x y)⁻ = ofPoint y

For distinct points the negative part of [x] - [y] is the point divisor [y].