Birational transform of logarithmic derivatives

The logarithmic version of the derivative computation of Hironaka/Algebra/Local/TransformDeriv.lean, [Kol07, (87.3)]: when the centre of the blow-up lies in a smooth hypersurface S (the hypothesis of [Kol07, Theorem 84]), the logarithmic derivative ideals satisfy the analogue of [Kol07, Theorem 76], Π⁻¹_*(D^j(−log S_r)(I, m)) ⊆ D^j(−log S)(Π⁻¹_*(I, m)), which Kollár says is "proved the same way using (75.4)".

Setting: R a regular local ring containing ℚ with coordinates x₀, …, x_{n−1}, the chart of the blow-up of P = (x₀, …, x_r) dividing by x_r, and S = V(x_h) with h < r (Kollár's x₁ ≠ x_r), whose birational transform in the chart is S₁ = V(y_h). The module defines the logarithmic derivative ideal of an ideal J of the chart ring along S₁, for the transported derivations ∂'ⱼ: D'(−log S₁)(J) = J + y_h ∂'_h(J) R' + ∑_{j ≠ h} ∂'ⱼ(J) R' (chartDlog, the definition of [Kol07, 87] for the chart ring; the chart ring is not local, so the logarithmic derivative ideal Dlog of Hironaka/Algebra/Local/LogDeriv.lean does not apply to it directly), together with its iterates chartDlogpow, and proves for I ≤ Pᵐ⁺¹

π⁻¹_*(D(−log S)(I), m) ≤ D'(−log S₁)(π⁻¹_*(I, m+1)) (transform_Dlog_le_chartDlog)

and, by iteration, for I ≤ Pᵐ⁺ʲ, π⁻¹_*(D^j(−log S)(I), m) ≤ D'^j(−log S₁)(π⁻¹_*(I, m+j)) (transform_Dlogpow_le_chartDlogpow).

The proof follows Kollár's indication. On the generators of D(−log S)(I): f transforms into x_r π⁻¹_*(f, m+1); x_h ∂_h f into y_r y_h ∂'_h π⁻¹_*(f, m+1) by (75.4); ∂ⱼ f for j ≠ h, r into ∂'ⱼ π⁻¹_*(f, m+1) or y_r ∂'ⱼ π⁻¹_*(f, m+1) by (75.1)–(75.2); and ∂_r f by (75.3) into a combination of y_r ∂'_r, y_h ∂'_h and the ∂'ᵢ (i < r, i ≠ h) applied to π⁻¹_*(f, m+1), plus a multiple of π⁻¹_*(f, m+1), all logarithmic along S₁. To check an inclusion π⁻¹_*(J, m) ≤ K on generators of J, the set {g ∈ Pᵐ | π⁻¹_*(g, m) ∈ K} is shown to be an ideal of R (transformPreimage).

Used for the logarithmic derivations of the blow-up (Hironaka/Algebra/Local/BlowUpLiftLog.lean, Hironaka/Algebra/Local/ChartLogDerivations.lean), for the inclusion ⊆ of [Kol07, (88.1)] (Hironaka/Algebra/Local/TransformDerivNormalForm.lean), and for Theorem 76 and its logarithmic version on manifolds (Hironaka/Manifold/BlowUp/Transform/DerivTransform.lean, Hironaka/Manifold/BlowUp/Transform/LogDerivBlowUp.lean).

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

The logarithmic derivative ideal of an ideal J of the chart ring along S₁ = V(y_h), for the transported derivations ∂'ⱼ: J + y_h ∂'_h(J) R' + ∑_{j ≠ h} ∂'ⱼ(J) R' (the definition of [Kol07, 87] for the chart ring).

Equations

• One or more equations did not get rendered due to their size.

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

D'^j(−log S₁), the j-th iterate of chartDlog.

Equations

• c.chartDlogpow r h j J = (c.chartDlog r h)^[j] J

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

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

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

theorem IsLocalRing.RegularCoords.chartDlog_le_iff {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r h : Fin n) {J K : Ideal ↥(chartRing c.x r)} : c.chartDlog r h J ≤ K ↔ J ≤ K ∧ (∀ z ∈ J, chartYR c.x r h * (c.chartDerivRing r h) z ∈ K) ∧ ∀ (j : Fin n), j ≠ h → ∀ z ∈ J, (c.chartDerivRing r j) z ∈ K

The generator description of D'(−log S₁)(J): it lies in K if and only if J, y_h ∂'_h(J) and the ∂'ⱼ(J), j ≠ h, do.

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

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

D'(−log S₁)(J) ≤ D'(J), the derivative ideal of the chart ring for all the ∂'ⱼ (chartD).

@[simp]

theorem IsLocalRing.RegularCoords.chartDlogpow_zero {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r h : Fin n) (J : Ideal ↥(chartRing c.x r)) : c.chartDlogpow r h 0 J = J

theorem IsLocalRing.RegularCoords.chartDlogpow_succ {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r h : Fin n) (j : ℕ) (J : Ideal ↥(chartRing c.x r)) : c.chartDlogpow r h (j + 1) J = c.chartDlog r h (c.chartDlogpow r h j J)

theorem IsLocalRing.RegularCoords.chartDlogpow_mono {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r h : Fin n) (j : ℕ) {J K : Ideal ↥(chartRing c.x r)} (hJK : J ≤ K) : c.chartDlogpow r h j J ≤ c.chartDlogpow r h j K

The marks: D^j(−log S)(I) ≤ D^j(I) ≤ Pᵐ for I ≤ Pᵐ⁺ʲ

theorem IsLocalRing.RegularCoords.Dpow_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 j : ℕ} (hI : I ≤ chartCenter c.x r ^ (m + j)) : c.Dpow j I ≤ chartCenter c.x r ^ m

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

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

The transform of the logarithmic derivative ideal

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

{g ∈ Pᵐ | π⁻¹_*(g, m) ∈ K} is an ideal of R, since transforms are additive and R-linear: the device for checking π⁻¹_*(J, m) ≤ K on generators of J.

Equations

• c.transformPreimage r m K = { carrier := {g : R | ∃ (hg : g ∈ IsLocalRing.chartCenter c.x r ^ m), IsLocalRing.transformElem c.x r g hg ∈ K}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem IsLocalRing.RegularCoords.mem_transformPreimage {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) {m : ℕ} {K : Ideal ↥(chartRing c.x r)} {g : R} : g ∈ c.transformPreimage r m K ↔ ∃ (hg : g ∈ chartCenter c.x r ^ m), transformElem c.x r g hg ∈ K

theorem IsLocalRing.RegularCoords.transformIdeal_le_of_le_transformPreimage {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) {J : Ideal R} {m : ℕ} (hJ : J ≤ chartCenter c.x r ^ m) {K : Ideal ↥(chartRing c.x r)} (hle : J ≤ c.transformPreimage r m K) : transformIdeal c.x r J m ≤ K

theorem IsLocalRing.RegularCoords.transform_Dlog_le_chartDlog {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 + 1)) : transformIdeal c.x r (c.Dlog h I) m ≤ c.chartDlog r h (transformIdeal c.x r I (m + 1))

Transform of the logarithmic derivative ideal ([Kol07, (87.3)] for one blow-up and j = 1, "proved the same way using (75.4)"): for S = V(x_h) with h < r and I ≤ Pᵐ⁺¹, π⁻¹_*(D(−log S)(I), m) ≤ D'(−log S₁)(π⁻¹_*(I, m+1)). On the generators of D(−log S)(I): f ↦ x_r π⁻¹_*(f, m+1); x_h ∂_h f ↦ y_r y_h ∂'_h π⁻¹_*(f, m+1) by (75.4); ∂ⱼ f, j ≠ h, by (75.1)–(75.3), where in (75.3) the term y_h ∂'_h π⁻¹_*(f, m+1) of the sum is the logarithmic generator and the other yᵢ ∂'ᵢ π⁻¹_*(f, m+1) are multiples of the ∂'ᵢ, i ≠ h.

theorem IsLocalRing.RegularCoords.transform_Dlogpow_le_chartDlogpow {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 j : ℕ} (hI : I ≤ chartCenter c.x r ^ (m + j)) : transformIdeal c.x r (c.Dlogpow h j I) m ≤ c.chartDlogpow r h j (transformIdeal c.x r I (m + j))

[Kol07, (87.3)] in the chart, j-fold, by iterating transform_Dlog_le_chartDlog: for I ≤ Pᵐ⁺ʲ, π⁻¹_*(D^j(−log S)(I), m) ≤ D'^j(−log S₁)(π⁻¹_*(I, m+j)).