The union of two fixed-degree effective Weil divisors

This file packages the pointwise maximum of two effective fixed-degree Weil divisors as their union. If D and E are effective divisors, D ⊔ E is the smallest divisor lying above both; its coefficient at a point is the larger of the two multiplicities. This complements the common part D ⊓ E from TauCeti.AlgebraicGeometry.WeilDivisor.Common: the two are linked by the lattice-ordered-group inclusion–exclusion identity (D ⊓ E) + (D ⊔ E) = D + E, which at the level of degrees reads deg (D ⊓ E) + deg (D ⊔ E) = deg D + deg E.

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 Abel-map and linear-system arguments merge unordered effective divisors; where the common part D ⊓ E isolates the shared points, the union D ⊔ E records the combined support with the larger multiplicities, and the inclusion–exclusion identity converts between the two. This file supplies that operation at the existing formal Weil-divisor level, before scheme-level symmetric powers or relative Cartier divisors are available.

This reuses Mathlib's lattice-ordered commutative group identity inf_add_sup (Mathlib.Algebra.Order.Group.Lattice); no external mathematics is vendored.

noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.sup {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) : EffectiveDivisorOfDegree X (degree (↑D ⊔ ↑E)).toNat

The union of two fixed-degree effective divisors.

Its underlying Weil divisor is the pointwise maximum D ⊔ E; its degree index is the actual degree of that maximum.

Equations

• D.sup E = Classical.choose ⋯

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.coe_sup {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) : ↑(D.sup E) = ↑D ⊔ ↑E

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.coeff_sup {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) (x : X) : (↑(D.sup E)).coeff x = max ((↑D).coeff x) ((↑E).coeff x)

The coefficient of the union is the maximum of the two coefficients.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.multiplicityFinsupp_sup {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) : (D.sup E).multiplicityFinsupp = D.multiplicityFinsupp ⊔ E.multiplicityFinsupp

The multiplicity function of the union is the pointwise maximum of multiplicities.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.equivSym_sup {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) : equivSym (D.sup E) = (Sym.equivNatSum X (degree (↑D ⊔ ↑E)).toNat).symm ⟨D.multiplicityFinsupp ⊔ E.multiplicityFinsupp, ⋯⟩

The symmetric-power representative of the union is the pointwise maximum of multiplicity functions.

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

The left input divisor lies below the union.

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

The right input divisor lies below the union.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.sup_le {X : Type u_1} {d e : ℕ} {F : WeilDivisor X} {D : EffectiveDivisorOfDegree X d} {E : EffectiveDivisorOfDegree X e} (hDF : ↑D ≤ F) (hEF : ↑E ≤ F) : ↑(D.sup E) ≤ F

Any Weil divisor above both inputs lies above their union.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.sup_eq_left {X : Type u_1} {d e : ℕ} {D : EffectiveDivisorOfDegree X d} {E : EffectiveDivisorOfDegree X e} : ↑(D.sup E) = ↑D ↔ ↑E ≤ ↑D

The union is the left input exactly when the right input is below the left input.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.sup_eq_right {X : Type u_1} {d e : ℕ} {D : EffectiveDivisorOfDegree X d} {E : EffectiveDivisorOfDegree X e} : ↑(D.sup E) = ↑E ↔ ↑D ≤ ↑E

The union is the right input exactly when the left input is below the right input.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.sup_comm {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) : D.sup E = (EffectiveDivisorOfDegree.cast ⋯) (E.sup D)

The union is symmetric in its inputs, up to the natural degree-index cast.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.left_le_degree_sup {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) : d ≤ (degree (↑D ⊔ ↑E)).toNat

The left degree index is bounded above by the degree of the union.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.right_le_degree_sup {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) : e ≤ (degree (↑D ⊔ ↑E)).toNat

The right degree index is bounded above by the degree of the union.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.degree_inf_toNat_add_degree_sup_toNat {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) : (degree (↑D ⊓ ↑E)).toNat + (degree (↑D ⊔ ↑E)).toNat = d + e

Inclusion–exclusion on the degree indices: the degrees of the common part and the union sum to d + e.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.degree_sup_toNat {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) : (degree (↑D ⊔ ↑E)).toNat = d + e - (degree (↑D ⊓ ↑E)).toNat

The degree of the union is d + e minus the degree of the common part.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.inf_add_sup {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) : (D.inf E).add (D.sup E) = (EffectiveDivisorOfDegree.cast ⋯) (D.add E)

Inclusion–exclusion for fixed-degree effective divisors: the common part plus the union recover the sum of the two divisors, up to the natural degree-index cast.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.sup_add_inf {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) : (D.sup E).add (D.inf E) = (EffectiveDivisorOfDegree.cast ⋯) (D.add E)

The union plus the common part also recover the sum of the two divisors, up to the natural degree-index cast.