Subtraction of fixed-degree effective Weil divisors

This file records the residual effective divisor obtained by subtracting an effective sub-divisor from a fixed-degree effective Weil divisor. If E ≤ D, with D of degree e and E of degree d, then D - E is effective of degree e - d. The cancellation lemmas show that adding the residual back recovers the original divisor, up to the unavoidable casts in the natural-number degree index.

This is formal divisor bookkeeping for the Jacobian challenge roadmap's Layer C symmetric-power lane (TauCetiRoadmap/JacobianChallenge/README.md, "Relative effective Cartier divisors and symmetric powers Symᵈ X"). The scheme-level construction is later geometry; this file supplies the elementary residual-divisor API used when separating a fixed effective base divisor from an unordered collection of points. No external mathematics is vendored.

noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.subOfLe {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X e) (E : EffectiveDivisorOfDegree X d) (hED : ↑E ≤ ↑D) : EffectiveDivisorOfDegree X (e - d)

The residual fixed-degree effective divisor D - E, defined when E ≤ D.

If D has degree e and E has degree d, the residual has degree e - d.

Equations

• D.subOfLe E hED = ⟨↑D - ↑E, ⋯⟩

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.coe_subOfLe {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X e) (E : EffectiveDivisorOfDegree X d) (hED : ↑E ≤ ↑D) : ↑(D.subOfLe E hED) = ↑D - ↑E

The underlying Weil divisor of a residual fixed-degree divisor is the difference of the underlying Weil divisors.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.coeff_subOfLe {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X e) (E : EffectiveDivisorOfDegree X d) (hED : ↑E ≤ ↑D) (x : X) : (↑(D.subOfLe E hED)).coeff x = (↑D).coeff x - (↑E).coeff x

The coefficient of a residual fixed-degree divisor is the difference of coefficients.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.multiplicityFinsupp_subOfLe {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X e) (E : EffectiveDivisorOfDegree X d) (hED : ↑E ≤ ↑D) : (D.subOfLe E hED).multiplicityFinsupp = D.multiplicityFinsupp - E.multiplicityFinsupp

The multiplicity function of a residual divisor is the truncated difference of the multiplicity functions.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.equivFinsupp_subOfLe_coe {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X e) (E : EffectiveDivisorOfDegree X d) (hED : ↑E ≤ ↑D) : ↑(equivFinsupp (D.subOfLe E hED)) = ↑(equivFinsupp D) - ↑(equivFinsupp E)

The finitely supported multiplicity representation of a residual divisor is the truncated difference of the representations of the original divisors.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.equivSym_subOfLe {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X e) (E : EffectiveDivisorOfDegree X d) (hED : ↑E ≤ ↑D) : equivSym (D.subOfLe E hED) = (Sym.equivNatSum X (e - d)).symm ⟨D.multiplicityFinsupp - E.multiplicityFinsupp, ⋯⟩

Under the symmetric-power equivalence, a residual divisor is represented by the truncated difference of multiplicity functions.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.degree_subOfLe {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X e) (E : EffectiveDivisorOfDegree X d) (hED : ↑E ≤ ↑D) : degree ↑(D.subOfLe E hED) = ↑(e - d)

The degree of the residual divisor is the difference of the degree indices.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.add_subOfLe {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X e) (E : EffectiveDivisorOfDegree X d) (hED : ↑E ≤ ↑D) : E.add (D.subOfLe E hED) = (EffectiveDivisorOfDegree.cast ⋯) D

Adding a sub-divisor back to its residual recovers the original divisor, up to the cast identifying d + (e - d) with e.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.subOfLe_add {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X e) (E : EffectiveDivisorOfDegree X d) (hED : ↑E ≤ ↑D) : (D.subOfLe E hED).add E = (EffectiveDivisorOfDegree.cast ⋯) D

Adding the residual on the left also recovers the original divisor, up to the cast identifying (e - d) + d with e.

@[simp]

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

Subtracting the zero fixed-degree divisor leaves the original divisor, up to the cast identifying d - 0 with d.

@[simp]

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

Subtracting a fixed-degree divisor from itself gives the zero residual divisor.