Effective Weil divisors of fixed degree

This file packages the fixed-degree part of the effective Weil-divisor monoid. For a type of points X, the type EffectiveDivisorOfDegree X d consists of effective formal divisors of degree d. It is equivalent to Mathlib's symmetric power Sym X d, by reading a multiset as its finitely supported multiplicity function and conversely reading an effective divisor by its natural-number coefficients.

This is the formal divisor model behind the Jacobian roadmap's Layer C symmetric-power lane: the scheme-level construction of Symᵈ X and relative effective Cartier divisors is later geometry, but the Abel-map input already needs the divisor represented by an unordered degree-d collection of points.

This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer C, "Relative effective Cartier divisors and symmetric powers Symᵈ X", as a small prerequisite built from the existing Layer A WeilDivisor API. No external mathematics is vendored.

@[reducible, inline]

abbrev TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree (X : Type u_3) (d : ℕ) : Type u_3

The effective Weil divisors of degree d.

Equations

• TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree X d = { D : TauCeti.AlgebraicGeometry.WeilDivisor X // D.IsEffective ∧ TauCeti.AlgebraicGeometry.WeilDivisor.degree D = ↑d }

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.ext {X : Type u_1} {d : ℕ} {D E : EffectiveDivisorOfDegree X d} (h : ↑D = ↑E) : D = E

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.ext_iff {X : Type u_1} {d : ℕ} {D E : EffectiveDivisorOfDegree X d} : D = E ↔ ↑D = ↑E

@[reducible, inline]

abbrev TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.zero (X : Type u_3) : EffectiveDivisorOfDegree X 0

The zero effective divisor, regarded as the unique effective divisor of degree 0.

Equations

• TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.zero X = ⟨0, ⋯⟩

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.coe_zero {X : Type u_1} : ↑(zero X) = 0

The underlying Weil divisor of the degree-zero effective divisor is zero.

def TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.cast {X : Type u_1} {d e : ℕ} (h : d = e) : EffectiveDivisorOfDegree X d ≃ EffectiveDivisorOfDegree X e

Change the degree index of a fixed-degree effective divisor along an equality.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

Changing the degree index along rfl leaves a fixed-degree divisor unchanged.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.coe_cast {X : Type u_1} {d e : ℕ} (h : d = e) (D : EffectiveDivisorOfDegree X d) : ↑((EffectiveDivisorOfDegree.cast h) D) = ↑D

Changing the degree index does not change the underlying Weil divisor.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.isEffective {X : Type u_1} {d : ℕ} (D : EffectiveDivisorOfDegree X d) : (↑D).IsEffective

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.degree_eq {X : Type u_1} {d : ℕ} (D : EffectiveDivisorOfDegree X d) : degree ↑D = ↑d

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.mem_effectiveSubmonoid {X : Type u_1} {d : ℕ} (D : EffectiveDivisorOfDegree X d) : ↑D ∈ effectiveSubmonoid X

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.ofFinsupp {X : Type u_1} {d : ℕ} (m : X →₀ ℕ) (hm : (m.sum fun (x : X) (n : ℕ) => n) = d) : EffectiveDivisorOfDegree X d

An effective divisor of degree d from finitely supported natural multiplicities whose total multiplicity is d.

Equations

• TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.ofFinsupp m hm = ⟨TauCeti.AlgebraicGeometry.WeilDivisor.ofFinsupp m, ⋯⟩

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.coe_ofFinsupp {X : Type u_1} {d : ℕ} (m : X →₀ ℕ) (hm : (m.sum fun (x : X) (n : ℕ) => n) = d) : ↑(ofFinsupp m hm) = WeilDivisor.ofFinsupp m

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.coeff_ofFinsupp {X : Type u_1} {d : ℕ} (m : X →₀ ℕ) (hm : (m.sum fun (x : X) (n : ℕ) => n) = d) (x : X) : (↑(ofFinsupp m hm)).coeff x = ↑(m x)

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.multiplicityFinsupp {X : Type u_1} {d : ℕ} (D : EffectiveDivisorOfDegree X d) : X →₀ ℕ

The finitely supported natural multiplicity function underlying an effective divisor.

Equations

• D.multiplicityFinsupp = Finsupp.ofSupportFinite (fun (x : X) => ((↑D).coeff x).toNat) ⋯

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.multiplicityFinsupp_apply {X : Type u_1} {d : ℕ} (D : EffectiveDivisorOfDegree X d) (x : X) : D.multiplicityFinsupp x = ((↑D).coeff x).toNat

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.ofFinsupp_multiplicityFinsupp {X : Type u_1} {d : ℕ} (D : EffectiveDivisorOfDegree X d) : WeilDivisor.ofFinsupp D.multiplicityFinsupp = ↑D

Rebuilding an effective divisor from its natural multiplicity function recovers the underlying Weil divisor.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.sum_multiplicityFinsupp {X : Type u_1} {d : ℕ} (D : EffectiveDivisorOfDegree X d) : (D.multiplicityFinsupp.sum fun (x : X) (n : ℕ) => n) = d

The natural multiplicity function of a degree-d effective divisor has total mass d.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.ofFinsupp_multiplicityFinsupp_eq {X : Type u_1} {d : ℕ} (D : EffectiveDivisorOfDegree X d) : ofFinsupp D.multiplicityFinsupp ⋯ = D

Rebuilding an effective divisor from its natural multiplicity function recovers the original fixed-degree divisor.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.multiplicityFinsupp_ofFinsupp {X : Type u_1} {d : ℕ} (m : X →₀ ℕ) (hm : (m.sum fun (x : X) (n : ℕ) => n) = d) : (ofFinsupp m hm).multiplicityFinsupp = m

The natural multiplicity function of a divisor built from a finitely supported function is that function.

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.equivFinsupp {X : Type u_1} {d : ℕ} : EffectiveDivisorOfDegree X d ≃ { m : X →₀ ℕ // (m.sum fun (x : X) (n : ℕ) => n) = d }

Fixed-degree effective divisors are equivalently finitely supported natural multiplicities with total mass d.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.equivFinsupp_apply_coe {X : Type u_1} {d : ℕ} (D : EffectiveDivisorOfDegree X d) : ↑(equivFinsupp D) = D.multiplicityFinsupp

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.equivFinsupp_symm_apply {X : Type u_1} {d : ℕ} (m : { m : X →₀ ℕ // (m.sum fun (x : X) (n : ℕ) => n) = d }) : ↑(equivFinsupp.symm m) = WeilDivisor.ofFinsupp ↑m

noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.ofSym {X : Type u_1} {d : ℕ} (s : Sym X d) : EffectiveDivisorOfDegree X d

The effective divisor associated to an unordered degree-d collection of points.

Equations

• TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.ofSym s = TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.equivFinsupp.symm ((Sym.equivNatSum X d) s)

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.coe_ofSym {X : Type u_1} {d : ℕ} (s : Sym X d) : ↑(ofSym s) = WeilDivisor.ofFinsupp ↑((Sym.equivNatSum X d) s)

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.coeff_ofSym {X : Type u_1} {d : ℕ} (s : Sym X d) (x : X) : (↑(ofSym s)).coeff x = ↑(Multiset.count x ↑s)

The symmetric-power divisor has coefficient equal to the multiplicity of the point in the unordered collection.

noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.equivSym {X : Type u_1} {d : ℕ} : EffectiveDivisorOfDegree X d ≃ Sym X d

Effective degree-d divisors are the same data as the d-th symmetric power of the underlying point type.

Equations

• TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.equivSym = TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.equivFinsupp.trans (Sym.equivNatSum X d).symm

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.equivSym_apply {X : Type u_1} {d : ℕ} (D : EffectiveDivisorOfDegree X d) : equivSym D = (Sym.equivNatSum X d).symm (equivFinsupp D)

Applying the symmetric-power equivalence is the same as applying Mathlib's multiplicity equivalence to the fixed-degree divisor's multiplicity function.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.equivSym_symm_apply {X : Type u_1} {d : ℕ} (s : Sym X d) : equivSym.symm s = ofSym s

The inverse of the symmetric-power equivalence is ofSym.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.ofSym_equivSym {X : Type u_1} {d : ℕ} (D : EffectiveDivisorOfDegree X d) : ofSym (equivSym D) = D

Converting a divisor to the symmetric power and back gives the original divisor.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.equivSym_ofSym {X : Type u_1} {d : ℕ} (s : Sym X d) : equivSym (ofSym s) = s

Converting a symmetric-power point to a divisor and back gives the original symmetric-power point.

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.pushforward {X : Type u_1} {Y : Type u_2} {d : ℕ} (f : X → Y) (D : EffectiveDivisorOfDegree X d) : EffectiveDivisorOfDegree Y d

Pushing forward a fixed-degree effective divisor preserves its degree.

Equations

• TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.pushforward f D = ⟨(TauCeti.AlgebraicGeometry.WeilDivisor.pushforward f) ↑D, ⋯⟩

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.coe_pushforward {X : Type u_1} {Y : Type u_2} {d : ℕ} (f : X → Y) (D : EffectiveDivisorOfDegree X d) : ↑(pushforward f D) = (WeilDivisor.pushforward f) ↑D

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.pushforward_id {X : Type u_1} {d : ℕ} (D : EffectiveDivisorOfDegree X d) : pushforward (fun (x : X) => x) D = D

Pushing forward along the identity function is the identity on fixed-degree divisors.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.pushforward_comp {X : Type u_1} {Y : Type u_2} {d : ℕ} {Z : Type u_3} (g : Y → Z) (f : X → Y) (D : EffectiveDivisorOfDegree X d) : pushforward g (pushforward f D) = pushforward (g ∘ f) D

Pushforwards of fixed-degree divisors compose functorially.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.pushforward_ofFinsupp {X : Type u_1} {Y : Type u_2} {d : ℕ} (f : X → Y) (m : X →₀ ℕ) (hm : (m.sum fun (x : X) (n : ℕ) => n) = d) : pushforward f (ofFinsupp m hm) = ofFinsupp (Finsupp.mapDomain f m) ⋯

Pushing forward a divisor built from multiplicities corresponds to Finsupp.mapDomain.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.multiplicityFinsupp_pushforward {X : Type u_1} {Y : Type u_2} {d : ℕ} (f : X → Y) (D : EffectiveDivisorOfDegree X d) : (pushforward f D).multiplicityFinsupp = Finsupp.mapDomain f D.multiplicityFinsupp

The multiplicity function of a pushforward is the pushed-forward multiplicity function.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.equivSym_pushforward {X : Type u_1} {Y : Type u_2} {d : ℕ} (f : X → Y) (D : EffectiveDivisorOfDegree X d) : equivSym (pushforward f D) = Sym.map f (equivSym D)

The symmetric-power equivalence sends divisor pushforward to Sym.map.