The transform of a derivative in the chart of a blow-up: the identities

The computation of Włodarczyk's proof of [Wlo05, Lemma 2.6.3] for an arbitrary derivation, in the local model: R a commutative k-algebra, the centre P = ⟨x₀, …, x_r⟩, the chart ring R' = R[xᵢ/x_r : i < r], y = x_r, φ : R → R', a k-derivation δ of R and its lift D' = Derivation.blowupLift to R' (Hironaka/Algebra/Local/BlowUpLift.lean, Włodarczyk's y σ^*(D)):

• D'(φ a) = φ(x_r · δ a) (blowupLift_algebraMap) and in particular D'(y) = y · φ(δ y) ∈ (y) (blowupLift_exc, Włodarczyk's "y divides D'(y)").
• The transform identity (transformElem_derivation). For f ∈ P^{m+1} write g = π⁻¹_*(f, m+1) = f / y^{m+1}; then δ f ∈ Pᵐ (a derivation lowers the P-order by at most one) and π⁻¹_*(δ f, m) = D'(g) + (m+1) · φ(δ y) · g. Proof: apply the extension δ̃ of δ to R[1/y] to y^{m+1} g = φ f: φ(δ f) = (m+1) yᵐ δ̃(y) g + y^{m+1} δ̃(g) = yᵐ ((m+1) φ(δ y) g + D'(g)), and π⁻¹_*(δ f, m) is the unique element of R' whose product with yᵐ is φ(δ f) (eq_transformElem_of_pow_mul_eq, Hironaka/Algebra/Local/Transform.lean). This is Włodarczyk's D'(y f) = y D'(f) + D'(y) f, D'(y^μ J) ⊆ y^μ (D'(J) + J), and it specialises to Kollár's (75.1)–(75.3) for δ = ∂ⱼ (Hironaka/Algebra/Local/TransformDeriv.lean: δ y = 0 for j ≠ r, δ y = 1 for j = r).
• The inclusion (transformIdeal_derivative_le): for I ≤ P^{m+1}, π⁻¹_*(D(I), m) ≤ D(π⁻¹_*(I, m+1)). Since yᵐ · π⁻¹_*(D(I), m) = D(I) R' (span_pow_mul_transformIdeal) and multiplication by yᵐ is injective on R', it suffices that D(I) R' ⊆ yᵐ · D(J), J = π⁻¹_*(I, m+1); by derivative_le_iff this is checked on the generators of D(I): φ f = yᵐ · (y g) with g ∈ J, and φ(δ f) = yᵐ · π⁻¹_*(δ f, m) with π⁻¹_*(δ f, m) = D'(g) + (m+1) φ(δ y) g ∈ D(J) by the transform identity. This is Włodarczyk's σ^c(D(I)) = y^{−μ+1} σ^*(D(I)) ⊆ y^{−μ} D'(y^μ σ^c(I)) ⊆ D(σ^c(I)) and Kollár's observation in [Kol07, 75] that "the right-hand sides of these equations are in D(π⁻¹_*(f, m))".

The derivative ideal D is Ideal.derivative k of Hironaka/Algebra/Derivative/Basic.lean, over all k-derivations, for the k-algebra structure of R' ⊆ R[1/x_r] induced through R. The inclusion is the local input of [Kol07, Theorem 76] for one blow-up on schemes (Hironaka/Scheme/BlowUpSequence/TransformDerivative.lean); its logarithmic version is Hironaka/Algebra/Local/BlowUpLiftLog.lean.

theorem Derivation.blowupLift_algebraMap {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) (a : R) : (blowupLift x r δ) ((algebraMap R ↥(IsLocalRing.chartRing x r)) a) = (algebraMap R ↥(IsLocalRing.chartRing x r)) (x r * δ a)

The lift agrees with x_r · δ on the image of R (the proof of [Wlo05, Lemma 2.6.3]).

theorem Derivation.blowupLift_exc {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) : (blowupLift x r δ) ((algebraMap R ↥(IsLocalRing.chartRing x r)) (x r)) ∈ Ideal.span {(algebraMap R ↥(IsLocalRing.chartRing x r)) (x r)}

Włodarczyk's "y divides D'(y)" (the proof of [Wlo05, Lemma 2.6.3]): D'(x_r) = x_r · φ(δ x_r) ∈ (x_r).

theorem Derivation.transformElem_derivation {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) {m : ℕ} {f : R} (hf : f ∈ IsLocalRing.chartCenter x r ^ (m + 1)) : IsLocalRing.transformElem x r (δ f) ⋯ = (blowupLift x r δ) (IsLocalRing.transformElem x r f hf) + (m + 1) • ((algebraMap R ↥(IsLocalRing.chartRing x r)) (δ (x r)) * IsLocalRing.transformElem x r f hf)

The transform identity (the proof of [Wlo05, Lemma 2.6.3]; [Kol07, (75.1)–(75.3)] for an arbitrary derivation): for f ∈ P^{m+1}, π⁻¹_*(δ f, m) = D'(π⁻¹_*(f, m+1)) + (m+1) · φ(δ x_r) · π⁻¹_*(f, m+1).

theorem Derivation.transformIdeal_derivative_le {k : Type u_1} {R : Type u} [CommRing k] [CommRing R] [Algebra k R] {n : ℕ} (x : Fin n → R) (r : Fin n) {I : Ideal R} {m : ℕ} (hI : I ≤ IsLocalRing.chartCenter x r ^ (m + 1)) : IsLocalRing.transformIdeal x r (Ideal.derivative k I) m ≤ Ideal.derivative k (IsLocalRing.transformIdeal x r I (m + 1))

The transform of the derivative ideal ([Wlo05, Lemma 2.6.3], σ^c(D(I)) ⊆ D(σ^c(I)); [Kol07, 75] and [Kol07, Theorem 76] for one blow-up): for I ≤ P^{m+1}, π⁻¹_*(D(I), m) ≤ D(π⁻¹_*(I, m+1)) in the chart ring.