The logarithmic version of Theorem 76 for one smooth blow-up

Kollár's logarithmic version of Theorem 76, equation (87.3) of [Kol07, 87]: for a smooth blow-up π : B_Z X → X with center Z ⊆ S and ord_Z I ≥ m + 1, π_*^{-1}(D(−log S)(I), m) ⊆ D(−log S₁)(π_*^{-1}(I, m + 1)), S₁ the strict transform of S (markedTransform_logDerivative_le); and for ord_Z I ≥ m, j ≤ m, π_*^{-1}(D^j(−log S)(I), m − j) ⊆ D^j(−log S₁)(π_*^{-1}(I, m)) (markedTransform_logDerivativeIter_le, by induction on j as for Theorem 76). Kollár says it "is proved the same way using (75.4)"; the proof here is that of Hironaka/Scheme/BlowUpSequence/TransformDerivative.lean, stalkwise on B_Z X, in the logarithmic vocabulary of Hironaka/Scheme/IdealSheaf/Derivative/LogarithmicSheaf.lean.

• Off the center (stalkIdeal_markedTransform_logDerivative_le_of_notMem): the marked transforms are the total transforms π^* K_z along the isomorphism π^♯ : 𝒪_{X,z} ≅ 𝒪_{B,q} (stalkMapπEquiv), the stalk of S₁ is π^*(S_z) (the saturation by the unit exceptional stalk), and D(−log ·) is transported along a ring isomorphism respecting the k-structures (Ideal.logDerivative_map_ringEquiv: conjugation of a derivation preserves the transported ideal).
• Over the center (stalkIdeal_markedTransform_logDerivative_le_of_mem): the chart description e : 𝒪_{B,q} ≅ R'_𝔮 of the stalk, with R' = 𝒪_{X,z}[yᵢ/y_ρ] the chart ring at P = Z_z; the stalk of π_*^{-1}(K, c) is the colon (π^* K_z : (π^♯ y_ρ)^c) (stalkIdeal_markedTransform_of_chart), so t · (π^♯ y_ρ)^m ∈ D(−log S_z)(I_z) 𝒪_{B,q}, which is (π^♯ y_ρ)^m · π_*^{-1}(D(−log S_z)(I_z), m) 𝒪_{B,q}, and t lies in the localization of the chart transform (π^♯ y_ρ a nonzerodivisor). The chart-level inclusion transformIdeal_logDerivative_le puts that transform inside D(−log (S_z R')^{sat})(π_*^{-1}(I_z, m + 1)), Ideal.map_logDerivative_le carries D(−log ·) through the localization R' → 𝒪_{B,q}, and the localized saturation ⋃ᵢ (S_z R' : y_ρⁱ) 𝒪_{B,q} is the stalk (S₁)_q = ⋃ᵢ (π^* S_z : (π^♯ y_ρ)ⁱ) (stalkIdeal_saturate_of_isInvertible, and the colon by a finitely generated ideal commutes with localization, map_colon_of_fg). Finally π_*^{-1}(I_z, m + 1) 𝒪_{B,q} ⊆ T_q as for Theorem 76.

Conventions. The statements assume no smoothness of S or of S₁: the stalk formula stalkIdeal_logDerivative holds for every closed subscheme, and the saturation is compared with the stalk of the strict transform directly. Nor do they assume Kollár's hypothesis Z ⊆ S: the chart lemma holds for every ideal J, and the strict transform of S is defined for every S; the theorems here are stated for an arbitrary closed subscheme S.

Logarithmic derivative ideals and ring isomorphisms

theorem Ideal.logDerivative_map_ringEquiv {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] (e : A ≃+* B) (hk : ∀ (a : k), e ((algebraMap k A) a) = (algebraMap k B) a) (J I : Ideal A) : map e.toRingHom (logDerivative k J I) = logDerivative k (map e.toRingHom J) (map e.toRingHom I)

The logarithmic derivative ideal is transported by a ring isomorphism respecting the k-structures: D(−log J)(I) B = D(−log (J B))(I B) — derivations are conjugated along e, and conjugation preserves the transported ideal.

theorem AlgebraicGeometry.stalkIdeal_markedTransform_logDerivative_le_of_notMem {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (Z S I : X.IdealSheafData) {m : ℕ} (q : ↥Z.blowUp) (hq : Z.blowUpπ q ∉ Z.support) : ((Scheme.IdealSheafData.logDerivative f S I).markedTransform Z m).stalkIdeal q ≤ Ideal.logDerivative k ((S.strictTransform Z).stalkIdeal q) ((I.markedTransform Z (m + 1)).stalkIdeal q)

Off the center: at q with π q ∉ Z, the marked transforms are the total transforms along the isomorphism π^♯, the stalk of S₁ is π^*(S_z), and D(−log ·) is transported along the isomorphism.

theorem AlgebraicGeometry.stalkIdeal_markedTransform_logDerivative_le_of_mem {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (Z S I : X.IdealSheafData) [CharZero k] [Smooth (CategoryTheory.CategoryStruct.comp Z.subschemeι f)] {m : ℕ} (hm : I.LeOrdAlong Z.support ↑(m + 1)) (q : ↥Z.blowUp) (hq : Z.blowUpπ q ∈ Z.support) : ((Scheme.IdealSheafData.logDerivative f S I).markedTransform Z m).stalkIdeal q ≤ Ideal.logDerivative k ((S.strictTransform Z).stalkIdeal q) ((I.markedTransform Z (m + 1)).stalkIdeal q)

Over the center, through the chart description of the stalk at q: the chart-level inclusion transformIdeal_logDerivative_le, localized at the prime 𝔮 of the fibre and transported along e, with the localized saturation identified with the stalk of the strict transform.

theorem AlgebraicGeometry.markedTransform_logDerivative_le {k : Type u} [Field k] {X : Scheme} [CharZero k] (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (Z : X.IdealSheafData) [Smooth (CategoryTheory.CategoryStruct.comp Z.subschemeι f)] (S I : X.IdealSheafData) {m : ℕ} (hm : I.LeOrdAlong Z.support ↑(m + 1)) : (Scheme.IdealSheafData.logDerivative f S I).markedTransform Z m ≤ Scheme.IdealSheafData.logDerivative (CategoryTheory.CategoryStruct.comp Z.blowUpπ f) (S.strictTransform Z) (I.markedTransform Z (m + 1))

Equation (87.3) of [Kol07, 87] for j = 1 and one blow-up: for a smooth blow-up with ord_Z I ≥ m + 1 along every component of the center, and any closed S (Kollár's Z ⊆ S is not assumed), π_*^{-1}(D(−log S)(I), m) ⊆ D(−log S₁)(π_*^{-1}(I, m + 1)), S₁ the strict transform of S.

One blow-up, all j

theorem AlgebraicGeometry.markedTransform_logDerivativeIter_le {k : Type u} [Field k] {X : Scheme} [CharZero k] (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (Z : X.IdealSheafData) [Smooth (CategoryTheory.CategoryStruct.comp Z.subschemeι f)] (S I : X.IdealSheafData) {m : ℕ} (hm : I.LeOrdAlong Z.support ↑m) {j : ℕ} (hj : j ≤ m) : (Scheme.IdealSheafData.logDerivativeIter f S j I).markedTransform Z (m - j) ≤ Scheme.IdealSheafData.logDerivativeIter (CategoryTheory.CategoryStruct.comp Z.blowUpπ f) (S.strictTransform Z) j (I.markedTransform Z m)

Equation (87.3) of [Kol07, 87] for one blow-up, by induction on j as in Theorem 76: for a smooth blow-up with ord_Z I ≥ m, any closed S, and j ≤ m, π_*^{-1}(D^j(−log S)(I), m − j) ⊆ D^j(−log S₁)(π_*^{-1}(I, m)).