Blow-up sequences all of whose centers are empty

A blow-up sequence all of whose centers are the unit ideal, every blow-up being the trivial one, an isomorphism [Kol07, Warning 20], erases to the empty sequence under the empty blow-up convention [Kol07, 32] (eraseEmpty_eq_nil); its composite is an isomorphism (isIso_stageMap_of_center_eq_top); the weak transform at its end is the inverse image of the starting ideal along the composite (the exceptional factor is the unit ideal at each stage, weakTransform_top_left); and the boundary at its end is the inverse image of the starting boundary with the (unit) exceptional members appended, a deletion of ⊤ members (IsTopErasure, Hironaka/Resolution/Algebraic/Kol07/EraseEmptyEmbedding.lean), assembled stage by stage from isTopErasure_inlEmb_top. These are the four facts needed about a round of the order reduction functor whose pull-back along a smooth morphism has no point of order ≥ d and is therefore skipped (the second clause of functoriality for smooth morphisms, [Kol07, 34.1]).

theorem Hironaka.Sequence.weakTransformSeq_last_eq_comap_composite_of_center_eq_top {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (I : X.IdealSheafData) (hc : ∀ (i : Fin S.length), S.center i = ⊤) : S.weakTransformSeq I (Fin.last S.length) = I.comap S.composite

When every center is the unit ideal, the weak transform at the end is the inverse image of the starting ideal along the composite: at each stage the exceptional factor is the unit ideal (weakTransform_top_left; [Kol07, Warning 20] along a sequence).

theorem Hironaka.Sequence.exists_isTopErasure_totalTransformSeq_of_center_eq_top {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (E : X.DivisorFamily) (hc : ∀ (i : Fin S.length), S.center i = ⊤) : ∃ (e : (E.comap S.composite).ι ↪o (S.totalTransformSeq E (Fin.last S.length)).ι), IsTopErasure (E.comap S.composite) (S.totalTransformSeq E (Fin.last S.length)) e

When every center is the unit ideal, the boundary at the end of the sequence is the inverse image of the starting boundary along the composite with unit members appended (IsTopErasure): stage by stage, the total transform under the trivial blow-up is the inverse image of the family extended by the (unit) exceptional member (isTopErasure_inlEmb_top; [Kol07, 32]).

theorem Hironaka.Sequence.isIso_composite_of_center_eq_top {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (hc : ∀ (i : Fin S.length), S.center i = ⊤) : CategoryTheory.IsIso S.composite

When every center is the unit ideal, the composite of the sequence is an isomorphism [Kol07, Warning 20].