The first-centre index across the deletion of empty blow-ups

Kollár's functoriality under smooth morphisms compares a blow-up sequence with a pullback from which the empty blow-ups have been deleted [Kol07, 34.1; item 32]. The affine resolution (Hironaka.Resolution.Algebraic.Kol07.Thm36.BR) truncates the principalization run at a first-centre index, so the index has to be read through the deletion. eraseIdx S m (Hironaka.Resolution.Algebraic.Kol07.Thm36.EraseEmptyIndex) is the position in S.eraseEmpty of the m-th stage of S; for an integral closed subscheme V(J) the absorbing stage, the first centre containing the strict transform of V(J), has a nonempty centre (center_firstCenterIndex_ne_top: the strict transform of an integral subscheme keeps a generic point up to that stage), so the predicate CenterContains transports through centerContains_eraseEmpty_iff:

• firstCenterIndex_eraseEmpty: the equality firstCenterIndex S.eraseEmpty J = eraseIdx S (firstCenterIndex S J); no deleted (empty) centre before the absorbing stage contains the transform, and the absorbing centre survives the deletion; when no centre ever contains the transform both indices are the lengths;
• take_eraseEmpty_firstCenterIndex: the truncations at the first containing index correspond under the deletion (eraseEmpty_take).

Stated for any blow-up sequence on a locally Noetherian scheme; used by Hironaka.Resolution.Algebraic.Kol07.Thm36.BRAffinePullback.

theorem Hironaka.Resolution.eraseIdx_length {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) : eraseIdx S S.length = S.eraseEmpty.length

The index of the length is the length of the erased sequence: every kept stage advances the index by one.

theorem Hironaka.Resolution.strictTransformSeq_ne_top_of_le_firstCenterIndex {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (S : X.BlowUpSequence) (J : X.IdealSheafData) [AlgebraicGeometry.IsIntegral J.subscheme] (i : Fin (S.length + 1)) (hi : ↑i ≤ firstCenterIndex S J) : S.strictTransformSeq J i ≠ ⊤

Up to the first containing index the strict transform of an integral V(J) is nonempty: it keeps a generic point (exists_isGenericPoint_strictTransformSeq_of_le_firstCenterIndex).

theorem Hironaka.Resolution.center_firstCenterIndex_ne_top {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (S : X.BlowUpSequence) (J : X.IdealSheafData) [AlgebraicGeometry.IsIntegral J.subscheme] (h : ∃ (n : ℕ), CenterContains S J n) : S.center ⟨firstCenterIndex S J, ⋯⟩ ≠ ⊤

The first containing centre of an integral V(J) is a nonempty centre: an empty centre ⊤ containing the strict transform would force the strict transform to be ⊤.

theorem Hironaka.Resolution.firstCenterIndex_eraseEmpty {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (S : X.BlowUpSequence) (J : X.IdealSheafData) [AlgebraicGeometry.IsIntegral J.subscheme] : firstCenterIndex S.eraseEmpty J = eraseIdx S (firstCenterIndex S J)

For an integral V(J), the first containing index of the sequence with its empty blow-ups deleted is the image under eraseIdx S of the first containing index of S Kol07, 34.1; item 32: before the absorbing stage no deleted (empty) centre contains the transform, and the absorbing centre is nonempty; when no centre ever contains the transform, both indices are the lengths.

theorem Hironaka.Resolution.take_eraseEmpty_firstCenterIndex {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (S : X.BlowUpSequence) (J : X.IdealSheafData) [AlgebraicGeometry.IsIntegral J.subscheme] : S.eraseEmpty.take (firstCenterIndex S.eraseEmpty J) = (S.take (firstCenterIndex S J)).eraseEmpty

The truncations at the first containing index correspond under the deletion of empty blow-ups (eraseEmpty_take).