Włodarczyk's homogenized and coefficient ideals against Kollár's maximal coefficient ideals

A comparison, used nowhere else in the library. Włodarczyk [Wlo05, §2.9] sets T(I) := D^{μ−1} I (Kollár's maximal-contact ideal MC_μ(I), Hironaka/Algebra/Local/MaximalContact.lean) and defines the homogenized ideal H(I) := I + D(I)·T(I) + ⋯ + D^{μ−1}(I)·T(I)^{μ−1}, with mark μ (homogenized); the coefficient ideal [Wlo05, Definition 2.10.1] is the marked sum C(I, μ) := ∑ᵢ (Dⁱ I, μ − i) (coefficientIdeal), where the sum of marked ideals with different marks is Włodarczyk's (I₁, μ₁) + ⋯ + (Iₘ, μₘ) := (∑ᵢ Iᵢ^{∏_{k ≠ i} μ_k}, ∏ μ_k) [Wlo05, §2.8] (MarkedIdeal.wsum).

Relation to Kollár's maximal coefficient ideals W_s(I) (Hironaka/Algebra/Local/Tuning.lean, with parameter m = μ): each summand Dⁱ I · (D^{μ−1} I)ⁱ of H(I) has weight (μ − i) + i = μ, so H(I) ≤ W_μ(I) (homogenized_le_W); each summand (Dⁱ I)^{μ!/(μ−i)} of C(I, μ) has weight μ!, so C(I, μ) ≤ W_{μ!}(I) (coefficientIdeal_I_le_W). [Wlo05, Lemma 2.9.1] is verified at the ideal level: H(I) = I for μ = 1; the series may run over all i; the marked form of the summands; D(H(I, μ)) ≤ H(D(I, μ)) for μ > 1; and T(H(I)) = T(I), the analogue of [Kol07, (99.4)]. The local halves of [Wlo05, Lemma 2.8.1 (1)] (the closed point lies in the cosupport of a marked sum when it lies in the cosupport of every summand, inCosupp_wsum) and of [Wlo05, Lemma 2.10.2] (inCosupp_coefficientIdeal) are included. His Lemmas 2.9.2, 2.10.2 and 2.10.4 otherwise concern multiple test blow-ups, the analogues of [Kol07, Theorem 100] and of the going-up for D-balanced ideals, and are not treated here.

Włodarczyk's displayed range for the coefficient ideal is i = 1, …, μ in the arXiv text; the proof of his Lemma 2.10.2 uses 0 ≤ i ≤ μ − 1, which is the range under which the marked sum of §2.8 is meaningful (a summand of mark 0 would make the product of marks 0); that range is used here.

def IsLocalRing.MarkedIdeal.wsum {R : Type u_1} [CommRing R] {k : ℕ} (L : Fin k → MarkedIdeal R) : MarkedIdeal R

Włodarczyk's sum of marked ideals with different marks [Wlo05, §2.8]: (I₁, μ₁) + ⋯ + (Iₖ, μₖ) := (∑ᵢ Iᵢ^{∏_{j ≠ i} μⱼ}, ∏ⱼ μⱼ).

Equations

• IsLocalRing.MarkedIdeal.wsum L = { I := ∑ i : Fin k, (L i).I ^ ∏ j ∈ Finset.univ.erase i, (L j).m, m := ∏ j : Fin k, (L j).m }

@[simp]

theorem IsLocalRing.MarkedIdeal.wsum_I {R : Type u_1} [CommRing R] {k : ℕ} (L : Fin k → MarkedIdeal R) : (wsum L).I = ∑ i : Fin k, (L i).I ^ ∏ j ∈ Finset.univ.erase i, (L j).m

@[simp]

theorem IsLocalRing.MarkedIdeal.wsum_m {R : Type u_1} [CommRing R] {k : ℕ} (L : Fin k → MarkedIdeal R) : (wsum L).m = ∏ j : Fin k, (L j).m

theorem IsLocalRing.MarkedIdeal.wsum_two {R : Type u_1} [CommRing R] (J K : MarkedIdeal R) : wsum ![J, K] = { I := J.I ^ K.m + K.I ^ J.m, m := J.m * K.m }

Włodarczyk's displayed binary case: (I, μ_I) + (J, μ_J) = (I^{μ_J} + J^{μ_I}, μ_I μ_J).

theorem IsLocalRing.MarkedIdeal.inCosupp_wsum {R : Type u_1} [CommRing R] [IsLocalRing R] {k : ℕ} {L : Fin k → MarkedIdeal R} (h : ∀ (i : Fin k), (L i).InCosupp) : (wsum L).InCosupp

[Wlo05, Lemma 2.8.1 (1)], the local half, valid in every local ring: if the closed point lies in every cosupp (Iᵢ, μᵢ), it lies in cosupp of the sum.

@[instance_reducible]

instance IsLocalRing.MarkedIdeal.instPowNat {R : Type u_1} [CommRing R] : Pow (MarkedIdeal R) ℕ

Powers of marked ideals, (I, m)ᵏ = (Iᵏ, m k): the iterated product of marked ideals of [Kol07, Definition 59] and [Wlo05, §2.8].

Equations

• IsLocalRing.MarkedIdeal.instPowNat = { pow := fun (J : IsLocalRing.MarkedIdeal R) (k : ℕ) => { I := J.I ^ k, m := J.m * k } }

@[simp]

theorem IsLocalRing.MarkedIdeal.pow_I {R : Type u_1} [CommRing R] (J : MarkedIdeal R) (k : ℕ) : (J ^ k).I = J.I ^ k

@[simp]

theorem IsLocalRing.MarkedIdeal.pow_m {R : Type u_1} [CommRing R] (J : MarkedIdeal R) (k : ℕ) : (J ^ k).m = J.m * k

The homogenized ideal ([Wlo05, §2.9])

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

Włodarczyk's homogenized ideal H(I) := ∑_{i < μ} Dⁱ(I) · T(I)ⁱ with T(I) = D^{μ-1} I (Kollár's MC_μ(I)); the marked ideal is (H(I), μ).

Equations

• c.homogenized I μ = ∑ i ∈ Finset.range μ, c.Dpow i I * c.MC I μ ^ i

theorem IsLocalRing.RegularCoords.homogenized_le_iff {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {I J : Ideal R} {μ : ℕ} : c.homogenized I μ ≤ J ↔ ∀ i < μ, c.Dpow i I * c.MC I μ ^ i ≤ J

theorem IsLocalRing.RegularCoords.Dpow_mul_MC_pow_le_homogenized {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {I : Ideal R} {μ i : ℕ} (hi : i < μ) : c.Dpow i I * c.MC I μ ^ i ≤ c.homogenized I μ

theorem IsLocalRing.RegularCoords.le_homogenized {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {I : Ideal R} {μ : ℕ} (hμ : 0 < μ) : I ≤ c.homogenized I μ

theorem IsLocalRing.RegularCoords.homogenized_one {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (I : Ideal R) : c.homogenized I 1 = I

[Wlo05, Lemma 2.9.1 (1)]: H(I, 1) = (I, 1).

theorem IsLocalRing.RegularCoords.Dpow_mul_MC_pow_le_homogenized' {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {I : Ideal R} {μ : ℕ} (hμ : 1 ≤ μ) (i : ℕ) : c.Dpow i I * c.MC I μ ^ i ≤ c.homogenized I μ

[Wlo05, Lemma 2.9.1 (2)]: the series ∑ᵢ Dⁱ(I) · T(I)ⁱ may run over all i; the terms with i ≥ μ lie in T(I)^μ = D^{μ−1}(I) · T(I)^{μ−1}.

theorem IsLocalRing.RegularCoords.homogenized_eq_iSup {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {I : Ideal R} {μ : ℕ} (hμ : 1 ≤ μ) : c.homogenized I μ = ⨆ (i : ℕ), c.Dpow i I * c.MC I μ ^ i

theorem IsLocalRing.RegularCoords.homogenized_le_W {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {I : Ideal R} {μ : ℕ} (hμ : 1 ≤ μ) : c.homogenized I μ ≤ c.W μ μ I

The relation to Kollár's maximal coefficient ideal: each summand Dⁱ I · (D^{μ−1} I)ⁱ has weight (μ − i) + i = μ, so H(I) ≤ W_μ(I) (with parameter m = μ).

theorem IsLocalRing.RegularCoords.markedD_mul_MC_pow {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (I : Ideal R) {μ i : ℕ} (hi : i ≤ μ) : c.markedD { I := I, m := μ } i hi * { I := c.MC I μ, m := 1 } ^ i = { I := c.Dpow i I * c.MC I μ ^ i, m := μ }

[Wlo05, Lemma 2.9.1 (3)], the summands: Dⁱ(I, μ) · (T(I), 1)ⁱ = (Dⁱ I · T(I)ⁱ, μ) for i ≤ μ.

theorem IsLocalRing.RegularCoords.homogenized_marked {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (I : Ideal R) (μ : ℕ) : { I := c.homogenized I μ, m := μ } = { I := ∑ i : Fin μ, (c.markedD { I := I, m := μ } ↑i ⋯ * { I := c.MC I μ, m := 1 } ^ ↑i).I, m := μ }

[Wlo05, Lemma 2.9.1 (3)]: (H(I), μ) = ∑_{i < μ} Dⁱ(I, μ) · (T(I), 1)ⁱ, a sum of marked ideals all of mark μ (the sum of equally marked ideals of [Kol07, Definition 59]).

theorem IsLocalRing.RegularCoords.MC_D {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {I : Ideal R} {μ : ℕ} (hμ : 1 < μ) : c.MC (c.D I) (μ - 1) = c.MC I μ

T(D(I), μ - 1) = T(I, μ) for μ > 1: the maximal-contact ideal of D(I, μ) = (D I, μ - 1).

theorem IsLocalRing.RegularCoords.D_finset_sum {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {ι : Type u_2} (s : Finset ι) (f : ι → Ideal R) : c.D (∑ i ∈ s, f i) = ∑ i ∈ s, c.D (f i)

theorem IsLocalRing.RegularCoords.D_homogenized_le {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {I : Ideal R} {μ : ℕ} (hμ : 1 < μ) : c.D (c.homogenized I μ) ≤ c.homogenized (c.D I) (μ - 1)

[Wlo05, Lemma 2.9.1 (4)]: for μ > 1, D(H(I, μ)) ≤ H(D(I, μ)), that is, D(H_μ(I)) ≤ H_{μ−1}(D I).

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

Dⁱ(W_s(I)) ≤ W_{s−i}(I) for i ≤ s (iterating D_W_succ_le).

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

W_1(I) ≤ MC_μ(I): a product of positive weight contains a factor Dʲ I with j < μ.

theorem IsLocalRing.RegularCoords.MC_homogenized {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {I : Ideal R} {μ : ℕ} (hμ : 1 ≤ μ) : c.MC (c.homogenized I μ) μ = c.MC I μ

[Wlo05, Lemma 2.9.1 (5)], the analogue of [Kol07, (99.4)]: T(H(I, μ)) = T(I, μ).

The coefficient ideal ([Wlo05, Definition 2.10.1])

def IsLocalRing.RegularCoords.coefficientIdeal {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (I : Ideal R) (μ : ℕ) : MarkedIdeal R

Włodarczyk's coefficient ideal C(I, μ) := ∑_{i < μ} (Dⁱ I, μ − i), the marked sum ([Wlo05, §2.8]) of the marked derivatives Dⁱ(I, μ) (markedD, Hironaka/Algebra/Local/Derivative.lean).

Equations

• c.coefficientIdeal I μ = IsLocalRing.MarkedIdeal.wsum fun (i : Fin μ) => c.markedD { I := I, m := μ } ↑i ⋯

theorem IsLocalRing.RegularCoords.prod_fin_sub_eq_factorial (μ : ℕ) : ∏ i : Fin μ, (μ - ↑i) = μ.factorial

theorem IsLocalRing.RegularCoords.coefficientIdeal_m {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (I : Ideal R) (μ : ℕ) : (c.coefficientIdeal I μ).m = μ.factorial

The mark of C(I, μ) is μ! = ∏_{i < μ} (μ - i).

theorem IsLocalRing.RegularCoords.coefficientIdeal_I {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (I : Ideal R) (μ : ℕ) : (c.coefficientIdeal I μ).I = ∑ i : Fin μ, c.Dpow (↑i) I ^ (μ.factorial / (μ - ↑i))

The ideal of C(I, μ) is ∑_{i < μ} (Dⁱ I)^{μ!/(μ-i)} (Villamayor's form).

theorem IsLocalRing.RegularCoords.coefficientIdeal_I_le_W {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (I : Ideal R) (μ : ℕ) : (c.coefficientIdeal I μ).I ≤ c.W μ μ.factorial I

The relation to Kollár's maximal coefficient ideal: each summand (Dⁱ I)^{μ!/(μ−i)} has weight (μ − i) · μ!/(μ−i) = μ!, so C(I, μ) ≤ W_{μ!}(I) (with parameter m = μ).

theorem IsLocalRing.RegularCoords.inCosupp_coefficientIdeal {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {I : Ideal R} {μ : ℕ} (hI : ↑μ ≤ ord I) : (c.coefficientIdeal I μ).InCosupp

The local half of [Wlo05, Lemma 2.10.2]: if μ ≤ ord I then the closed point lies in cosupp C(I, μ), since each Dⁱ I has order ≥ μ − i (le_ord_Dpow).