The blow-up lift of a logarithmic derivation

[Kol07, (87.3)], "proved the same way using (75.4)": the logarithmic version of Theorem 76 at the chart level, for an arbitrary ideal. R is any commutative k-algebra, x : Fin n → R, P = chartCenter x r = (x₀, …, x_r), R' = chartRing x r = R[xᵢ/x_r] ⊆ R[1/x_r], φ : R → R', and J ⊆ R any ideal (the ideal of the hypersurface S).

• A k-derivation δ of R preserving J lifts, by Derivation.blowupLift of Hironaka/Algebra/Local/BlowUpLift.lean (Włodarczyk's D' = y σ^*(D), D'(φ a) = φ(x_r · δ a)), to a derivation of R' preserving J R' (blowupLift_preservesIdeal_map; Leibniz on the generators φ(J)) and preserving the x_r-saturation (J R')^{sat} = ⋃ᵢ (J R' : x_rⁱ), the chart-level ideal of the strict transform of V(J) (blowupLift_preservesIdeal_saturation): for z · x_rⁱ ∈ J R', applying D' gives z · D'(x_rⁱ) + x_rⁱ · D'(z) ∈ J R', and D'(x_rⁱ) ∈ (x_rⁱ) because D'(x_r) = x_r φ(δ x_r) (Włodarczyk's "y divides D'(y)" in the proof of [Wlo05, Lemma 2.6.3]), so x_rⁱ D'(z) ∈ J R'.
• Hence, for I ⊆ P^{m+1}, π⁻¹_*(D(−log J)(I), m) ⊆ D(−log (J R')^{sat})(π⁻¹_*(I, m+1)) (transformIdeal_logDerivative_le): on the generators f and δ f of D(−log J)(I), by the transform identity π⁻¹_*(δ f, m) = D'(π⁻¹_*(f, m+1)) + (m+1) φ(δ x_r) π⁻¹_*(f, m+1) of Hironaka/Algebra/Local/BlowUpLiftTransform.lean (Kollár's (75.1)–(75.3) for an arbitrary derivation), with D' now a logarithmic derivation along the saturation. In coordinates with J = (x_h), h < r, this is transform_Dlog_le_chartDlog of Hironaka/Algebra/Local/TransformLogDeriv.lean.

The logarithmic derivative ideal D(−log J) is Ideal.logDerivative k J of Hironaka/Scheme/IdealSheaf/Derivative/Logarithmic.lean. Used for (87.3) on schemes (Hironaka/Scheme/BlowUpSequence/TransformLogDerivative.lean).

theorem Derivation.blowupLift_preservesIdeal_map {k : Type u_1} {R : Type u} [CommRing k] [CommRing R] [Algebra k R] {n : ℕ} (x : Fin n → R) (r : Fin n) (δ : Derivation k R R) (J : Ideal R) (hδ : δ.PreservesIdeal J) : (blowupLift x r δ).PreservesIdeal (Ideal.map (algebraMap R ↥(IsLocalRing.chartRing x r)) J)

A derivation preserving J lifts to a derivation of the chart ring preserving J R'.

theorem Derivation.blowupLift_pow_algebraMap_mem {k : Type u_1} {R : Type u} [CommRing k] [CommRing R] [Algebra k R] {n : ℕ} (x : Fin n → R) (r : Fin n) (δ : Derivation k R R) (i : ℕ) : (blowupLift x r δ) ((algebraMap R ↥(IsLocalRing.chartRing x r)) (x r) ^ i) ∈ Ideal.span {(algebraMap R ↥(IsLocalRing.chartRing x r)) (x r) ^ i}

Włodarczyk's "y divides D'(y)" for the powers: D'(x_rⁱ) ∈ (x_rⁱ).

theorem Derivation.blowupLift_preservesIdeal_saturation {k : Type u_1} {R : Type u} [CommRing k] [CommRing R] [Algebra k R] {n : ℕ} (x : Fin n → R) (r : Fin n) (δ : Derivation k R R) (J : Ideal R) (hδ : δ.PreservesIdeal J) : (blowupLift x r δ).PreservesIdeal (⨆ (i : ℕ), Submodule.colon (Ideal.map (algebraMap R ↥(IsLocalRing.chartRing x r)) J) ↑(Ideal.span {(algebraMap R ↥(IsLocalRing.chartRing x r)) (x r)} ^ i))

The lift also preserves the x_r-saturation ⋃ᵢ (J R' : x_rⁱ) of J R', the chart-level ideal of the strict transform of V(J), because D'(x_r) ∈ (x_r).

theorem Derivation.transformIdeal_logDerivative_le {k : Type u_1} {R : Type u} [CommRing k] [CommRing R] [Algebra k R] {n : ℕ} (x : Fin n → R) (r : Fin n) (J : Ideal R) {I : Ideal R} {m : ℕ} (hI : I ≤ IsLocalRing.chartCenter x r ^ (m + 1)) : IsLocalRing.transformIdeal x r (Ideal.logDerivative k J I) m ≤ Ideal.logDerivative k (⨆ (i : ℕ), Submodule.colon (Ideal.map (algebraMap R ↥(IsLocalRing.chartRing x r)) J) ↑(Ideal.span {(algebraMap R ↥(IsLocalRing.chartRing x r)) (x r)} ^ i)) (IsLocalRing.transformIdeal x r I (m + 1))

[Kol07, (87.3)] for one blow-up and j = 1, at the chart level, for an arbitrary ideal J: for I ⊆ P^{m+1}, π⁻¹_*(D(−log J)(I), m) ⊆ D(−log (J R')^{sat})(π⁻¹_*(I, m + 1)).