Fixed-degree positive and negative parts of a Weil divisor

This file packages the positive and negative parts of a formal Weil divisor as fixed-degree effective divisors. The order file proves that every formal divisor decomposes as D = D⁺ - D⁻, with both parts effective and with disjoint support. The fixed-degree divisor API, in turn, is the formal model for symmetric powers. The declarations here bridge those two layers by turning D⁺ and D⁻ into EffectiveDivisorOfDegree terms with their actual degrees as indices.

This is formal divisor bookkeeping for the Jacobian challenge roadmap's Layer A and Layer C: TauCetiRoadmap/JacobianChallenge/README.md, specifically "Divisors on a curve: Weil divisors ⊕_x ℤ", "Degree", and the symmetric-power prerequisite "Relative effective Cartier divisors and symmetric powers Symᵈ X". No external mathematics is vendored; the proofs reuse Tau Ceti's WeilDivisor.Order positive/negative-part API and the existing EffectiveDivisorOfDegree packaging.

Positive and negative parts

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.posPart {X : Type u_1} (D : WeilDivisor X) : EffectiveDivisorOfDegree X (degree D⁺).toNat

The positive part of a Weil divisor, packaged as an effective divisor of its own degree.

Equations

• TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.posPart D = ⟨D⁺, ⋯⟩

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.negPart {X : Type u_1} (D : WeilDivisor X) : EffectiveDivisorOfDegree X (degree D⁻).toNat

The negative part of a Weil divisor, packaged as an effective divisor of its own degree.

Equations

• TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.negPart D = ⟨D⁻, ⋯⟩

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.coe_posPart {X : Type u_1} (D : WeilDivisor X) : ↑(posPart D) = D⁺

The underlying Weil divisor of the packaged positive part is D⁺.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.coe_negPart {X : Type u_1} (D : WeilDivisor X) : ↑(negPart D) = D⁻

The underlying Weil divisor of the packaged negative part is D⁻.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.posPart_coe_of_isEffective {X : Type u_1} {d : ℕ} (D : EffectiveDivisorOfDegree X d) : posPart ↑D = (EffectiveDivisorOfDegree.cast ⋯) D

If a divisor is already effective, its packaged positive part is the divisor itself, up to the degree-index cast.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.negPart_coe_of_isEffective {X : Type u_1} {d : ℕ} (D : EffectiveDivisorOfDegree X d) : negPart ↑D = (EffectiveDivisorOfDegree.cast ⋯) (zero X)

If a divisor is effective, its packaged negative part is the zero divisor.

Point differences

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.posPart_pointDifference {X : Type u_1} {x y : X} (h : x ≠ y) : posPart (pointDifference x y) = (EffectiveDivisorOfDegree.cast ⋯) (ofSym (Sym.oneEquiv x))

For distinct points, the packaged positive part of [x] - [y] is [x].

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.negPart_pointDifference {X : Type u_1} {x y : X} (h : x ≠ y) : negPart (pointDifference x y) = (EffectiveDivisorOfDegree.cast ⋯) (ofSym (Sym.oneEquiv y))

For distinct points, the packaged negative part of [x] - [y] is [y].