The centres of an order reduction lie over the cosupport

For a marked ideal (I, m) and a blow-up sequence of order ≥ m for it, the centre Z_i of the i-th blow-up satisfies ord_{Z_i} I_i ≥ m, where I_i is the marked transform of I at stage i [Kol07, Definition 60; Theorem 69]. Since the marked transform contains the pullback Π_i^* I (it is the colon ideal Π_i^* I : F^m by the exceptional divisor F), V(I_i) ⊆ Π_i^{-1}(V(I)); hence for m ≥ 1 every centre lies over V(I) = cosupp I. This is the observation "by (21.2), π_0 ⋯ π_{j−1}(Z_j) ⊂ X̄" in the proof of [Kol07, Corollary 22], on which the identification of the end result of the truncated sequence with an open subscheme of the last centre rests.

• comap_stageMap_le_markedTransformSeq: Π_i^* I ≤ I_i along any blow-up sequence.
• stageMap_mem_support_of_mem_center: for a blow-up sequence of order ≥ m with m ≥ 1, the centres lie over V(I).
• stageMap_mem_support_of_mem_center_BP: the same for the principalization sequence BP(A, I, ∅): with an empty boundary it is the order reduction BMO_1(A, I, 1, ∅) (BP_of_isEmpty), a sequence of order ≥ 1 by the defining property of the functor.

The lemmas are used to place the centres of Kollár's resolution over the singular locus and, in the form stageMap_mem_support_of_mem_center_BP, to identify the first centre containing the strict transform of the embedded scheme (Hironaka.Resolution.Algebraic.Kol07.Thm36.AffineTheorem36).

theorem Hironaka.Resolution.comap_stageMap_le_markedTransformSeq_mk {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (I : X.IdealSheafData) (m j : ℕ) (hj : j < S.length + 1) : I.comap (S.stageMap ⟨j, hj⟩) ≤ S.markedTransformSeq I m ⟨j, hj⟩

The pullback Π_j^* I is contained in the marked transform I_j of (I, m) along a sequence, in the ⟨j, hj⟩ form of the indices: the colon ideal contains the ideal at every step.

theorem Hironaka.Resolution.comap_stageMap_le_markedTransformSeq {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (I : X.IdealSheafData) (m : ℕ) (i : Fin (S.length + 1)) : I.comap (S.stageMap i) ≤ S.markedTransformSeq I m i

The pullback Π_i^* I is contained in the marked transform I_i of (I, m) at stage i of a blow-up sequence [Kol07, Definition 60]: the marked transform is a colon ideal of the pullback.

theorem Hironaka.Resolution.stageMap_mem_support_of_mem_center {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] {S : X.BlowUpSequence} {I : X.IdealSheafData} {E : X.DivisorFamily} {m : ℕ} (hS : S.IsOrderGeSeq f I m E) (hm : 1 ≤ m) (i : Fin S.length) {z : ↥(S.stage i.castSucc)} (hz : z ∈ (S.center i).support) : (S.stageMap i.castSucc) z ∈ I.support

In a blow-up sequence of order ≥ m for (I, m) with m ≥ 1 on an ambient X smooth over k (the standing hypothesis under which the order is defined), every centre lies over V(I) [Kol07, Definition 60; Theorem 69]: the order of the marked transform I_i is ≥ m ≥ 1 at every point of the centre Z_i (semicontinuity), so Z_i ⊆ V(I_i) ⊆ V(Π_i^* I) = Π_i^{-1}(V(I)).

theorem Hironaka.Resolution.stageMap_mem_support_of_mem_center_BP {k : Type u} [Field k] [CharZero k] (TA : AlgebraicGeometry.Triple k) (hE : IsEmpty TA.E.ι) (i : Fin (Sequence.BP TA).length) {z : ↥((Sequence.BP TA).stage i.castSucc)} (hz : z ∈ ((Sequence.BP TA).center i).support) : ((Sequence.BP TA).stageMap i.castSucc) z ∈ TA.I.support

The centres of the principalization sequence BP(A, I, ∅) lie over V(I) ("by (21.2), π_0 ⋯ π_{j−1}(Z_j) ⊂ X̄" in the proof of [Kol07, Corollary 22]): with an empty boundary BP is the order reduction BMO_1(A, I, 1, ∅) (BP_of_isEmpty), of order ≥ 1 for (I, 1).