Common parts of fixed-degree effective Weil divisors

This file packages the pointwise minimum of two effective fixed-degree Weil divisors as their common effective part. If D and E are effective divisors, D ⊓ E is the largest divisor lying below both. Removing it from D and from E gives two residual effective divisors with disjoint support.

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 later Abel-map and linear-system arguments need to split unordered effective divisors into their common sub-divisor and the two remaining parts; this file supplies that operation at the existing formal Weil-divisor level, before scheme-level symmetric powers or relative Cartier divisors are available.

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

The common effective part of two fixed-degree effective divisors.

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

Equations

• D.inf E = Classical.choose ⋯

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.coe_inf {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) : ↑(D.inf E) = ↑D ⊓ ↑E

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.coeff_inf {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) (x : X) : (↑(D.inf E)).coeff x = min ((↑D).coeff x) ((↑E).coeff x)

The coefficient of the common part is the minimum of the two coefficients.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.multiplicityFinsupp_inf {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) : (D.inf E).multiplicityFinsupp = D.multiplicityFinsupp ⊓ E.multiplicityFinsupp

The multiplicity function of the common part is the pointwise minimum of multiplicities.

@[simp]

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

The symmetric-power representative of the common part is the pointwise minimum of multiplicity functions.

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

The common part lies below the left input divisor.

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

The common part lies below the right input divisor.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.le_inf {X : Type u_1} {d e : ℕ} {F : WeilDivisor X} {D : EffectiveDivisorOfDegree X d} {E : EffectiveDivisorOfDegree X e} (hFD : F ≤ ↑D) (hFE : F ≤ ↑E) : F ≤ ↑(D.inf E)

Any Weil divisor below both inputs lies below their common part.

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

The common part is the left input exactly when the left input is below the right input.

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

The common part is the right input exactly when the right input is below the left input.

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

The degree of the common part is bounded by the left degree index.

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

The degree of the common part is bounded by the right degree index.

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

The residual part of the left divisor after removing the common part.

It is the fixed-degree difference D - (D ⊓ E), available since the common part lies below D.

Equations

• D.leftResidual E = D.subOfLe (D.inf E) ⋯

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

The residual part of the right divisor after removing the common part.

It is the fixed-degree difference E - (D ⊓ E), available since the common part lies below E.

Equations

• D.rightResidual E = E.subOfLe (D.inf E) ⋯

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.coe_leftResidual {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) : ↑(D.leftResidual E) = ↑D - ↑(D.inf E)

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.coe_rightResidual {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) : ↑(D.rightResidual E) = ↑E - ↑(D.inf E)

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.coeff_leftResidual {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) (x : X) : (↑(D.leftResidual E)).coeff x = (↑D).coeff x - min ((↑D).coeff x) ((↑E).coeff x)

The coefficient of the left residual is coeff D x - min (coeff D x) (coeff E x).

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.coeff_rightResidual {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) (x : X) : (↑(D.rightResidual E)).coeff x = (↑E).coeff x - min ((↑D).coeff x) ((↑E).coeff x)

The coefficient of the right residual is coeff E x - min (coeff D x) (coeff E x).

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.multiplicityFinsupp_leftResidual {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) : (D.leftResidual E).multiplicityFinsupp = D.multiplicityFinsupp - (D.inf E).multiplicityFinsupp

The multiplicity function of the left residual is the truncated multiplicity difference.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.multiplicityFinsupp_rightResidual {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) : (D.rightResidual E).multiplicityFinsupp = E.multiplicityFinsupp - (D.inf E).multiplicityFinsupp

The multiplicity function of the right residual is the truncated multiplicity difference.

@[simp]

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

The symmetric-power representative of the left residual is the truncated multiplicity difference from the left divisor.

@[simp]

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

The symmetric-power representative of the right residual is the truncated multiplicity difference from the right divisor.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.leftResidual_inf_rightResidual_eq_zero {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) : ↑(D.leftResidual E) ⊓ ↑(D.rightResidual E) = 0

The two residual divisors left after removing the common part are coefficientwise disjoint.

@[simp]

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

Removing the common part from the left divisor and adding it back recovers the left divisor, up to the natural degree-index cast.

@[simp]

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

Adding the common part before the left residual also recovers the left divisor, up to the natural degree-index cast.

@[simp]

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

Removing the common part from the right divisor and adding it back recovers the right divisor, up to the natural degree-index cast.

@[simp]

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

Adding the common part before the right residual also recovers the right divisor, up to the natural degree-index cast.