Degree and the divisor order

This file records the monotonicity of the formal Weil-divisor degree maps with respect to the coefficientwise order. If D ≤ E, then the effective difference E - D has nonnegative weighted degree whenever the weights are nonnegative, so weightedDegree w D ≤ weightedDegree w E. With positive weights this becomes strict unless D = E, and equality of degrees under a coefficientwise inequality forces equality of divisors.

These are Layer A divisor-and-degree facts for the Jacobian challenge roadmap (TauCetiRoadmap/JacobianChallenge/README.md): they are the order-theoretic counterpart of the existing effective-divisor positivity API and support later complete-linear-system and Abel-map bookkeeping. No external mathematics is vendored; the proofs reuse Tau Ceti's WeilDivisor.Order API and Mathlib's ordered-additive-group lemmas.

Weighted degree

theorem TauCeti.AlgebraicGeometry.WeilDivisor.weightedDegree_le_of_le_of_nonneg_on_support {X : Type u_1} {w : X → ℤ} {D E : WeilDivisor X} (hDE : D ≤ E) (hw : ∀ x ∈ (E - D).support, 0 ≤ w x) : (weightedDegree w) D ≤ (weightedDegree w) E

With nonnegative weights on the support of the difference, a coefficientwise increase does not decrease weighted degree.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.weightedDegree_le_of_le {X : Type u_1} {w : X → ℤ} (hw : ∀ (x : X), 0 ≤ w x) {D E : WeilDivisor X} (hDE : D ≤ E) : (weightedDegree w) D ≤ (weightedDegree w) E

With nonnegative weights, weighted degree is monotone for the coefficientwise divisor order.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.monotone_weightedDegree {X : Type u_1} {w : X → ℤ} (hw : ∀ (x : X), 0 ≤ w x) : Monotone ⇑(weightedDegree w)

Bundled monotonicity of weighted degree for nonnegative weights.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.weightedDegree_lt_of_le_of_ne_of_pos_on_support {X : Type u_1} {w : X → ℤ} {D E : WeilDivisor X} (hDE : D ≤ E) (hne : D ≠ E) (hw : ∀ x ∈ (E - D).support, 0 < w x) : (weightedDegree w) D < (weightedDegree w) E

With positive weights on the support of the difference, a proper coefficientwise increase strictly increases weighted degree.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.weightedDegree_lt_of_le_of_ne_of_pos {X : Type u_1} {w : X → ℤ} (hw : ∀ (x : X), 0 < w x) {D E : WeilDivisor X} (hDE : D ≤ E) (hne : D ≠ E) : (weightedDegree w) D < (weightedDegree w) E

With everywhere-positive weights, a proper coefficientwise increase strictly increases weighted degree.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.weightedDegree_lt_of_lt_of_pos {X : Type u_1} {w : X → ℤ} (hw : ∀ (x : X), 0 < w x) {D E : WeilDivisor X} (hDE : D < E) : (weightedDegree w) D < (weightedDegree w) E

With everywhere-positive weights, strict coefficientwise inequality strictly increases weighted degree.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.eq_of_le_of_weightedDegree_eq_of_pos_on_support {X : Type u_1} {w : X → ℤ} {D E : WeilDivisor X} (hDE : D ≤ E) (hdeg : (weightedDegree w) D = (weightedDegree w) E) (hw : ∀ x ∈ (E - D).support, 0 < w x) : D = E

With positive weights on the support of the difference, equality of weighted degrees under a coefficientwise inequality forces equality of divisors.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.eq_of_le_of_weightedDegree_eq_of_pos {X : Type u_1} {w : X → ℤ} (hw : ∀ (x : X), 0 < w x) {D E : WeilDivisor X} (hDE : D ≤ E) (hdeg : (weightedDegree w) D = (weightedDegree w) E) : D = E

With everywhere-positive weights, equality of weighted degrees under a coefficientwise inequality forces equality of divisors.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.IsEffective.exists_eq_ofPoint_of_weightedDegree_eq_one {X : Type u_1} {w : X → ℤ} {D : WeilDivisor X} (hD : D.IsEffective) (hw : ∀ x ∈ D.support, 0 < w x) (hdeg : (weightedDegree w) D = 1) : ∃ (x : X), w x = 1 ∧ D = ofPoint x

An effective divisor of weighted degree one is a point divisor: with positive weights on its support, weightedDegree w D = 1 forces D = [x] at a single point x of weight one.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.strictMono_weightedDegree {X : Type u_1} {w : X → ℤ} (hw : ∀ (x : X), 0 < w x) : StrictMono ⇑(weightedDegree w)

For positive weights, weighted degree is strictly monotone for the coefficientwise divisor order.

Unweighted degree

theorem TauCeti.AlgebraicGeometry.WeilDivisor.degree_le_of_le {X : Type u_1} {D E : WeilDivisor X} (hDE : D ≤ E) : degree D ≤ degree E

The unweighted degree is monotone for the coefficientwise divisor order.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.monotone_degree {X : Type u_1} : Monotone ⇑degree

Bundled monotonicity of unweighted degree.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.degree_lt_of_le_of_ne {X : Type u_1} {D E : WeilDivisor X} (hDE : D ≤ E) (hne : D ≠ E) : degree D < degree E

A proper coefficientwise increase strictly increases unweighted degree.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.degree_lt_of_lt {X : Type u_1} {D E : WeilDivisor X} (hDE : D < E) : degree D < degree E

Strict coefficientwise inequality strictly increases unweighted degree.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.eq_of_le_of_degree_eq {X : Type u_1} {D E : WeilDivisor X} (hDE : D ≤ E) (hdeg : degree D = degree E) : D = E

Equality of unweighted degrees under a coefficientwise inequality forces equality of divisors.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.strictMono_degree {X : Type u_1} : StrictMono ⇑degree

The unweighted degree is strictly monotone for the coefficientwise divisor order.

Inclusion–exclusion at the level of degrees

theorem TauCeti.AlgebraicGeometry.WeilDivisor.degree_inf_add_degree_sup {X : Type u_1} (D E : WeilDivisor X) : degree (D ⊓ E) + degree (D ⊔ E) = degree D + degree E

The lattice-ordered-group inclusion–exclusion identity for the unweighted degree: deg (D ⊓ E) + deg (D ⊔ E) = deg D + deg E.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.weightedDegree_inf_add_weightedDegree_sup {X : Type u_1} (w : X → ℤ) (D E : WeilDivisor X) : (weightedDegree w) (D ⊓ E) + (weightedDegree w) (D ⊔ E) = (weightedDegree w) D + (weightedDegree w) E

The lattice-ordered-group inclusion–exclusion identity for the weighted degree: w-deg (D ⊓ E) + w-deg (D ⊔ E) = w-deg D + w-deg E.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.degree_le_of_le {X : Type u_1} {d e : ℕ} {D : EffectiveDivisorOfDegree X d} {E : EffectiveDivisorOfDegree X e} (hDE : ↑D ≤ ↑E) : d ≤ e

If a fixed-degree effective divisor is coefficientwise below another, its degree index is also bounded above.