The inclusion ⊆ of Kollár's (88.1) in a chart

[Kol07, Theorem 88]: for a smooth blow-up sequence of order ≥ m whose centres lie in the birational transforms of a smooth hypersurface S, D^s Π⁻¹_*(I, m) = ∑_{j ≤ s} D^{s−j}(−log S_r) Π⁻¹_*(D^j I, m − j) (88.1). The inclusion ⊇ follows from [Kol07, Theorem 76]. This module proves the inclusion ⊆ for one blow-up in the chart of the blow-up of P = (x₀, …, x_r) dividing by x_r, with S = V(x_h), h < r, and S₁ = V(y_h) its transform: for I ≤ Pᵐ and s ≤ m,

D'^s π⁻¹_*(I, m) ≤ ∑_{j ≤ s} D'^{s−j}(−log S₁) π⁻¹_*(D^j I, m − j) (iterate_chartD_transformIdeal_le),

where D' = chartD is the derivative ideal of the chart ring for all the transported derivations ∂'ᵢ (Hironaka/Algebra/Local/TransformDeriv.lean) and D'(−log S₁) = chartDlog the logarithmic one, for y_h ∂'_h and the ∂'ᵢ, i ≠ h, which preserve (y_h) (Hironaka/Algebra/Local/TransformLogDeriv.lean).

Kollár's proof applies the decomposition [Kol07, (87.2)], D^s(I) = D^s(−log S)(I) + D^{s−1}(−log S)(∂I/∂x₁) + ⋯ + (∂^s I/∂x₁^s), to the transform and then commutes ∂/∂y₁ with the transform by (75.1). Here the inclusion is obtained directly from the generators of the transform, in three steps:

• Leibniz on generators. A derivation maps span G into span G + span (δ '' G) (Derivation.mem_span_sup_span_image), so D'^s (span G) is generated by the ≤ s-fold chart derivatives of the elements of G (chartWords, iterate_chartD_span_le).
• Moving ∂'_h to the right. The commutators [∂'_h, y_h ∂'_h] = ∂'_h and [∂'_h, ∂'_i] = 0 give ∂'_h D'(−log S₁)(K) ⊆ D'(−log S₁)(K) + D'(−log S₁)(∂'_h K) (span_image_chartDlog_le), hence the same for the iterates D'^t(−log S₁) (span_image_chartDlogpow_le): a ∂'_h applied after t logarithmic derivations is a ∂'_h applied before them, up to logarithmic terms.
• The normal form. Every ≤ s-fold chart derivative of an element of G lies in ∑_{j ≤ s} D'^{s−j}(−log S₁) (∂'_h^j G) (chartWords_subset_iSup, with pivotDerivs the ideal of the j-fold ∂'_h-derivatives of G), and for the generators g = π⁻¹_*(f, m), f ∈ I, ∂'_h^j g = π⁻¹_*(∂_h^j f, m − j) ∈ π⁻¹_*(D^j I, m − j) by (75.1) iterated (Hironaka/Algebra/Local/TransformDerivIter.lean).

The argument on generators is the library's own. It is needed because the intermediate identity (88.2) of Kollár's proof, read as a statement about all elements of the ideal π⁻¹_*(I, m), does not hold in general (HironakaExamples/Theorem88Counterexample.lean).

Used for Theorem 88 on schemes (Hironaka/Resolution/Algebraic/Kol07/Theorem88BlowUp.lean) and on manifolds (Hironaka/Manifold/BlowUp/Transform/LogDerivBlowUp.lean), and for the logarithmic derivations of the chart (Hironaka/Algebra/Local/ChartLogDerivations.lean).

theorem Derivation.mem_span_sup_span_image {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (δ : Derivation k A A) (S : Set A) {z : A} (hz : z ∈ Ideal.span S) : δ z ∈ Ideal.span S ⊔ Ideal.span (⇑δ '' S)

Leibniz on generators: a derivation maps span S into span S ⊔ span (δ '' S).

D' on spans: Leibniz on the generators

theorem IsLocalRing.RegularCoords.chartD_mono {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) {J K : Ideal ↥(chartRing c.x r)} (hJK : J ≤ K) : c.chartD r J ≤ c.chartD r K

theorem IsLocalRing.RegularCoords.chartD_span_le {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) (W : Set ↥(chartRing c.x r)) : c.chartD r (Ideal.span W) ≤ Ideal.span (W ∪ ⋃ (i : Fin n), ⇑(c.chartDerivRing r i) '' W)

D'(span W) ⊆ span (W ∪ ⋃ᵢ ∂'ᵢ W).

noncomputable def IsLocalRing.RegularCoords.chartWords {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) (G : Set ↥(chartRing c.x r)) : ℕ → Set ↥(chartRing c.x r)

The ≤ s-fold chart derivatives of the elements of G.

Equations

• c.chartWords r G 0 = G
• c.chartWords r G s.succ = c.chartWords r G s ∪ ⋃ (i : Fin n), ⇑(c.chartDerivRing r i) '' c.chartWords r G s

@[simp]

theorem IsLocalRing.RegularCoords.chartWords_zero {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) (G : Set ↥(chartRing c.x r)) : c.chartWords r G 0 = G

theorem IsLocalRing.RegularCoords.chartWords_succ {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) (G : Set ↥(chartRing c.x r)) (s : ℕ) : c.chartWords r G (s + 1) = c.chartWords r G s ∪ ⋃ (i : Fin n), ⇑(c.chartDerivRing r i) '' c.chartWords r G s

theorem IsLocalRing.RegularCoords.iterate_chartD_span_le {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) (G : Set ↥(chartRing c.x r)) (s : ℕ) : (c.chartD r)^[s] (Ideal.span G) ≤ Ideal.span (c.chartWords r G s)

D'^s (span G) is generated by the ≤ s-fold chart derivatives of the elements of G.

D'(−log S₁) and sums

theorem IsLocalRing.RegularCoords.chartDlog_sup_le {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r h : Fin n) (A B : Ideal ↥(chartRing c.x r)) : c.chartDlog r h (A ⊔ B) ≤ c.chartDlog r h A ⊔ c.chartDlog r h B

theorem IsLocalRing.RegularCoords.chartDlogpow_sup_le {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r h : Fin n) (t : ℕ) (A B : Ideal ↥(chartRing c.x r)) : c.chartDlogpow r h t (A ⊔ B) ≤ c.chartDlogpow r h t A ⊔ c.chartDlogpow r h t B

theorem IsLocalRing.RegularCoords.chartDlogpow_le_succ {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r h : Fin n) (t : ℕ) (A : Ideal ↥(chartRing c.x r)) : c.chartDlogpow r h t A ≤ c.chartDlogpow r h (t + 1) A

Moving ∂'_h past the logarithmic derivations

noncomputable def IsLocalRing.RegularCoords.chartDlogGen {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r h : Fin n) (K : Ideal ↥(chartRing c.x r)) : Set ↥(chartRing c.x r)

The generating set of D'(−log S₁)(K): K, y_h ∂'_h K, ∂'_j K for j ≠ h.

Equations

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

theorem IsLocalRing.RegularCoords.chartDlog_eq_span {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r h : Fin n) (K : Ideal ↥(chartRing c.x r)) : c.chartDlog r h K = Ideal.span (c.chartDlogGen r h K)

theorem IsLocalRing.RegularCoords.span_image_chartDlog_le {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r h : Fin n) (K : Ideal ↥(chartRing c.x r)) : Ideal.span (⇑(c.chartDerivRing r h) '' ↑(c.chartDlog r h K)) ≤ c.chartDlog r h K ⊔ c.chartDlog r h (Ideal.span (⇑(c.chartDerivRing r h) '' ↑K))

[∂'_h, y_h ∂'_h] = ∂'_h and [∂'_h, ∂'_j] = 0: ∂'_h D'(−log S₁)(K) ⊆ D'(−log S₁)(K) + D'(−log S₁)(∂'_h K).

theorem IsLocalRing.RegularCoords.span_image_chartDlogpow_le {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r h : Fin n) (t : ℕ) (K : Ideal ↥(chartRing c.x r)) : Ideal.span (⇑(c.chartDerivRing r h) '' ↑(c.chartDlogpow r h t K)) ≤ c.chartDlogpow r h t K ⊔ c.chartDlogpow r h t (Ideal.span (⇑(c.chartDerivRing r h) '' ↑K))

∂'_h D'^t(−log S₁)(K) ⊆ D'^t(−log S₁)(K) + D'^t(−log S₁)(∂'_h K): a ∂'_h applied after t logarithmic derivations is a ∂'_h applied before them, up to logarithmic terms.

The normal form

noncomputable def IsLocalRing.RegularCoords.pivotDerivs {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r h : Fin n) (G : Set ↥(chartRing c.x r)) (j : ℕ) : Ideal ↥(chartRing c.x r)

The ideal generated by the j-fold ∂'_h-derivatives of the elements of G.

Equations

• c.pivotDerivs r h G j = Ideal.span ((⇑(c.chartDerivRing r h))^[j] '' G)

theorem IsLocalRing.RegularCoords.span_image_pivotDerivs_le {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r h : Fin n) (G : Set ↥(chartRing c.x r)) (j : ℕ) : Ideal.span (⇑(c.chartDerivRing r h) '' ↑(c.pivotDerivs r h G j)) ≤ c.pivotDerivs r h G j ⊔ c.pivotDerivs r h G (j + 1)

theorem IsLocalRing.RegularCoords.iSup_chartDlogpow_le_succ {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r h : Fin n) (A : ℕ → Ideal ↥(chartRing c.x r)) (s : ℕ) : ⨆ (j : ℕ), ⨆ (_ : j ≤ s), c.chartDlogpow r h (s - j) (A j) ≤ ⨆ (j : ℕ), ⨆ (_ : j ≤ s + 1), c.chartDlogpow r h (s + 1 - j) (A j)

The raise of the level: ∑_{j ≤ s} D'^{s−j}(−log) A_j ⊆ ∑_{j ≤ s+1} D'^{s+1−j}(−log) A_j.

theorem IsLocalRing.RegularCoords.chartWords_subset_iSup {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r h : Fin n) (G : Set ↥(chartRing c.x r)) (s : ℕ) (z : ↥(chartRing c.x r)) : z ∈ c.chartWords r G s → z ∈ ⨆ (j : ℕ), ⨆ (_ : j ≤ s), c.chartDlogpow r h (s - j) (c.pivotDerivs r h G j)

The normal form: every ≤ s-fold chart derivative of an element of G lies in ∑_{j ≤ s} D'^{s−j}(−log S₁) (∂'_h^j G).

The inclusion ⊆ of (88.1)

theorem IsLocalRing.RegularCoords.iterate_chartD_transformIdeal_le {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) {h : Fin n} (hh : h < r) {I : Ideal R} {m : ℕ} (hI : I ≤ chartCenter c.x r ^ m) {s : ℕ} (hs : s ≤ m) : (c.chartD r)^[s] (transformIdeal c.x r I m) ≤ ⨆ (j : ℕ), ⨆ (_ : j ≤ s), c.chartDlogpow r h (s - j) (transformIdeal c.x r (c.Dpow j I) (m - j))

The inclusion ⊆ of [Kol07, (88.1)] for one blow-up in the chart (the proof of [Kol07, Theorem 88]): in the chart dividing by x_r, for the hypersurface coordinate x_h, h < r, I ≤ Pᵐ and s ≤ m, D'^s π⁻¹_*(I, m) ≤ ∑_{j ≤ s} D'^{s−j}(−log (y_h)) π⁻¹_*(D^j I, m − j).