Birational transform of derivatives

Let R be a regular local ring containing ℚ with coordinates x₀, …, x_{n−1} (RegularCoords), P = (x₀, …, x_r) the centre of the blow-up, R' = R[xᵢ/x_r : i < r] ⊆ R[1/x_r] the chart ring dividing by x_r, with the coordinates yᵢ = xᵢ/x_r (i < r), yⱼ = xⱼ (j ≥ r), and ∂'ⱼ the derivations of R' transported from the partial derivatives ∂ⱼ of R (chartDerivRing, Hironaka/Algebra/Local/Chart.lean). For f ∈ Pᵐ the transform π⁻¹_*(f, m) = f / x_rᵐ lies in R' (transformElem, Hironaka/Algebra/Local/BirationalTransform.lean). This module computes the derivatives of transforms, [Kol07, 75]:

• (75.1) π⁻¹_*(∂ⱼ f, m) = ∂'ⱼ π⁻¹_*(f, m+1) for j < r (transform_pderiv_lt);
• (75.2) π⁻¹_*(∂ⱼ f, m) = y_r ∂'ⱼ π⁻¹_*(f, m+1) for j > r (transform_pderiv_gt);
• (75.3) `π⁻¹_(∂_r f, m) = y_r ∂'r π⁻¹(f, m+1) − ∑{i<r} yᵢ ∂'ᵢ π⁻¹*(f, m+1)
  • (m+1) π⁻¹_*(f, m+1) (transform_pderiv_eq`);
• (75.4) π⁻¹_*(xⱼ ∂ⱼ f, m) = y_r yⱼ ∂'ⱼ π⁻¹_*(f, m+1) for j < r (transform_x_pderiv).

All four follow from one computation in R[1/x_r]: with u = 1/x_r, ∂ⱼ(f uᵐ) = (∂ⱼ f) uᵐ − m [j = r] f u^{m+1} (awayPderiv_algebraMap_mul_invX_pow).

Kollár observes that the right-hand sides lie in the derivative ideal of π⁻¹_*(f, m), which is the case of one blow-up and j = 1 of [Kol07, Theorem 76]: for an ideal I ≤ Pᵐ⁺¹, π⁻¹_*(D(I), m) ≤ D'(π⁻¹_*(I, m+1)) (transform_D_le_chartD), where D' is the derivative ideal of the chart ring with respect to the ∂'ⱼ (chartD); the same holds with the derivative ideal for all ℚ-derivations of R' (transform_D_le_Dimg_transform). The proof uses that D(I) is generated by the elements of I and their partial derivatives, and that transforms are additive and R-linear (transformElem_add, transformElem_smul), with π⁻¹_*(f, m) = x_r π⁻¹_*(f, m+1) (transformElem_succ).

The same computation in the form of [Wlo05, Lemma 2.6.3] (and, with the coordinates of the centre indexed last, [BM08, Lemma 3.1]): the derivations x_r ∂ⱼ of R[1/x_r] preserve the chart ring (smul_awayPderiv_mem), with x_r ∂ⱼ = ∂'ⱼ for j < r, x_r ∂_r = y_r ∂'_r − ∑_{i<r} yᵢ ∂'ᵢ, and x_r ∂ⱼ = y_r ∂'ⱼ for j > r (smul_awayPderiv_of_lt, smul_awayPderiv_self, smul_awayPderiv_of_gt).

Conventions: indices are zero-based, so Kollár's x₁, …, x_r are x₀, …, x_r here, and the marks are shifted by one: the statements are for f ∈ Pᵐ⁺¹, with π⁻¹_*(∂ⱼ f, m) defined because ∂ⱼ(Pᵐ⁺¹) ≤ Pᵐ (pderiv_mem_chartCenter_pow).

The inclusion transform_D_le_chartD is the local input of Theorem 76 for one blowing-up on manifolds (Hironaka/Manifold/BlowUp/Transform/DerivTransform.lean) and of the worked example HironakaExamples/DerivativeSequence.lean; the logarithmic version is Hironaka/Algebra/Local/TransformLogDeriv.lean, the iterated version on a generator Hironaka/Algebra/Local/TransformDerivIter.lean, and the derivations x_r ∂ⱼ are lifted to the blow-up in Hironaka/Algebra/Local/BlowUpLift.lean.

Derivatives lower the power of the centre

theorem IsLocalRing.RegularCoords.pderiv_mem_chartCenter_pow {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) {m : ℕ} {f : R} (hf : f ∈ chartCenter c.x r ^ m) (j : Fin n) : (c.pderiv j) f ∈ chartCenter c.x r ^ (m - 1)

∂ⱼ(Pᵐ) ≤ Pᵐ⁻¹: the partial derivative of an element of Pᵐ lies in Pᵐ⁻¹, so π⁻¹_*(∂ⱼ f, m − 1) is defined for f ∈ Pᵐ.

theorem IsLocalRing.RegularCoords.D_le_chartCenter_pow {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) {I : Ideal R} {m : ℕ} (hI : I ≤ chartCenter c.x r ^ (m + 1)) : c.D I ≤ chartCenter c.x r ^ m

For ideals: I ≤ Pᵐ⁺¹ gives D(I) ≤ Pᵐ.

The computation in R[1/x_r]

theorem IsLocalRing.RegularCoords.mk_eq_algebraMap_mul_invX_pow {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) (f : R) (m : ℕ) : Localization.mk f ⟨c.x r ^ m, ⋯⟩ = (algebraMap R (Localization.Away (c.x r))) f * invX c.x r ^ m

theorem IsLocalRing.RegularCoords.algebraMap_mul_invX_pow_succ {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) (m : ℕ) : (algebraMap R (Localization.Away (c.x r))) (c.x r) * invX c.x r ^ (m + 1) = invX c.x r ^ m

theorem IsLocalRing.RegularCoords.awayPderiv_invX_pow {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r j : Fin n) (m : ℕ) : (c.awayPderiv r j) (invX c.x r ^ m) = -(m • (invX c.x r ^ (m + 1) * if j = r then 1 else 0))

theorem IsLocalRing.RegularCoords.awayPderiv_algebraMap_mul_invX_pow {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r j : Fin n) (f : R) (m : ℕ) : (c.awayPderiv r j) ((algebraMap R (Localization.Away (c.x r))) f * invX c.x r ^ m) = (algebraMap R (Localization.Away (c.x r))) ((c.pderiv j) f) * invX c.x r ^ m - m • ((algebraMap R (Localization.Away (c.x r))) f * invX c.x r ^ (m + 1) * if j = r then 1 else 0)

The chain-rule computation behind [Kol07, 75]: in R[1/x_r], ∂ⱼ(f uᵐ) = (∂ⱼ f) uᵐ − m [j = r] f u^{m+1} with u = 1/x_r.

theorem IsLocalRing.RegularCoords.coe_transformElem_eq {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) (f : R) {m : ℕ} (hf : f ∈ chartCenter c.x r ^ m) : ↑(transformElem c.x r f hf) = (algebraMap R (Localization.Away (c.x r))) f * invX c.x r ^ m

Kollár's formulas (75.1)–(75.4)

theorem IsLocalRing.RegularCoords.transform_pderiv_lt {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) {j : Fin n} (hj : j < r) {m : ℕ} {f : R} (hf : f ∈ chartCenter c.x r ^ (m + 1)) : transformElem c.x r ((c.pderiv j) f) ⋯ = (c.chartDerivRing r j) (transformElem c.x r f hf)

[Kol07, (75.1)] (also [Wlo05, Lemma 2.6.3]): for j < r and f ∈ Pᵐ⁺¹, π⁻¹_*(∂ⱼ f, m) = ∂'ⱼ π⁻¹_*(f, m+1).

theorem IsLocalRing.RegularCoords.transform_pderiv_gt {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) {j : Fin n} (hj : r < j) {m : ℕ} {f : R} (hf : f ∈ chartCenter c.x r ^ (m + 1)) : transformElem c.x r ((c.pderiv j) f) ⋯ = chartYR c.x r r * (c.chartDerivRing r j) (transformElem c.x r f hf)

[Kol07, (75.2)]: for j > r and f ∈ Pᵐ⁺¹, π⁻¹_*(∂ⱼ f, m) = y_r ∂'ⱼ π⁻¹_*(f, m+1).

theorem IsLocalRing.RegularCoords.transform_pderiv_eq {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) {m : ℕ} {f : R} (hf : f ∈ chartCenter c.x r ^ (m + 1)) : transformElem c.x r ((c.pderiv r) f) ⋯ = chartYR c.x r r * (c.chartDerivRing r r) (transformElem c.x r f hf) - ∑ i : Fin n with i < r, chartYR c.x r i * (c.chartDerivRing r i) (transformElem c.x r f hf) + (m + 1) • transformElem c.x r f hf

[Kol07, (75.3)], by the chain rule (also [Wlo05, Lemma 2.6.3] and [BM08, Lemma 3.1]): for f ∈ Pᵐ⁺¹, π⁻¹_*(∂_r f, m) = y_r ∂'_r π⁻¹_*(f, m+1) − ∑_{i<r} yᵢ ∂'ᵢ π⁻¹_*(f, m+1) + (m+1)·π⁻¹_*(f, m+1), the last term being (m+1, −1)·π⁻¹_*(f, m+1) in Kollár's notation: multiply by m+1 and lower the mark by one.

theorem IsLocalRing.RegularCoords.transform_x_pderiv {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) {j : Fin n} (hj : j < r) {m : ℕ} {f : R} (hf : f ∈ chartCenter c.x r ^ (m + 1)) : transformElem c.x r (c.x j * (c.pderiv j) f) ⋯ = chartYR c.x r r * chartYR c.x r j * (c.chartDerivRing r j) (transformElem c.x r f hf)

[Kol07, (75.4)]: for j < r and f ∈ Pᵐ⁺¹, π⁻¹_*(xⱼ ∂ⱼ f, m) = y_r yⱼ ∂'ⱼ π⁻¹_*(f, m+1).

The derivative ideal of a transform: π⁻¹_*(D(I), m) ≤ D'(π⁻¹_*(I, m+1))

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

The derivative ideal of an ideal J of the chart ring with respect to the transported derivations ∂'ⱼ: J + ∑ⱼ ∂'ⱼ(J) R'.

Equations

• c.chartD r J = J ⊔ ⨆ (j : Fin n), Ideal.span (⇑(c.chartDerivRing r j) '' ↑J)

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

theorem IsLocalRing.RegularCoords.chartDerivRing_mem_chartD {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) {J : Ideal ↥(chartRing c.x r)} {z : ↥(chartRing c.x r)} (hz : z ∈ J) (j : Fin n) : (c.chartDerivRing r j) z ∈ c.chartD r J

theorem IsLocalRing.RegularCoords.transformElem_add {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) {m : ℕ} {f g : R} (hf : f ∈ chartCenter c.x r ^ m) (hg : g ∈ chartCenter c.x r ^ m) (hfg : f + g ∈ chartCenter c.x r ^ m) : transformElem c.x r (f + g) hfg = transformElem c.x r f hf + transformElem c.x r g hg

Transforms are additive and R-linear, by their uniqueness: π⁻¹_*(f, m) is the only element g of the chart ring with x_rᵐ g = f (eq_transformElem_of_pow_mul_eq).

theorem IsLocalRing.RegularCoords.transformElem_smul {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) {m : ℕ} (a : R) {g : R} (hg : g ∈ chartCenter c.x r ^ m) (hag : a • g ∈ chartCenter c.x r ^ m) : transformElem c.x r (a • g) hag = (algebraMap R ↥(chartRing c.x r)) a * transformElem c.x r g hg

theorem IsLocalRing.RegularCoords.transformElem_zero {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) {m : ℕ} (h0 : 0 ∈ chartCenter c.x r ^ m) : transformElem c.x r 0 h0 = 0

theorem IsLocalRing.RegularCoords.transformElem_succ {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) {m : ℕ} {f : R} (hf : f ∈ chartCenter c.x r ^ (m + 1)) (hf' : f ∈ chartCenter c.x r ^ m) : transformElem c.x r f hf' = (algebraMap R ↥(chartRing c.x r)) (c.x r) * transformElem c.x r f hf

Lowering the mark multiplies by x_r: π⁻¹_*(f, m) = x_r · π⁻¹_*(f, m+1).

theorem IsLocalRing.RegularCoords.transform_D_le_chartD {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) {I : Ideal R} {m : ℕ} (hI : I ≤ chartCenter c.x r ^ (m + 1)) : transformIdeal c.x r (c.D I) m ≤ c.chartD r (transformIdeal c.x r I (m + 1))

The derivative ideal of a transform ([Kol07, 75]: "the right-hand sides of these equations are in D(π⁻¹_*(f, m))"; [Wlo05, Lemma 2.6.3]), the case of one blow-up and j = 1 of [Kol07, Theorem 76]: for I ≤ Pᵐ⁺¹, π⁻¹_*(D(I), m) ≤ D'(π⁻¹_*(I, m+1)), with D' the derivative ideal of the chart ring with respect to the ∂'ⱼ.

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

∂'_r y_r = 1, so the identity g = ∂(y g) − y ∂g of [Kol07, Definition 73] puts J inside Dimg J, the derivative ideal of the chart ring for all ℚ-derivations.

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

theorem IsLocalRing.RegularCoords.transform_D_le_Dimg_transform {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) {I : Ideal R} {m : ℕ} (hI : I ≤ chartCenter c.x r ^ (m + 1)) : transformIdeal c.x r (c.D I) m ≤ Dimg (transformIdeal c.x r I (m + 1))

The inclusion transform_D_le_chartD in the coordinate-free form of [Kol07, (73.1)]: π⁻¹_*(D(I), m) ≤ D(π⁻¹_*(I, m+1)) with D the derivative ideal for all ℚ-derivations of the chart ring.

The derivations x_r ∂ⱼ of the chart ring ([Wlo05, Lemma 2.6.3], [BM08, Lemma 3.1])

theorem IsLocalRing.RegularCoords.smul_awayPderiv_of_lt {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) {j : Fin n} (hj : j < r) : (algebraMap R (Localization.Away (c.x r))) (c.x r) • c.awayPderiv r j = c.chartDeriv r j

x_r ∂ⱼ = ∂'ⱼ for j < r ([Wlo05, Lemma 2.6.3]).

theorem IsLocalRing.RegularCoords.smul_awayPderiv_of_gt {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) {j : Fin n} (hj : r < j) : (algebraMap R (Localization.Away (c.x r))) (c.x r) • c.awayPderiv r j = chartY c.x r r • c.chartDeriv r j

x_r ∂ⱼ = y_r ∂'ⱼ for j > r, that is, ∂ⱼ = ∂'ⱼ on the coordinates outside the centre ([Wlo05, Lemma 2.6.3]; the first line of [BM08, Lemma 3.1]).

theorem IsLocalRing.RegularCoords.smul_awayPderiv_self {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) : (algebraMap R (Localization.Away (c.x r))) (c.x r) • c.awayPderiv r r = chartY c.x r r • c.chartDeriv r r - ∑ i : Fin n with i < r, chartY c.x r i • c.chartDeriv r i

x_r ∂_r = y_r ∂'_r − ∑_{i<r} yᵢ ∂'ᵢ ([Wlo05, Lemma 2.6.3]; the second line of [BM08, Lemma 3.1]).

theorem IsLocalRing.RegularCoords.smul_awayPderiv_mem {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r j : Fin n) {z : Localization.Away (c.x r)} (hz : z ∈ chartRing c.x r) : ((algebraMap R (Localization.Away (c.x r))) (c.x r) • c.awayPderiv r j) z ∈ chartRing c.x r

x_r ∂ⱼ preserves the chart ring for every j; in the words of [Wlo05, Lemma 2.6.3], "any derivation D of O_X induces a derivation yσ^*(D) of O_{X'}".