Kollár's Lemma 61 in local form: the monomial computation

The proof of [Kol07, Lemma 61] takes f(x₁, …, xₙ) ∈ I of order m = max-ord I at p, writes its birational transform as π⁻¹_* f = y_r^{-m} f(y₁y_r, …, y_{r-1}y_r, y_r, …, yₙ), and observes that a monomial of degree m of f becomes a monomial of degree at most 2m after the substitution, hence "a monomial of degree ≤ 2m − m = m" of π⁻¹_* f.

This file carries out that computation in the power series ring K⟦y⟧. With the zero-based indexing of Hironaka/Algebra/Local/ChartRing.lean (xᵢ ↦ yᵢ y_r for i < r, xⱼ ↦ yⱼ for j ≥ r), the monomial x^α goes to y^{σ(α)} with σ(α) = α + (∑_{i<r} αᵢ) e_r (chartExp, injective, |σ(α)| = |α| + ∑_{i<r} αᵢ ≤ 2|α|), so distinct monomials of f stay distinct and coeff_{σ α}(φ̂ f) = coeff_α f (coeff_subst_chartSubst). If every monomial of f has x₀..x_r-degree ≥ m (the local form of f ∈ P̂ᵐ, P the ideal of the centre), then φ̂ f = y_r^m g and, for order f = m, order g ≤ m (exists_X_pow_mul_eq_subst_chartSubst). The transfer of this bound from K⟦x⟧ to a regular local ring R through the Cohen isomorphism R̂ ≅ K⟦x⟧ is made in Hironaka/Algebra/Local/ChartCompletion.lean and the modules following it.

The exponent substitution

noncomputable def IsLocalRing.chartExp {n : ℕ} (r : Fin n) (α : Fin n →₀ ℕ) : Fin n →₀ ℕ

The exponent substitution σ(α) = (α₀, …, α_{r-1}, α₀ + ⋯ + α_r, α_{r+1}, …), i.e. α + (∑_{i<r} αᵢ) e_r: the exponent of "the corresponding monomial" in the proof of [Kol07, Lemma 61].

Equations

• IsLocalRing.chartExp r α = α + Finsupp.single r (∑ i : Fin n with i < r, α i)

theorem IsLocalRing.chartExp_apply_of_ne {n : ℕ} (r : Fin n) {i : Fin n} (hi : i ≠ r) (α : Fin n →₀ ℕ) : (chartExp r α) i = α i

theorem IsLocalRing.chartExp_apply_self {n : ℕ} (r : Fin n) (α : Fin n →₀ ℕ) : (chartExp r α) r = α r + ∑ i : Fin n with i < r, α i

theorem IsLocalRing.sum_filter_le_chartExp_apply_self {n : ℕ} (r : Fin n) (α : Fin n →₀ ℕ) : ∑ i : Fin n with i ≤ r, α i = (chartExp r α) r

theorem IsLocalRing.chartExp_injective {n : ℕ} (r : Fin n) : Function.Injective (chartExp r)

σ is injective.

theorem IsLocalRing.degree_add' {n : ℕ} (α β : Fin n →₀ ℕ) : Finsupp.degree (α + β) = Finsupp.degree α + Finsupp.degree β

theorem IsLocalRing.degree_chartExp {n : ℕ} (r : Fin n) (α : Fin n →₀ ℕ) : Finsupp.degree (chartExp r α) = Finsupp.degree α + ∑ i : Fin n with i < r, α i

|σ(α)| = |α| + ∑_{i<r} αᵢ.

theorem IsLocalRing.sum_filter_lt_le_degree {n : ℕ} (r : Fin n) (α : Fin n →₀ ℕ) : ∑ i : Fin n with i < r, α i ≤ Finsupp.degree α

theorem IsLocalRing.degree_chartExp_le {n : ℕ} (r : Fin n) (α : Fin n →₀ ℕ) : Finsupp.degree (chartExp r α) ≤ 2 * Finsupp.degree α

|σ(α)| ≤ 2|α|.

theorem IsLocalRing.degree_chartExp_sub_le {n : ℕ} (r : Fin n) {α : Fin n →₀ ℕ} {m : ℕ} (h : Finsupp.degree α = m) : Finsupp.degree (chartExp r α) - m ≤ m

For |α| = m, |σ(α)| − m ≤ m: the bound "≤ 2m − m = m" of the proof of [Kol07, Lemma 61].

The substitution xᵢ ↦ yᵢ y_r (i < r), xⱼ ↦ yⱼ (j ≥ r)

noncomputable def IsLocalRing.chartSubst {n : ℕ} (r : Fin n) {K : Type u_1} [CommRing K] : Fin n → MvPowerSeries (Fin n) K

The substitution xᵢ ↦ yᵢ y_r for i < r, xⱼ ↦ yⱼ for j ≥ r, in K⟦y⟧: the substitution of [Kol07, Definition 60, (60.3)].

Equations

• IsLocalRing.chartSubst r i = if i < r then MvPowerSeries.X i * MvPowerSeries.X r else MvPowerSeries.X i

theorem IsLocalRing.hasSubst_chartSubst {n : ℕ} (r : Fin n) {K : Type u_1} [CommRing K] : MvPowerSeries.HasSubst (chartSubst r)

theorem IsLocalRing.chartSubst_prod {n : ℕ} (r : Fin n) {K : Type u_1} [CommRing K] (α : Fin n →₀ ℕ) : (α.prod fun (s : Fin n) (e : ℕ) => chartSubst r s ^ e) = (MvPowerSeries.monomial (chartExp r α)) 1

The monomial x^α goes to y^{σ(α)} under the chart substitution.

theorem IsLocalRing.coeff_subst_chartSubst {n : ℕ} (r : Fin n) {K : Type u_1} [CommRing K] (f : MvPowerSeries (Fin n) K) (α : Fin n →₀ ℕ) : (MvPowerSeries.coeff (chartExp r α)) (MvPowerSeries.subst (chartSubst r) f) = (MvPowerSeries.coeff α) f

The coefficient formula coeff_{σ α}(φ̂ f) = coeff_α f: since σ is injective, the corresponding monomial of φ̂ f has the coefficient of x^α in f.

theorem IsLocalRing.coeff_subst_chartSubst_eq_zero {n : ℕ} (r : Fin n) {K : Type u_1} [CommRing K] {f : MvPowerSeries (Fin n) K} {β : Fin n →₀ ℕ} (hβ : ∀ (d : Fin n →₀ ℕ), (MvPowerSeries.coeff d) f ≠ 0 → chartExp r d ≠ β) : (MvPowerSeries.coeff β) (MvPowerSeries.subst (chartSubst r) f) = 0

Every monomial of φ̂ f is y^{σ(d)} for a monomial x^d of f.

theorem IsLocalRing.coeff_subst_chartSubst_eq_zero_of_lt {n : ℕ} (r : Fin n) {K : Type u_1} [CommRing K] {f : MvPowerSeries (Fin n) K} {m : ℕ} (hP : ∀ (d : Fin n →₀ ℕ), (MvPowerSeries.coeff d) f ≠ 0 → m ≤ ∑ i : Fin n with i ≤ r, d i) {β : Fin n →₀ ℕ} (hβ : β r < m) : (MvPowerSeries.coeff β) (MvPowerSeries.subst (chartSubst r) f) = 0

If every monomial of f has x₀..x_r-degree ≥ m (f ∈ P̂ᵐ), then every monomial of φ̂ f has y_r-exponent ≥ m.

theorem IsLocalRing.exists_X_pow_mul_eq_subst_chartSubst {n : ℕ} (r : Fin n) {K : Type u_1} [CommRing K] {f : MvPowerSeries (Fin n) K} {m : ℕ} (hord : f.order = ↑m) (hP : ∀ (d : Fin n →₀ ℕ), (MvPowerSeries.coeff d) f ≠ 0 → m ≤ ∑ i : Fin n with i ≤ r, d i) : ∃ (g : MvPowerSeries (Fin n) K), MvPowerSeries.X r ^ m * g = MvPowerSeries.subst (chartSubst r) f ∧ g.order ≤ ↑m

The monomial computation of the proof of [Kol07, Lemma 61]: if order f = m and every monomial of f has x₀..x_r-degree ≥ m (f ∈ P̂ᵐ), then φ̂ f = y_r^m g with order g ≤ m — the monomial of degree m of f survives with degree ≤ 2m − m = m.