A finite succession of monoidal transformations is one blow-up

A morphism obtained by a finite succession of monoidal transformations "can be also obtained by a single monoidal transformation with suitably chosen center" (the remark following Main Theorem I in [Hir64, pp. 132–133]; the induction step is Hironaka's J(m) device, the composition of two blow-ups as one blow-up, [TSPA, Tag 080B]): for X Noetherian and S : BlowUpSequence X, there is an ideal sheaf K on X whose support is the union of the images of the centers under the partial composites and a canonical isomorphism S.last ≅ K.blowUp over X.

The empty sequence gives K = ⊤ (the trivial blow-up, blowUp.isIso_π_of_isInvertible); the inductive step is blowUp.exists_comp_iso applied to the first center and the center of the induction hypothesis on the blown-up scheme, the support union splitting off the index 0. Main Theorem I takes the composite of the resolution sequence as a single blow-up K.blowUp and then enlarges its centre (Hironaka/Resolution/Algebraic/Hir64/MainTheoremI.lean).

theorem AlgebraicGeometry.iUnion_fin_succ_eq {α : Type u_1} {n : ℕ} (F : Fin (n + 1) → Set α) : ⋃ (i : Fin (n + 1)), F i = F 0 ∪ ⋃ (j : Fin n), F j.succ

A union over Fin (n + 1) splits off the index 0.

theorem AlgebraicGeometry.exists_blowUp_composite_iso_nil (X : Scheme) : ∃ (K : X.IdealSheafData), ↑K.support = ⋃ (i : Fin (Scheme.BlowUpSequence.nil X).length), ⇑((Scheme.BlowUpSequence.nil X).stageMap i.castSucc) '' ↑((Scheme.BlowUpSequence.nil X).center i).support ∧ ∃ (e : (Scheme.BlowUpSequence.nil X).last ≅ K.blowUp), CategoryTheory.CategoryStruct.comp e.hom K.blowUpπ = (Scheme.BlowUpSequence.nil X).composite ∧ ∀ (ψ : (Scheme.BlowUpSequence.nil X).last ⟶ K.blowUp), CategoryTheory.CategoryStruct.comp ψ K.blowUpπ = (Scheme.BlowUpSequence.nil X).composite → ψ = e.hom

The empty sequence is one blow-up: K = ⊤, blowUp X ⊤ ≅ X.

theorem AlgebraicGeometry.exists_blowUp_composite_iso_cons (X : Scheme) [IsNoetherian X] (D : X.IdealSheafData) (rest : D.blowUp.BlowUpSequence) (K' : D.blowUp.IdealSheafData) (hK' : ↑K'.support = ⋃ (i : Fin rest.length), ⇑(rest.stageMap i.castSucc) '' ↑(rest.center i).support) (e' : rest.last ≅ K'.blowUp) (he' : CategoryTheory.CategoryStruct.comp e'.hom K'.blowUpπ = rest.composite) : ∃ (K : X.IdealSheafData), ↑K.support = ⋃ (i : Fin (Scheme.BlowUpSequence.cons X D rest).length), ⇑((Scheme.BlowUpSequence.cons X D rest).stageMap i.castSucc) '' ↑((Scheme.BlowUpSequence.cons X D rest).center i).support ∧ ∃ (e : (Scheme.BlowUpSequence.cons X D rest).last ≅ K.blowUp), CategoryTheory.CategoryStruct.comp e.hom K.blowUpπ = (Scheme.BlowUpSequence.cons X D rest).composite ∧ ∀ (ψ : (Scheme.BlowUpSequence.cons X D rest).last ⟶ K.blowUp), CategoryTheory.CategoryStruct.comp ψ K.blowUpπ = (Scheme.BlowUpSequence.cons X D rest).composite → ψ = e.hom

The inductive step: the composition of two blow-ups as one blow-up (blowUp.exists_comp_iso, [TSPA, Tag 080B]) applied to D and the center K' of the induction hypothesis on D.blowUp; the support union splits off the index 0 (|V(D)|, under 𝟙 X) and shifts the other indices along π_D.

theorem AlgebraicGeometry.exists_blowUp_composite_iso' {X : Scheme} (S : X.BlowUpSequence) [IsNoetherian X] : ∃ (K : X.IdealSheafData), ↑K.support = ⋃ (i : Fin S.length), ⇑(S.stageMap i.castSucc) '' ↑(S.center i).support ∧ ∃ (e : S.last ≅ K.blowUp), CategoryTheory.CategoryStruct.comp e.hom K.blowUpπ = S.composite ∧ ∀ (ψ : S.last ⟶ K.blowUp), CategoryTheory.CategoryStruct.comp ψ K.blowUpπ = S.composite → ψ = e.hom

exists_blowUp_composite_iso by induction on the sequence, the Noetherian hypothesis carried along the stages (blowUp.isNoetherian).

theorem AlgebraicGeometry.exists_blowUp_composite_iso {X : Scheme} [IsNoetherian X] (S : X.BlowUpSequence) : ∃ (K : X.IdealSheafData), ↑K.support = ⋃ (i : Fin S.length), ⇑(S.stageMap i.castSucc) '' ↑(S.center i).support ∧ ∃ (e : S.last ≅ K.blowUp), CategoryTheory.CategoryStruct.comp e.hom K.blowUpπ = S.composite ∧ ∀ (ψ : S.last ⟶ K.blowUp), CategoryTheory.CategoryStruct.comp ψ K.blowUpπ = S.composite → ψ = e.hom

A finite succession of monoidal transformations of a Noetherian scheme is one blow-up, with center supported in the union of the images of the centers (the remark following Main Theorem I in [Hir64, pp. 132–133]).