Maximal coefficient ideals

[Kol07, Definition 98]: for an ideal I with m = max-ord I, the maximal coefficient ideal of order s is W_s(I) = ∑ { ∏ⱼ (Dʲ I)^{cⱼ} : ∑ⱼ (m − j) cⱼ ≥ s }, the sum over all exponent vectors c : {0, …, m} → ℕ of weight at least s. Here R is a regular local ring containing ℚ with coordinates (RegularCoords), Dʲ its iterated derivative ideals (Hironaka/Algebra/Local/Derivative.lean), and the parameter m is explicit: c.W m s I, with the weight wt m c. The module proves the local forms of [Kol07, Proposition 99] and of its Claim 99.9:

• W_0(I) = R; Iᵏ ≤ W_s(I) for m k ≥ s (pow_le_W); MC_m(I)ˢ ≤ W_s(I) (MC_pow_le_W); W_1(I) = MC_m(I) for m ≥ 1 (W_one); W_s(I) = R when ord I < m (W_eq_top_of_ord_lt);
• (99.1) W_{s+1}(I) ≤ W_s(I) and (99.2) W_s(I) · W_t(I) ≤ W_{s+t}(I) (W_succ_le, W_mul_le);
• (99.3) D(W_{s+1}(I)) = W_s(I) for ord I ≤ m, m ≥ 1 (D_W_succ: the inclusion ≤ by the product rule; the reverse by Kollár's argument with an element x₁ ∈ MC_m(I) of order 1 and a derivation ∂ with ∂ x₁ = 1, showing x₁^{s−t} W_t(I) ≤ D(W_{s+1}(I)) by induction on t), and its iterate Dⁱ(W_s(I)) = W_{s−i}(I) (Dpow_W);
• the order: ord W_s(I) = s when ord I = m ≥ 1 (ord_W; for s = m! this is [Kol07, Theorem 54.2 (i)]), and s ≤ ord W_s(I) ↔ m ≤ ord I for s ≥ 1 (le_ord_W_iff: the cosupports of (W_s(I), s) and (I, m) agree);
• (99.4) MC_s(W_s(I)) = W_1(I) = MC_m(I) (MC_W) and (99.5) W_s(I) is MC-invariant (isMCInvariant_W);
• Claim 99.9 in the weight language (exists_le_wt_eq: every exponent vector of weight ≥ (r + m − 1) L_m, with L_m = lcm(2, …, m), has a sub-vector of weight exactly r L_m) and its consequences (99.6) W_s(I) · W_t(I) = W_{s+t}(I) for s = r L_m and t ≥ (m − 1) L_m (W_mul_W_eq), (99.7) W_s(I)ʲ = W_{js}(I) for s = r L_m, r ≥ m − 1 (W_pow), and (99.8) W_s(I) is D-balanced for such s (isDBalanced_W).

Conventions: indices are zero-based; MC_m(I) = D^{m−1}(I) is the maximal-contact ideal of Hironaka/Algebra/Local/MaximalContact.lean; D-balanced and MC-invariant are IsDBalanced (Hironaka/Algebra/Local/Balanced.lean) and IsMCInvariant (Hironaka/Algebra/Local/MaximalContact.lean).

Used for the maximal coefficient ideal sheaf and Theorem 100 (Hironaka/Resolution/Algebraic/Tuning/Sheaf.lean, Hironaka/Resolution/Algebraic/Tuning/Cosupport.lean, Hironaka/Resolution/Algebraic/Tuning/MCTuned.lean, Hironaka/Resolution/Algebraic/Tuning/Corollary101.lean, Hironaka/Resolution/Algebraic/Tuning/Parameter.lean), for the tuning parameter (Hironaka/Algebra/Local/TuningParam.lean) and on manifolds (Hironaka/Manifold/IdealSheaf/TuningLemmas.lean).

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

The weight ∑ⱼ (m − j) cⱼ of an exponent vector c : {0, …, m} → ℕ ([Kol07, Definition 98]).

Equations

• IsLocalRing.wt m e = ∑ j : Fin (m + 1), (m - ↑j) * e j

theorem IsLocalRing.wt_add (m : ℕ) (e e' : Fin (m + 1) → ℕ) : wt m (e + e') = wt m e + wt m e'

theorem IsLocalRing.wt_single (m : ℕ) (j : Fin (m + 1)) (k : ℕ) : wt m (Pi.single j k) = (m - ↑j) * k

Claim 99.9

def IsLocalRing.Lcm (m : ℕ) : ℕ

L_m = lcm(2, …, m), with L_1 = 1 ([Kol07, Claim 99.9]).

Equations

• IsLocalRing.Lcm m = (Finset.Icc 2 m).lcm id

theorem IsLocalRing.Lcm_pos (m : ℕ) : 0 < Lcm m

theorem IsLocalRing.dvd_Lcm {m w : ℕ} (h1 : 1 ≤ w) (h2 : w ≤ m) : w ∣ Lcm m

Every w with 1 ≤ w ≤ m divides L_m.

theorem IsLocalRing.exists_le_sum_eq {ι : Type u_1} [Fintype ι] (b : ι → ℕ) (r : ℕ) (hr : r ≤ ∑ i : ι, b i) : ∃ d ≤ b, ∑ i : ι, d i = r

A vector bounded by b with a prescribed sum r ≤ ∑ b (Kollár's "choose 0 ≤ dᵢ ≤ bᵢ such that ∑ dᵢ = r" in the proof of Claim 99.9).

theorem IsLocalRing.exists_le_wt_eq {m : ℕ} (hm : 1 ≤ m) (r : ℕ) {e : Fin (m + 1) → ℕ} (he : (r + m - 1) * Lcm m ≤ wt m e) : ∃ e' ≤ e, wt m e' = r * Lcm m

[Kol07, Claim 99.9] in the weight language of Definition 98 (Kollár's variable uᵢ of degree i is D^{m−i} I, dᵢ = c_{m−i}, deg d = wt_m c; the index m, of weight 0, is ignored): every exponent vector e with wt e ≥ (r + m − 1) L_m has a sub-vector e' ≤ e with wt e' = r L_m. Proof as Kollár's: write eⱼ = bⱼ (L_m/wⱼ) + fⱼ with wⱼ fⱼ < L_m (wⱼ = m − j); if ∑ bⱼ ≥ r pick d ≤ b with ∑ d = r and e'ⱼ = dⱼ L_m/wⱼ; otherwise wt e < (r − 1) L_m + m L_m, a contradiction.

def IsLocalRing.RegularCoords.W {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (m s : ℕ) (I : Ideal R) : Ideal R

The maximal coefficient ideal of order s ([Kol07, Definition 98]), W_s(I) = ∑_{wt c ≥ s} ∏ⱼ (Dʲ I)^{cⱼ}, with the parameter m (Kollár's max-ord I) explicit.

Equations

• c.W m s I = ⨆ (e : Fin (m + 1) → ℕ), ⨆ (_ : s ≤ IsLocalRing.wt m e), ∏ j : Fin (m + 1), c.Dpow (↑j) I ^ e j

theorem IsLocalRing.RegularCoords.prod_le_W {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {m s : ℕ} {e : Fin (m + 1) → ℕ} (he : s ≤ wt m e) (I : Ideal R) : ∏ j : Fin (m + 1), c.Dpow (↑j) I ^ e j ≤ c.W m s I

theorem IsLocalRing.RegularCoords.W_le_iff {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {m s : ℕ} {I J : Ideal R} : c.W m s I ≤ J ↔ ∀ (e : Fin (m + 1) → ℕ), s ≤ wt m e → ∏ j : Fin (m + 1), c.Dpow (↑j) I ^ e j ≤ J

@[simp]

theorem IsLocalRing.RegularCoords.W_zero {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (m : ℕ) (I : Ideal R) : c.W m 0 I = ⊤

W_0(I) = R.

theorem IsLocalRing.RegularCoords.pow_le_W {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {m s k : ℕ} (h : s ≤ m * k) (I : Ideal R) : I ^ k ≤ c.W m s I

Iᵏ ≤ W_s(I) whenever m k ≥ s.

theorem IsLocalRing.RegularCoords.pow_ceil_le_W {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {m s : ℕ} (hm : 1 ≤ m) (I : Ideal R) : I ^ ((s + m - 1) / m) ≤ c.W m s I

I^⌈s/m⌉ ≤ W_s(I) for m ≥ 1.

theorem IsLocalRing.RegularCoords.MC_pow_le_W {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {m : ℕ} (hm : 1 ≤ m) (s : ℕ) (I : Ideal R) : c.MC I m ^ s ≤ c.W m s I

MC_m(I)ˢ ≤ W_s(I): the exponent vector c_{m−1} = s has weight s (Kollár's x₁^{s+1} ∈ W_{s+1}(I) in the proof of [Kol07, Proposition 99]).

theorem IsLocalRing.RegularCoords.pow_mem_W {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {m : ℕ} (hm : 1 ≤ m) {s : ℕ} {I : Ideal R} {h : R} (hh : h ∈ c.MC I m) : h ^ s ∈ c.W m s I

hˢ ∈ W_s(I) for h ∈ MC_m(I).

theorem IsLocalRing.RegularCoords.W_one {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {m : ℕ} (hm : 1 ≤ m) (I : Ideal R) : c.W m 1 I = c.MC I m

W_1(I) = D^{m−1} I = MC_m(I) for m ≥ 1 (the proof of (99.4) in [Kol07, Proposition 99]).

theorem IsLocalRing.RegularCoords.W_eq_top_of_ord_lt {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {m : ℕ} (hm : 1 ≤ m) {I : Ideal R} (h : ord I < ↑m) (s : ℕ) : c.W m s I = ⊤

If ord I < m then W_s(I) = R for every s, since MC_m(I) = R ([Kol07, Lemma 74 (3)] locally).

Proposition 99 (1)–(3)

theorem IsLocalRing.RegularCoords.W_anti {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {m s t : ℕ} (h : s ≤ t) (I : Ideal R) : c.W m t I ≤ c.W m s I

theorem IsLocalRing.RegularCoords.W_succ_le {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (m s : ℕ) (I : Ideal R) : c.W m (s + 1) I ≤ c.W m s I

[Kol07, (99.1)]: W_{s+1}(I) ≤ W_s(I).

theorem IsLocalRing.RegularCoords.W_mul_le {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (m s t : ℕ) (I : Ideal R) : c.W m s I * c.W m t I ≤ c.W m (s + t) I

[Kol07, (99.2)]: W_s(I) · W_t(I) ≤ W_{s+t}(I).

theorem IsLocalRing.RegularCoords.Dpow_pow_le_W {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (m : ℕ) (j : Fin (m + 1)) (k : ℕ) (I : Ideal R) : c.Dpow (↑j) I ^ k ≤ c.W m ((m - ↑j) * k) I

A single generator: (Dʲ I)^k ≤ W_{(m-j)k}(I).

theorem IsLocalRing.RegularCoords.Dpow_le_W_of_le {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {m j : ℕ} (hj : j ≤ m) (I : Ideal R) : c.Dpow j I ≤ c.W m (m - j) I

theorem IsLocalRing.RegularCoords.D_Dpow_le_W {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (m : ℕ) (j : Fin (m + 1)) (I : Ideal R) : c.D (c.Dpow (↑j) I) ≤ c.W m (m - ↑j - 1) I

theorem IsLocalRing.RegularCoords.D_Dpow_pow_le_W {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (m : ℕ) (j : Fin (m + 1)) (k : ℕ) (I : Ideal R) : c.D (c.Dpow (↑j) I ^ k) ≤ c.W m ((m - ↑j) * k - 1) I

The product rule for one generator: D((Dʲ I)^k) ≤ W_{(m-j)k - 1}(I).

theorem IsLocalRing.RegularCoords.prod_le_W_sum {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (m : ℕ) (s : Finset (Fin (m + 1))) (e : Fin (m + 1) → ℕ) (I : Ideal R) : ∏ l ∈ s, c.Dpow (↑l) I ^ e l ≤ c.W m (∑ l ∈ s, (m - ↑l) * e l) I

A product of generators lies in W of its weight.

theorem IsLocalRing.RegularCoords.D_prod_le_W {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (m : ℕ) (s : Finset (Fin (m + 1))) (e : Fin (m + 1) → ℕ) (I : Ideal R) : c.D (∏ l ∈ s, c.Dpow (↑l) I ^ e l) ≤ c.W m (∑ l ∈ s, (m - ↑l) * e l - 1) I

The product rule for a product of generators (Kollár's "follows from the product rule" in the proof of [Kol07, Proposition 99]): D(∏ (Dˡ I)^{eₗ}) ≤ W_{wt(e) − 1}(I).

theorem IsLocalRing.RegularCoords.D_W_succ_le {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (m s : ℕ) (I : Ideal R) : c.D (c.W m (s + 1) I) ≤ c.W m s I

The inclusion ⊆ of [Kol07, (99.3)], by the product rule: D(W_{s+1}(I)) ≤ W_s(I).

theorem IsLocalRing.RegularCoords.exists_isUnit_pderiv {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {h : R} (hh : h ∈ maximalIdeal R) (hh' : h ∉ maximalIdeal R ^ 2) : ∃ (i : Fin n), IsUnit ((c.pderiv i) h)

An element of 𝔪 ∖ 𝔪² has a coordinate partial that is a unit (the contrapositive of mem_maximalIdeal_sq_of_pderiv_mem, Hironaka/Algebra/Local/Coords.lean): Kollár's ∂/∂x₁ in the proof of [Kol07, Proposition 99] is u⁻¹ ∂ᵢ for such an i, with ∂ᵢ x₁ = u.

theorem IsLocalRing.RegularCoords.exists_maximalContact_deriv {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {I : Ideal R} {m : ℕ} (hm : 1 ≤ m) (hI : ord I = ↑m) : ∃ h ∈ c.MC I m, ordElem h = 1 ∧ ∃ (δ : Derivation ℚ R R), δ h = 1 ∧ ∀ (J : Ideal R), ∀ f ∈ J, δ f ∈ c.D J

Kollár's "Pick x₁ ∈ MC(I) that has order 1" (the proof of [Kol07, Proposition 99]): for ord I = m ≥ 1 there are x₁ ∈ MC_m(I) of order 1 and a derivation ∂ with ∂ x₁ = 1 mapping every ideal J into D J, namely ∂ = u⁻¹ ∂ᵢ for an i with ∂ᵢ x₁ = u a unit. No hypothesis that the ∂ᵢ span the derivations is needed.

theorem IsLocalRing.RegularCoords.pow_mem_D_W_succ {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {m : ℕ} (hm : 1 ≤ m) {I : Ideal R} {h : R} (hh : h ∈ c.MC I m) {δ : Derivation ℚ R R} (h1 : δ h = 1) (hD : ∀ (J : Ideal R), ∀ f ∈ J, δ f ∈ c.D J) (s : ℕ) : h ^ s ∈ c.D (c.W m (s + 1) I)

(The proof of [Kol07, Proposition 99].) x₁ˢ = (s+1)⁻¹ ∂(x₁^{s+1}) ∈ D(W_{s+1}(I)).

theorem IsLocalRing.RegularCoords.pow_mul_mem_D_W_succ {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {m : ℕ} (hm : 1 ≤ m) {I : Ideal R} {h : R} (hh : h ∈ c.MC I m) {δ : Derivation ℚ R R} (h1 : δ h = 1) (hD : ∀ (J : Ideal R), ∀ f ∈ J, δ f ∈ c.D J) (s t : ℕ) : t ≤ s → ∀ f ∈ c.W m t I, h ^ (s - t) * f ∈ c.D (c.W m (s + 1) I)

(The proof of [Kol07, Proposition 99].) x₁^{s−t} W_t(I) ≤ D(W_{s+1}(I)) for t ≤ s, by induction on t.

theorem IsLocalRing.RegularCoords.D_W_succ {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {m : ℕ} (hm : 1 ≤ m) {I : Ideal R} (hI : ord I ≤ ↑m) (s : ℕ) : c.D (c.W m (s + 1) I) = c.W m s I

[Kol07, (99.3)]: D(W_{s+1}(I)) = W_s(I) for ord I ≤ m, m ≥ 1.

theorem IsLocalRing.RegularCoords.Dpow_W {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {m : ℕ} (hm : 1 ≤ m) {I : Ideal R} (hI : ord I ≤ ↑m) {i s : ℕ} (hi : i ≤ s) : c.Dpow i (c.W m s I) = c.W m (s - i) I

(99.3) iterated, Kollár's "applying (3) repeatedly": Dⁱ(W_s(I)) = W_{s−i}(I) for i ≤ s.

The order of W_s(I)

theorem IsLocalRing.RegularCoords.prod_le_maximalIdeal_pow {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {m : ℕ} {I : Ideal R} (hI : I ≤ maximalIdeal R ^ m) (e : Fin (m + 1) → ℕ) : ∏ j : Fin (m + 1), c.Dpow (↑j) I ^ e j ≤ maximalIdeal R ^ wt m e

Every generator of W_s(I) lies in 𝔪^{wt(e)} when I ≤ 𝔪ᵐ, since Dʲ I ≤ 𝔪^{m−j} (the estimate in the proof of [Kol07, Theorem 100]).

theorem IsLocalRing.RegularCoords.W_le_maximalIdeal_pow {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {m s : ℕ} {I : Ideal R} (hI : I ≤ maximalIdeal R ^ m) : c.W m s I ≤ maximalIdeal R ^ s

theorem IsLocalRing.RegularCoords.le_ord_W {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {m : ℕ} {I : Ideal R} (hm : ↑m ≤ ord I) (s : ℕ) : ↑s ≤ ord (c.W m s I)

If m ≤ ord I then s ≤ ord (W_s(I)) (the estimate in the proof of [Kol07, Theorem 100]).

theorem IsLocalRing.RegularCoords.ord_W_le {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {m : ℕ} (hm : 1 ≤ m) {I : Ideal R} (hI : ord I = ↑m) (s : ℕ) : ord (c.W m s I) ≤ ↑s

If ord I = m ≥ 1 then ord (W_s(I)) ≤ s, since Dˢ(W_s(I)) = W_0(I) = R ((99.3) iterated) and an ideal whose s-th derivative ideal is the unit ideal has order ≤ s ([Kol07, Lemma 74 (3)] locally).

theorem IsLocalRing.RegularCoords.ord_W {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {m : ℕ} (hm : 1 ≤ m) {I : Ideal R} (hI : ord I = ↑m) (s : ℕ) : ord (c.W m s I) = ↑s

If ord I = m ≥ 1 then ord (W_s(I)) = s; for s = m! this is [Kol07, Theorem 54.2 (i)], locally.

theorem IsLocalRing.RegularCoords.le_ord_W_iff {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {m : ℕ} (hm : 1 ≤ m) {I : Ideal R} {s : ℕ} (hs1 : 1 ≤ s) : ↑s ≤ ord (c.W m s I) ↔ ↑m ≤ ord I

For s ≥ 1, cosupp (W_s(I), s) = cosupp (I, m), locally: s ≤ ord (W_s(I)) ↔ m ≤ ord I; no hypothesis ord I ≤ m is needed.

Proposition 99 (4)–(5)

theorem IsLocalRing.RegularCoords.MC_W {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {m : ℕ} (hm : 1 ≤ m) {I : Ideal R} (hI : ord I ≤ ↑m) {s : ℕ} (hs1 : 1 ≤ s) : c.MC (c.W m s I) s = c.MC I m

[Kol07, (99.4)]: MC_s(W_s(I)) = W_1(I) = MC_m(I) for s ≥ 1, ord I ≤ m, m ≥ 1 (the mark of W_s(I) is s, its order by ord_W).

theorem IsLocalRing.RegularCoords.isMCInvariant_W {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {m : ℕ} (hm : 1 ≤ m) {I : Ideal R} (hI : ord I ≤ ↑m) {s : ℕ} (hs1 : 1 ≤ s) : c.IsMCInvariant (c.W m s I) s

[Kol07, (99.5)] (Kollár: "Together with (2) and (3), this implies (5)"): W_s(I) is MC-invariant with respect to s: MC_s(W_s) · D(W_s) = W_1 · W_{s−1} ≤ W_s.

Proposition 99 (6)–(8)

theorem IsLocalRing.RegularCoords.W_mul_W_eq {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {m : ℕ} (hm : 1 ≤ m) (r t : ℕ) (ht : (m - 1) * Lcm m ≤ t) (I : Ideal R) : c.W m (r * Lcm m) I * c.W m t I = c.W m (r * Lcm m + t) I

[Kol07, (99.6)] (Kollár: "(6) is implied by (99.9)"): W_s(I) · W_t(I) = W_{s+t}(I) for s = r L_m and t ≥ (m − 1) L_m.

theorem IsLocalRing.RegularCoords.W_pow_le {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (m a k : ℕ) (I : Ideal R) : c.W m a I ^ k ≤ c.W m (k * a) I

W_a(I)^k ≤ W_{ka}(I) (99.2 iterated).

theorem IsLocalRing.RegularCoords.W_pow {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {m : ℕ} (hm : 1 ≤ m) {r : ℕ} (hr : m - 1 ≤ r) (j : ℕ) (I : Ideal R) : c.W m (r * Lcm m) I ^ j = c.W m (j * (r * Lcm m)) I

[Kol07, (99.7)]: W_s(I)ʲ = W_{js}(I) for s = r L_m, r ≥ m − 1.

theorem IsLocalRing.RegularCoords.Dpow_W_pow_le {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {m : ℕ} (hm : 1 ≤ m) {I : Ideal R} (hI : ord I ≤ ↑m) {r : ℕ} (hr : m - 1 ≤ r) {i : ℕ} (hi : i < r * Lcm m) : c.Dpow i (c.W m (r * Lcm m) I) ^ (r * Lcm m) ≤ c.W m (r * Lcm m) I ^ (r * Lcm m - i)

(The proof of (99.8) in [Kol07, Proposition 99].) For s = r L_m, r ≥ m − 1, ord I ≤ m and i < s: (Dⁱ W_s(I))ˢ = W_{s−i}(I)ˢ ≤ W_{s(s−i)}(I) = W_s(I)^{s−i}.

theorem IsLocalRing.RegularCoords.isDBalanced_W {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {m : ℕ} (hm : 1 ≤ m) {I : Ideal R} (hI : ord I ≤ ↑m) {r : ℕ} (hr : m - 1 ≤ r) : c.IsDBalanced (c.W m (r * Lcm m) I) (r * Lcm m)

[Kol07, (99.8)]: W_s(I) is D-balanced with respect to s for s = r L_m, r ≥ m − 1, ord I ≤ m (the mark s is the order of W_s(I) by ord_W when s ≥ 1, that is, r ≥ 1).