Theorem 88: the parts that need no coordinates

[Kol07, Theorem 88] describes the derivatives D^s Π_*^{-1}(I, m) of the transform of a marked ideal along a smooth blow-up sequence of order ≥ m whose centers lie in the transforms of a smooth hypersurface S, as the sum (88.1) of logarithmic derivatives along S_r of the transforms of the derivatives D^j I. This module collects the parts of its proof that need no coordinates; the chart computation is in Hironaka/Resolution/Algebraic/Kol07/Theorem88BlowUp.lean and the induction along the sequence in Hironaka/Resolution/Algebraic/Kol07/Theorem88Sequence.lean.

• The inclusion ⊇. "Using (76) we obtain … thus the right-hand side of (88.1) is contained in the left-hand side": at every stage of a smooth blow-up sequence of order ≥ m, for j ≤ s ≤ m and any closed S, D^{s−j}(−log S_i) Π_*^{-1}(D^j I, m − j) ⊆ D^{s−j} Π_*^{-1}(D^j I, m − j), which lies in D^{s−j} D^j Π_*^{-1}(I, m) = D^s Π_*^{-1}(I, m) (logDerivativeIter_le_derivativeIter, markedTransformSeq_derivativeIter_le with the monotonicity of D^{s−j}, and D^a D^b = D^{a+b}, [Kol07, Lemma 74 (1)]; logDerivativeIter_markedTransformSeq_le_derivativeIter).
• Off the hypersurface. At a point q ∉ S' the logarithmic derivatives are the derivatives, (D^r(−log S')(K))_q = (D^r K)_q: the stalk formulas with (S')_q = 𝒪_q (stalkIdeal_eq_top_of_notMem_support) and Ideal.logDerivative_top (stalkIdeal_logDerivativeIter_of_notMem_support). This is what makes the charts missing the strict transform of S harmless in Kollár's proof.
• The marked transform of a sum. For marked transforms of the same mark c that are defined (F^c ∣ π^* K_j for every summand), π_*^{-1}(∑ K_j, c) ⊆ ∑ π_*^{-1}(K_j, c): π^* K_j = F^c · π_*^{-1}(K_j, c) for each j (pow_mul_colon_of_dvd), so π^*(∑ K_j) = F^c · ∑ π_*^{-1}(K_j, c), and the colon by the invertible F^c recovers the sum (colon_pow_eq_of_mul_eq); markedTransform_iSup_le, in fact an equality. Kollár uses it to push the transform inside the sum in the inductive step of the proof.
• The composition rule for logarithmic derivatives, D^a(−log S) ∘ D^b(−log S) = D^{a+b}(−log S) (logDerivativeIter_logDerivativeIter, Function.iterate_add_apply), the analogue of [Kol07, Lemma 74 (1)], used at the end of the proof.

theorem Ideal.logDerivativeIter_top {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (r : ℕ) (I : Ideal A) : logDerivativeIter k ⊤ r I = derivativeIter k r I

At ring level (logDerivative_top iterated): along the unit ideal the iterated logarithmic derivatives are the iterated derivatives.

The composition rule for logarithmic derivatives

theorem AlgebraicGeometry.logDerivativeIter_logDerivativeIter {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (S K : X.IdealSheafData) (a b : ℕ) : Scheme.IdealSheafData.logDerivativeIter f S a (Scheme.IdealSheafData.logDerivativeIter f S b K) = Scheme.IdealSheafData.logDerivativeIter f S (a + b) K

The composition rule D^a(−log S)(D^b(−log S)(K)) = D^{a+b}(−log S)(K), the analogue of [Kol07, Lemma 74 (1)] for logarithmic derivatives, used at the end of the proof of [Kol07, Theorem 88].

The marked transform of a sum

theorem AlgebraicGeometry.mul_iSup' {X : Scheme} {ι : Sort u_1} (I : X.IdealSheafData) (J : ι → X.IdealSheafData) : I * ⨆ (i : ι), J i = ⨆ (i : ι), I * J i

Multiplication of ideal sheaves distributes over suprema (sectionwise Submodule.mul_iSup).

theorem AlgebraicGeometry.markedTransform_iSup_le {X : Scheme} (Z : X.IdealSheafData) (K : ℕ → X.IdealSheafData) (s c : ℕ) (hK : ∀ j ≤ s, Z.exceptionalDivisor ^ c ∣ (K j).comap Z.blowUpπ) : (⨆ (j : ℕ), ⨆ (_ : j ≤ s), K j).markedTransform Z c ≤ ⨆ (j : ℕ), ⨆ (_ : j ≤ s), (K j).markedTransform Z c

For marked transforms of the same mark c that are defined, the marked transform of a sum lies in the sum of the marked transforms (in fact equals it): each π^* K_j is F^c · π_*^{-1}(K_j, c), so π^*(⨆ K_j) = F^c · ⨆ π_*^{-1}(K_j, c) and the colon by the invertible F^c recovers ⨆ π_*^{-1}(K_j, c). Used in the inductive step of the proof of [Kol07, Theorem 88].

Off the hypersurface the logarithmic derivatives are the derivatives

theorem AlgebraicGeometry.stalkIdeal_logDerivative_of_notMem_support {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [LocallyOfFiniteType f] (S K : X.IdealSheafData) {q : ↥X} (hq : q ∉ S.support) : (Scheme.IdealSheafData.logDerivative f S K).stalkIdeal q = (Scheme.IdealSheafData.derivative f K).stalkIdeal q

Off the hypersurface the logarithmic derivative is the derivative, at the level of stalks.

theorem AlgebraicGeometry.stalkIdeal_logDerivativeIter_of_notMem_support {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [LocallyOfFiniteType f] (S K : X.IdealSheafData) (r : ℕ) {q : ↥X} (hq : q ∉ S.support) : (Scheme.IdealSheafData.logDerivativeIter f S r K).stalkIdeal q = (Scheme.IdealSheafData.derivativeIter f r K).stalkIdeal q

Off the hypersurface the iterated logarithmic derivatives are the iterated derivatives, (D^r(−log S)(K))_q = (D^r K)_q (the charts missing the strict transform of S in the proof of [Kol07, Theorem 88]).

The inclusion ⊇ of (88.1) along the sequence

theorem AlgebraicGeometry.logDerivativeIter_markedTransformSeq_le_derivativeIter {k : Type u} [Field k] {X : Scheme} [CharZero k] (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (B : X.BlowUpSequence) (S I : X.IdealSheafData) (E : X.DivisorFamily) (m : ℕ) (h : B.IsOrderGeSeq f I m E) {s j : ℕ} (hj : j ≤ s) (hs : s ≤ m) (i : Fin (B.length + 1)) : Scheme.IdealSheafData.logDerivativeIter (CategoryTheory.CategoryStruct.comp (B.stageMap i) f) (B.strictTransformSeq S i) (s - j) (B.markedTransformSeq (Scheme.IdealSheafData.derivativeIter f j I) (m - j) i) ≤ Scheme.IdealSheafData.derivativeIter (CategoryTheory.CategoryStruct.comp (B.stageMap i) f) s (B.markedTransformSeq I m i)

"Using (76) we obtain … the right-hand side of (88.1) is contained in the left-hand side" (the proof of [Kol07, Theorem 88]): every summand of the right-hand side of (88.1) lies in the left-hand side, at every stage, for every closed S: D^{s−j}(−log S_i) J_i^{(j)} ⊆ D^{s−j} J_i^{(j)} ⊆ D^{s−j} D^j I_i = D^s I_i.