Theorem 88 along a blow-up sequence

[Kol07, Theorem 88]: for a smooth blow-up sequence Π : X_r → ⋯ → X of order ≥ m with every center Z_i ⊆ S_i, S a smooth hypersurface with strict transforms S_i, and s ≤ m, at every stage D^s Π_*^{-1}(I, m) = ∑_{j ≤ s} D^{s−j}(−log S_i) Π_*^{-1}(D^j I, m − j) (88.1). This is the form in which the derivatives of the transform of a marked ideal are controlled in the going-up theorem for D-balanced ideals (Hironaka/Resolution/Algebraic/Kol07/Corollary89.lean).

The induction on the sequence (Kollár's (88.3)): peel the first blow-up π : X_1 → X with center Z ⊆ S. The tail is a sequence of order ≥ m for (X_1, π_*^{-1}(I, m), E_1) with the hypersurface S_1 = π_*^{-1}S, a smooth hypersurface (isSmoothDivisor_strictTransform_of_le), so the induction hypothesis gives (88.1) for the tail with the ideals D^j π_*^{-1}(I, m). By the one-blow-up case (Hironaka/Resolution/Algebraic/Kol07/Theorem88BlowUp.lean), D^j π_*^{-1}(I, m) = ∑_{l ≤ j} D^{j−l}(−log S_1) π_*^{-1}(D^l I, m − l); the marked transform along the tail of this sum lies in the sum of the marked transforms (markedTransformSeq_iSup_le, the marks being defined by the order bounds), each of which lies in D^{j−l}(−log S_i) Π_*^{-1}(D^l I, m − l) by (87.3) along the sequence (markedTransformSeq_logDerivativeIter_le), and D^{s−j}(−log S_i) D^{j−l}(−log S_i) = D^{s−l}(−log S_i) (the composition rule); D(−log S_i) of a sum lies in the sum (logDerivativeIter_iSup_le). The reverse inclusion is Theorem 76 for the first blow-up and monotonicity. Stage 0 and the empty sequence are (88.1) on X itself: the j = s summand is D^s I, the others lie in it.

theorem Ideal.logDerivative_iSup_le {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] {ι : Sort u_3} (J : Ideal A) (K : ι → Ideal A) : logDerivative k J (⨆ (i : ι), K i) ≤ ⨆ (i : ι), logDerivative k J (K i)

D(−log J) of a sum lies in the sum of the D(−log J)s.

theorem Ideal.logDerivativeIter_iSup_le {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] {ι : Sort u_3} (J : Ideal A) (t : ℕ) (K : ι → Ideal A) : logDerivativeIter k J t (⨆ (i : ι), K i) ≤ ⨆ (i : ι), logDerivativeIter k J t (K i)

D^t(−log J) of a sum lies in the sum of the D^t(−log J)s.

theorem Hironaka.Sequence.logDerivativeIter_iSup_le {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.LocallyOfFiniteType f] (S : X.IdealSheafData) {ι : Sort u_1} (t : ℕ) (K : ι → X.IdealSheafData) : AlgebraicGeometry.Scheme.IdealSheafData.logDerivativeIter f S t (⨆ (i : ι), K i) ≤ ⨆ (i : ι), AlgebraicGeometry.Scheme.IdealSheafData.logDerivativeIter f S t (K i)

D^t(−log S) of a sum of ideal sheaves lies in the sum (checked on stalks).

theorem Hironaka.Sequence.markedTransformSeq_iSup_le {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (B : X.BlowUpSequence) (h : B.IsSmooth f) (K : ℕ → X.IdealSheafData) (s c : ℕ) (hK : ∀ j ≤ s, ∀ (i : Fin B.length), (B.markedTransformSeq (K j) c i.castSucc).LeOrdAlong (B.center i).support ↑c) (i : Fin (B.length + 1)) : B.markedTransformSeq (⨆ (j : ℕ), ⨆ (_ : j ≤ s), K j) c i ≤ ⨆ (j : ℕ), ⨆ (_ : j ≤ s), B.markedTransformSeq (K j) c i

The marked transform of a sum along a sequence lies in the sum of the marked transforms when every summand has order ≥ c along every center (so that the marked transforms are defined in the sense of [Kol07, Definition 60]); markedTransform_iSup_le at every stage.

theorem Hironaka.Sequence.IsOrderGeSeq.of_le {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) (B : X.BlowUpSequence) {I J : X.IdealSheafData} {m : ℕ} {E : X.DivisorFamily} (h : B.IsOrderGeSeq f I m E) (hJ : J ≤ I) : B.IsOrderGeSeq f J m E

IsOrderGeSeq is antitone in the ideal (the order is antitone, the marked transform monotone).

theorem Hironaka.Sequence.derivativeIter_eq_iSup_logDerivativeIter {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) (S I : X.IdealSheafData) (s : ℕ) : AlgebraicGeometry.Scheme.IdealSheafData.derivativeIter f s I = ⨆ (j : ℕ), ⨆ (_ : j ≤ s), AlgebraicGeometry.Scheme.IdealSheafData.logDerivativeIter f S (s - j) (AlgebraicGeometry.Scheme.IdealSheafData.derivativeIter f j I)

(88.1) on X itself (the empty sequence, or stage 0): the j = s summand is D^s I and the others lie in it (logDerivativeIter_le_derivativeIter and [Kol07, Lemma 74 (1)]).

theorem Hironaka.Sequence.derivativeIter_markedTransformSeq_eq_iSup {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (B : X.BlowUpSequence) (S I : X.IdealSheafData) (E : X.DivisorFamily) (m : ℕ) (hS : AlgebraicGeometry.IsSmoothDivisor S) (h : B.IsOrderGeSeq f I m E) (hZS : ∀ (i : Fin B.length), B.strictTransformSeq S i.castSucc ≤ B.center i) {s : ℕ} (hs : s ≤ m) (i : Fin (B.length + 1)) : AlgebraicGeometry.Scheme.IdealSheafData.derivativeIter (CategoryTheory.CategoryStruct.comp (B.stageMap i) f) s (B.markedTransformSeq I m i) = ⨆ (j : ℕ), ⨆ (_ : j ≤ s), AlgebraicGeometry.Scheme.IdealSheafData.logDerivativeIter (CategoryTheory.CategoryStruct.comp (B.stageMap i) f) (B.strictTransformSeq S i) (s - j) (B.markedTransformSeq (AlgebraicGeometry.Scheme.IdealSheafData.derivativeIter f j I) (m - j) i)

[Kol07, Theorem 88]: (88.1) at every stage of a smooth blow-up sequence of order ≥ m whose centers lie in the strict transforms of the smooth hypersurface S.