Iterated derivatives of a transform along a divided coordinate

In the chart of the blow-up of P = (x₀, …, x_r) dividing by x_r (Hironaka/Algebra/Local/TransformDeriv.lean), [Kol07, (75.1)] says that for a divided coordinate x_h, h < r, differentiation with respect to x_h commutes with the transform: ∂'_h π⁻¹_*(f, m+1) = π⁻¹_*(∂_h f, m). Iterating j times gives, for f ∈ Pᵐ and j ≤ m, ∂'_h^j π⁻¹_*(f, m) = π⁻¹_*(∂_h^j f, m − j) (iterate_chartDerivRing_transformElem), and hence, for I ≤ Pᵐ and f ∈ I, the j-fold ∂'_h-derivative of the generator π⁻¹_*(f, m) of π⁻¹_*(I, m) lies in π⁻¹_*(D^j I, m − j), because ∂_h^j f ∈ D^j I (iterate_chartDerivRing_transformElem_mem).

This is the observation of the proof of [Kol07, Theorem 88] that, "by (75.1)", differentiation commutes with the birational transform for ∂/∂x₁ and ∂/∂y₁. It is stated here for the generators π⁻¹_*(f, m), f ∈ I, of the transform and not for all its elements: the ideal generated by the j-fold ∂'_h-derivatives of all elements of π⁻¹_*(I, m) need not lie in π⁻¹_*(D^j I, m − j) (HironakaExamples/Theorem88Counterexample.lean). The statement on generators suffices for the inclusion ⊆ of [Kol07, (88.1)], proved in Hironaka/Algebra/Local/TransformDerivNormalForm.lean.

theorem IsLocalRing.transformElem_congr {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {f₁ f₂ : R} (hf : f₁ = f₂) {m₁ m₂ : ℕ} (hm : m₁ = m₂) (hf₁ : f₁ ∈ chartCenter x r ^ m₁) (hf₂ : f₂ ∈ chartCenter x r ^ m₂) : transformElem x r f₁ hf₁ = transformElem x r f₂ hf₂

Transformed elements of equal elements with equal marks are equal (the membership proofs are irrelevant).

theorem IsLocalRing.RegularCoords.iterate_chartDerivRing_transformElem {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) {h : Fin n} (hh : h < r) {m : ℕ} {f : R} (hf : f ∈ chartCenter c.x r ^ m) {j : ℕ} (hj : j ≤ m) : ∃ (hf' : (⇑(c.pderiv h))^[j] f ∈ chartCenter c.x r ^ (m - j)), (⇑(c.chartDerivRing r h))^[j] (transformElem c.x r f hf) = transformElem c.x r ((⇑(c.pderiv h))^[j] f) hf'

[Kol07, (75.1)] iterated (the proof of [Kol07, Theorem 88]): in the chart dividing by x_r, for h < r, f ∈ Pᵐ and j ≤ m, ∂'_h^j π⁻¹_*(f, m) = π⁻¹_*(∂_h^j f, m − j).

theorem IsLocalRing.RegularCoords.iterate_chartDerivRing_transformElem_mem {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) {j : ℕ} (hj : j ≤ m) {f : R} (hf : f ∈ I) : (⇑(c.chartDerivRing r h))^[j] (transformElem c.x r f ⋯) ∈ transformIdeal c.x r (c.Dpow j I) (m - j)

For I ≤ Pᵐ, f ∈ I and j ≤ m, the j-fold ∂'_h-derivative of the generator π⁻¹_*(f, m) lies in the transform of D^j I: ∂'_h^j π⁻¹_*(f, m) = π⁻¹_*(∂_h^j f, m − j) ∈ π⁻¹_*(D^j I, m − j).