The maximal coefficient ideal as a finite sum

[Kol07, Definition 98] writes W_s(I) = ∑_{wt(e) ≥ s} ∏ⱼ (Dʲ I)^{eⱼ} as a sum over all exponent vectors e : Fin (m + 1) → ℕ of weight wt e = ∑ⱼ (m − j) eⱼ ≥ s; RegularCoords.W of Hironaka/Algebra/Local/Tuning.lean is that supremum. On an analytic manifold the sum has to be a locally finitely generated ideal sheaf, so this module shows that the supremum is a finite sum: it suffices to take the exponent vectors with eⱼ ≤ s for j < m and e_m = 0 (tuningExponents m s, iSup_wt_eq_sum_tuningExponents). Indeed, clamping e to e' = (min (eⱼ, s))_{j<m}, e'_m = 0 (clampExponent) keeps the weight ≥ s (if some eⱼ ≥ s with j < m, the single term (m − j) s ≥ s does; otherwise only the weightless e_m changed) and enlarges the product, since Pᵃ ⊆ Pᵇ for b ≤ a. The lemma holds for any family P : Fin (m + 1) → Ideal R of ideals of a commutative semiring; the Dʲ I play no role.

Used for the maximal coefficient ideal sheaf on manifolds (Hironaka/Manifold/IdealSheaf/Tuning.lean, Hironaka/Manifold/IdealSheaf/TuningLemmas.lean, Hironaka/Manifold/BlowUp/Transform/TuningTransform.lean). The statement is not in the sources.

def IsLocalRing.tuningExponents (m s : ℕ) : Finset (Fin (m + 1) → ℕ)

The exponent vectors that carry W_s: eⱼ ≤ s for j < m, e_m = 0, and wt e ≥ s.

Equations

• IsLocalRing.tuningExponents m s = {e ∈ Fintype.piFinset fun (x : Fin (m + 1)) => Finset.range (s + 1) | s ≤ IsLocalRing.wt m e ∧ e (Fin.last m) = 0}

theorem IsLocalRing.mem_tuningExponents {m s : ℕ} {e : Fin (m + 1) → ℕ} : e ∈ tuningExponents m s ↔ (∀ (j : Fin (m + 1)), e j ≤ s) ∧ s ≤ wt m e ∧ e (Fin.last m) = 0

def IsLocalRing.clampExponent (m s : ℕ) (e : Fin (m + 1) → ℕ) : Fin (m + 1) → ℕ

The clamp of an exponent vector at s, with the weightless last exponent set to 0.

Equations

• IsLocalRing.clampExponent m s e j = if j = Fin.last m then 0 else min (e j) s

theorem IsLocalRing.clampExponent_le (m s : ℕ) (e : Fin (m + 1) → ℕ) (j : Fin (m + 1)) : clampExponent m s e j ≤ e j

theorem IsLocalRing.wt_clampExponent_ge {m s : ℕ} {e : Fin (m + 1) → ℕ} (he : s ≤ wt m e) : s ≤ wt m (clampExponent m s e)

theorem IsLocalRing.clampExponent_mem_tuningExponents {m s : ℕ} {e : Fin (m + 1) → ℕ} (he : s ≤ wt m e) : clampExponent m s e ∈ tuningExponents m s

theorem IsLocalRing.prod_pow_le_prod_pow_of_le {R : Type u_1} [CommSemiring R] {ι : Type u_2} [Fintype ι] (P : ι → Ideal R) {e e' : ι → ℕ} (h : ∀ (j : ι), e' j ≤ e j) : ∏ j : ι, P j ^ e j ≤ ∏ j : ι, P j ^ e' j

Products of powers of ideals are antitone in the exponents.

theorem IsLocalRing.iSup_wt_eq_sum_tuningExponents {R : Type u_1} [CommSemiring R] (m s : ℕ) (P : Fin (m + 1) → Ideal R) : ⨆ (e : Fin (m + 1) → ℕ), ⨆ (_ : s ≤ wt m e), ∏ j : Fin (m + 1), P j ^ e j = ∑ e ∈ tuningExponents m s, ∏ j : Fin (m + 1), P j ^ e j

Kollár's sum over all exponent vectors of weight ≥ s is the finite sum over tuningExponents m s, for any family P of ideals.