The cosupport under a blow-up whose center lies in it

The boundary-clearing step of the proof of Theorem 103 [Kol07, 104, Step 2.1] keeps the birational transforms of the already cleared members E^i (i < j) disjoint from the cosupport while BD_{n,m,j} blows up centers inside cosupp(I, m). The fact behind it: under one blow-up with center Z ⊆ cosupp(I, m), a point of cosupp(π_*^{-1} I, m) maps to a point of cosupp(I, m). Over Z this holds because Z ⊆ cosupp(I, m); off the exceptional divisor because the weak transform is the pull-back there (the exceptional factor is the unit ideal, stalkIdeal_weakTransform_of_notMem), π is a local isomorphism (isIso_stalkMap_π_of_notMem_support), and the order is a stalk invariant (ord_map_ringEquiv); this is le_ord_of_le_ord_weakTransform. Hence a divisor disjoint from the cosupport has birational transform disjoint from the cosupport of the weak transform (disjoint_cosupp_strictTransform_of_disjoint, with coe_support_strictTransform), and along a smooth blow-up sequence of order m, whose centers lie in the cosupport by condition (4) of [Kol07, Definition 66] and upper semicontinuity (le_ord_of_mem_center), the disjointness persists to the end (disjoint_cosupp_strictTransformSeq_last_of_disjoint).

The weak transform is the birational transform π_*^{-1} I of [Kol07, 58].

theorem Hironaka.Sequence.stalkIdeal_weakTransform_of_notMem {X : AlgebraicGeometry.Scheme} (Z I : X.IdealSheafData) {x' : ↥Z.blowUp} (hx' : x' ∉ Z.exceptionalDivisor.support) : (I.weakTransform Z).stalkIdeal x' = (I.comap Z.blowUpπ).stalkIdeal x'

Off the exceptional divisor the weak transform (the birational transform of [Kol07, 58]) has the stalk of the pull-back: the exceptional factor is the unit ideal there, and a colon by the unit ideal is the ideal itself.

theorem Hironaka.Sequence.ord_weakTransform_of_notMem {X : AlgebraicGeometry.Scheme} (Z I : X.IdealSheafData) {x' : ↥Z.blowUp} (hx' : x' ∉ Z.exceptionalDivisor.support) : (I.weakTransform Z).ord x' = I.ord (Z.blowUpπ x')

Off the exceptional divisor the order of the weak transform is the order of the ideal at the image point (π is a local isomorphism there, and the order is a stalk invariant).

theorem Hironaka.Sequence.le_ord_of_le_ord_weakTransform {X : AlgebraicGeometry.Scheme} (Z I : X.IdealSheafData) {m : ℕ} (hZ : ∀ x ∈ Z.support, ↑m ≤ I.ord x) (x' : ↥Z.blowUp) (h : ↑m ≤ (I.weakTransform Z).ord x') : ↑m ≤ I.ord (Z.blowUpπ x')

If the center Z lies in cosupp(I, m), a point of cosupp(π_*^{-1} I, m) on the blow-up maps to a point of cosupp(I, m).

theorem Hironaka.Sequence.disjoint_cosupp_strictTransform_of_disjoint {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (Z I D : X.IdealSheafData) {m : ℕ} (hZ : ∀ x ∈ Z.support, ↑m ≤ I.ord x) (hD : Disjoint {x : ↥X | ↑m ≤ I.ord x} ↑D.support) : Disjoint {x' : ↥Z.blowUp | ↑m ≤ (I.weakTransform Z).ord x'} ↑(D.strictTransform Z).support

A divisor disjoint from cosupp(I, m) has birational transform disjoint from cosupp(π_*^{-1} I, m) when the center lies in cosupp(I, m).

theorem Hironaka.Sequence.disjoint_cosupp_strictTransformSeq_last_of_disjoint {k : Type u} [Field k] [CharZero k] {m : ℕ} (n : ℕ) {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (S : X.BlowUpSequence) {J : X.IdealSheafData} {E : X.DivisorFamily} : S.IsOrderSeq f J E m → ∀ (D : X.IdealSheafData), Disjoint {x : ↥X | ↑m ≤ J.ord x} ↑D.support → Disjoint {x : ↥(S.stage (Fin.last S.length)) | ↑m ≤ (S.weakTransformSeq J (Fin.last S.length)).ord x} ↑(S.strictTransformSeq D (Fin.last S.length)).support

Along a smooth blow-up sequence of order m, whose centers lie in the cosupport (condition (4) of [Kol07, Definition 66]), a divisor disjoint from cosupp(I, m) keeps its birational transform disjoint from the cosupport of the final ideal; this is what keeps the cleared members cleared in [Kol07, 104, Step 2.1].