The chart logarithmic derivations are logarithmic along the strict transform

In the chart of the blow-up of P = (x₀, …, x_r) dividing by x_r, for the hypersurface coordinate x_h, h < r, the strict transform of S = (x_h) is S₁ = (y_h), y_h = x_h / x_r; its ideal in the chart ring, as read off the stalk of the blow-up (Hironaka/Resolution/Algebraic/Kol07/Theorem88BlowUp.lean), is the x_r-saturation ⋃ᵢ ((φ x_h) : x_rⁱ) of the total transform (φ x_h) = (x_r y_h) (chartSat). The logarithmic chart derivations y_h ∂'_h and ∂'_i, i ≠ h, of Hironaka/Algebra/Local/TransformLogDeriv.lean preserve it: a derivation δ with δ(g) ∈ (g)^{sat} preserves (g)^{sat} whatever δ(x_r) is (preservesIdeal_chartSat_of_apply_mem), and ∂'_i (x_r y_h) ∈ {0, y_h}, y_h ∂'_h (x_r y_h) = x_r y_h (chartDerivRing_chartYR). For k-linear coordinates the chart derivations are k-derivations (chartDerivRingOver), so the chart logarithmic derivative ideal D'(−log S₁) (chartDlog) lies in the logarithmic derivative ideal D(−log (x_r y_h)^{sat}) for all k-derivations (Ideal.logDerivative, Hironaka/Scheme/IdealSheaf/Derivative/Logarithmic.lean): chartDlog_le_logDerivative, iterated as chartDlogpow_le_logDerivativeIter. This is the bridge from the chart-level inclusion ⊆ of [Kol07, (88.1)] (Hironaka/Algebra/Local/TransformDerivNormalForm.lean) to the stalks of the blow-up in the proof of [Kol07, Theorem 88] for one blow-up (Hironaka/Resolution/Algebraic/Kol07/Theorem88BlowUp.lean).

theorem IsLocalRing.chartYR_self_eq_algebraMap {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) : chartYR x r r = (algebraMap R ↥(chartRing x r)) (x r)

The chart coordinate y_r is x_r itself.

The chart derivations as k-derivations

theorem IsLocalRing.RegularCoords.chartDerivRing_algebraMap_eq_zero {R : Type u_2} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) {a : R} (ha : ∀ (i : Fin n), (c.pderiv i) a = 0) (j : Fin n) : (c.chartDerivRing r j) ((algebraMap R ↥(chartRing c.x r)) a) = 0

A chart derivation kills the image of an element of R killed by all coordinate derivations: ∂'_j (φ a) = 0 if every ∂_i a = 0 (from the formulas defining chartDeriv in Hironaka/Algebra/Local/Chart.lean).

noncomputable def IsLocalRing.RegularCoords.chartDerivRingOver {k : Type u_1} [CommRing k] {R : Type u_2} [CommRing R] [Algebra k R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) (hk : c.IsLinearOver k) (j : Fin n) : Derivation k ↥(chartRing c.x r) ↥(chartRing c.x r)

The chart derivations as k-derivations, for k-linear coordinates (derivationOver, Hironaka/Algebra/Local/CoordsOver.lean).

Equations

• c.chartDerivRingOver r hk j = IsLocalRing.derivationOver (c.chartDerivRing r j) ⋯

@[simp]

theorem IsLocalRing.RegularCoords.chartDerivRingOver_apply {k : Type u_1} [CommRing k] {R : Type u_2} [CommRing R] [Algebra k R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) (hk : c.IsLinearOver k) (j : Fin n) (z : ↥(chartRing c.x r)) : (c.chartDerivRingOver r hk j) z = (c.chartDerivRing r j) z

The x_r-saturation of a principal ideal

noncomputable def IsLocalRing.RegularCoords.chartSat {R : Type u_2} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) (g : ↥(chartRing c.x r)) : Ideal ↥(chartRing c.x r)

⋃ᵢ ((g) : x_rⁱ), the x_r-saturation of the principal ideal (g) of the chart ring; for g = φ x_h, the chart ideal of the strict transform of (x_h).

Equations

• c.chartSat r g = ⨆ (i : ℕ), Submodule.colon (Ideal.span {g}) ↑(Ideal.span {(algebraMap R ↥(IsLocalRing.chartRing c.x r)) (c.x r)} ^ i)

theorem IsLocalRing.RegularCoords.mem_chartSat_iff {R : Type u_2} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) {g z : ↥(chartRing c.x r)} : z ∈ c.chartSat r g ↔ ∃ (i : ℕ), (algebraMap R ↥(chartRing c.x r)) (c.x r) ^ i * z ∈ Ideal.span {g}

theorem IsLocalRing.RegularCoords.span_singleton_le_chartSat {R : Type u_2} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) (g : ↥(chartRing c.x r)) : Ideal.span {g} ≤ c.chartSat r g

theorem IsLocalRing.RegularCoords.mem_chartSat_of_pow_mul_mem {R : Type u_2} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) {g z : ↥(chartRing c.x r)} {i : ℕ} (hz : (algebraMap R ↥(chartRing c.x r)) (c.x r) ^ i * z ∈ c.chartSat r g) : z ∈ c.chartSat r g

theorem IsLocalRing.RegularCoords.preservesIdeal_chartSat_of_apply_mem {k : Type u_1} [CommRing k] {R : Type u_2} [CommRing R] [Algebra k R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) (δ : Derivation k ↥(chartRing c.x r) ↥(chartRing c.x r)) {g : ↥(chartRing c.x r)} (hδ : δ g ∈ c.chartSat r g) : δ.PreservesIdeal (c.chartSat r g)

A derivation with δ g ∈ (g)^{sat} preserves the saturation (g)^{sat}, whatever δ(x_r) is: from x_rⁱ z = a g, x_rⁱ δz = δ(a g) − i x_r^{i−1} δ(x_r) z ∈ (g)^{sat}.

The chart logarithmic derivations preserve the strict transform's ideal

theorem IsLocalRing.RegularCoords.preservesIdeal_chartSat_smul_chartDerivRingOver {k : Type u_1} [CommRing k] {R : Type u_2} [CommRing R] [Algebra k R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) (hk : c.IsLinearOver k) {h : Fin n} (hh : h < r) : (chartYR c.x r h • c.chartDerivRingOver r hk h).PreservesIdeal (c.chartSat r ((algebraMap R ↥(chartRing c.x r)) (c.x h)))

y_h ∂'_h preserves (x_r y_h)^{sat}: y_h ∂'_h (x_r y_h) = x_r y_h.

theorem IsLocalRing.RegularCoords.preservesIdeal_chartSat_chartDerivRingOver {k : Type u_1} [CommRing k] {R : Type u_2} [CommRing R] [Algebra k R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) (hk : c.IsLinearOver k) {h : Fin n} (hh : h < r) {i : Fin n} (hi : i ≠ h) : (c.chartDerivRingOver r hk i).PreservesIdeal (c.chartSat r ((algebraMap R ↥(chartRing c.x r)) (c.x h)))

∂'_i, i ≠ h, preserves (x_r y_h)^{sat}: ∂'_i (x_r y_h) = y_h if i = r, 0 otherwise, and y_h ∈ (x_r y_h)^{sat}.

theorem IsLocalRing.RegularCoords.chartDlog_le_logDerivative {k : Type u_1} [CommRing k] {R : Type u_2} [CommRing R] [Algebra k R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) (hk : c.IsLinearOver k) {h : Fin n} (hh : h < r) (K : Ideal ↥(chartRing c.x r)) : c.chartDlog r h K ≤ Ideal.logDerivative k (c.chartSat r ((algebraMap R ↥(chartRing c.x r)) (c.x h))) K

D'(−log S₁)(K) (chartDlog) lies in D(−log (x_r y_h)^{sat})(K) (Ideal.logDerivative): the chart logarithmic derivations are k-derivations preserving the strict transform's chart ideal.

theorem IsLocalRing.RegularCoords.chartDlogpow_le_logDerivativeIter {k : Type u_1} [CommRing k] {R : Type u_2} [CommRing R] [Algebra k R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) (hk : c.IsLinearOver k) {h : Fin n} (hh : h < r) (t : ℕ) (K : Ideal ↥(chartRing c.x r)) : c.chartDlogpow r h t K ≤ Ideal.logDerivativeIter k (c.chartSat r ((algebraMap R ↥(chartRing c.x r)) (c.x h))) t K

The iterate: D'^t(−log S₁)(K) ⊆ D^t(−log (x_r y_h)^{sat})(K).