The logarithmic version of Theorem 76 along a blow-up sequence

Kollár's logarithmic version of Theorem 76, equation (87.3) of [Kol07, 87], along a smooth blow-up sequence B of order ≥ m starting with (X, I, m, E), for any closed S (the statements drop Kollár's hypothesis that every center lies in the strict transform S_i of S, which the proofs do not require): for j ≤ m and every stage i, Π_*^{-1}(D^j(−log S)(I), m − j) ⊆ D^j(−log S_i)(Π_*^{-1}(I, m)) (markedTransformSeq_logDerivativeIter_le), and the marked transforms of the logarithmic derivative sequence are defined at every stage (exceptionalAt_pow_dvd_comap_step_logDerivativeIter).

The joint induction (as for Theorem 76 in Hironaka/Scheme/BlowUpSequence/DerivativeSequence.lean, and as in [Wlo05, Lemma 2.6.4]). Induction on the sequence B: for nil the statement is the identity; for cons X D rest, at the first stage the one-blow-up statement of Hironaka/Scheme/BlowUpSequence/TransformLogDerivative.lean (markedTransform_logDerivativeIter_le), then the marked recursion is monotone in its starting ideal (markedTransformSeq_mono) and the tail is a sequence of order ≥ m for the transformed data (B_D X, π_*^{-1}(I, m), E_1) with the hypersurface S₁ = strictTransform D S, to which the induction hypothesis applies. Definedness at every stage is that of the derivative sequence (exceptionalAt_pow_dvd_comap_step_derivativeIter), transported to the smaller ideals D^j(−log S)(I) ⊆ D^j(I) (logDerivativeIter_le_derivativeIter) by the antitonicity of the order (ord_anti) and the monotonicity of the marked recursion.

Convention: in the printed (87.3) the subscripts of S appear interchanged; here S is on the left and its transform S_i on the right.

theorem AlgebraicGeometry.markedTransformSeq_logDerivativeIter_le {X : Scheme} {k : Type u} [Field k] [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) {j : ℕ} (hj : j ≤ m) (i : Fin (B.length + 1)) : B.markedTransformSeq (Scheme.IdealSheafData.logDerivativeIter f S j I) (m - j) i ≤ Scheme.IdealSheafData.logDerivativeIter (CategoryTheory.CategoryStruct.comp (B.stageMap i) f) (B.strictTransformSeq S i) j (B.markedTransformSeq I m i)

Equation (87.3) of [Kol07, 87] along the sequence: for a smooth blow-up sequence of order ≥ m starting with (X, I, m, E), any closed S, and j ≤ m, Π_*^{-1}(D^j(−log S)(I), m − j) ⊆ D^j(−log S_i)(Π_*^{-1}(I, m)) at every stage, S_i the strict transform of S.

theorem AlgebraicGeometry.exceptionalAt_pow_dvd_comap_step_logDerivativeIter {X : Scheme} {k : Type u} [Field k] [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) {j : ℕ} (hj : j ≤ m) (i : Fin B.length) : B.exceptionalAt i ^ (m - j) ∣ (B.markedTransformSeq (Scheme.IdealSheafData.logDerivativeIter f S j I) (m - j) i.castSucc).comap (B.step i)

The marked transform (π_i)_*^{-1}(J_i, m − j) of the logarithmic derivative sequence J_i := Π_*^{-1}(D^j(−log S)(I), m − j) is defined at every stage in the sense of [Kol07, Definition 60] (F_{i+1}^{m−j} divides π_i^* J_i), because D^j(−log S)(I) ⊆ D^j(I) and the derivative sequence is defined (exceptionalAt_pow_dvd_comap_step_derivativeIter).