The composite of two blow-ups is one blow-up

With b : X' ⟶ X the blow-up along I, E its exceptional ideal, J' an ideal sheaf on X' and K_m = descendCenter I J' m Hironaka's J(m) with K_m.comap b = J' · E^m (Hironaka.Scheme.BlowUp.Composite.Main), the chain of canonical isomorphisms over X

B_{J'} X' ≅ B_{J' E^m} X' = B_{K_m 𝒪_{X'}} X' ≅ B_{I K_m} X

gives Hironaka's unique isomorphism h : X' → X₂ with f' = f₀ ∘ f₁ ∘ h between the composite of the two monoidal transformations and the monoidal transformation with centre J(m) J₀ [Hir64, Ch. 0, §3, p. 133]; [TSPA, Tag 080B]. The first step is the blow-up of a product with an invertible factor (blowUp.exists_mul_isInvertible_iso, read backwards), the second the equality of centres, the third the blow-up of a product centre (blowUp.exists_mulIso). Isomorphisms over X compose, and a canonical one stays canonical (exists_unique_iso_over_of_iso). blowUp.exists_comp_iso chooses m = m₀ and adds the support |V(K)| = |Z| ∪ b(|Z'|). The result is used for the composite of a blow-up sequence (Hironaka.Scheme.BlowUpSequence.CompositeBlowUp).

theorem AlgebraicGeometry.exists_unique_iso_over_of_iso {A B C X : Scheme} {f : A ⟶ X} {g : B ⟶ X} {h : C ⟶ X} (e₁ : A ≅ B) (he₁ : CategoryTheory.CategoryStruct.comp e₁.hom g = f) (h₂ : ∃ (e : B ≅ C), CategoryTheory.CategoryStruct.comp e.hom h = g ∧ ∀ (ψ : B ⟶ C), CategoryTheory.CategoryStruct.comp ψ h = g → ψ = e.hom) : ∃ (e : A ≅ C), CategoryTheory.CategoryStruct.comp e.hom h = f ∧ ∀ (ψ : A ⟶ C), CategoryTheory.CategoryStruct.comp ψ h = f → ψ = e.hom

Composing an isomorphism e₁ : A ≅ B over X with a canonical isomorphism B ≅ C over X gives a canonical isomorphism A ≅ C over X: a morphism ψ : A ⟶ C over X gives the morphism e₁.inv ≫ ψ : B ⟶ C over X, which is the canonical one.

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.exists_iso_of_eq {X : Scheme} {L L' : X.IdealSheafData} (h : L = L') : ∃ (e : L.blowUp ≅ L'.blowUp), CategoryTheory.CategoryStruct.comp e.hom L'.blowUpπ = L.blowUpπ

Equal centers have the same blow-up, over X.

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.exists_iso_mul_isInvertible {X : Scheme} (J L : X.IdealSheafData) (hL : L.IsInvertible) : ∃ (e : J.blowUp ≅ (J * L).blowUp), CategoryTheory.CategoryStruct.comp e.hom (J * L).blowUpπ = J.blowUpπ ∧ ∀ (ψ : J.blowUp ⟶ (J * L).blowUp), CategoryTheory.CategoryStruct.comp ψ (J * L).blowUpπ = J.blowUpπ → ψ = e.hom

The trivial factor read from blowUp J ([TSPA, Tag 080B]: a power of the exceptional ideal cuts out an effective Cartier divisor, whose blow-up is trivial): for L invertible, blowUp J ≅ blowUp (J * L) over X, uniquely — the inverse of blowUp.exists_mul_isInvertible_iso; uniqueness from the universal property of blowUp (J * L), the pullback (J * L).comap (π J) = E_J · L.comap (π J) being invertible.

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.exists_iso_of_comap_descendCenter_eq {X : Scheme} (I : X.IdealSheafData) (J' : I.blowUp.IdealSheafData) (m : ℕ) (hm : (descendCenter I J' m).comap I.blowUpπ = J' * I.exceptionalDivisor ^ m) : ∃ (e : J'.blowUp ≅ (I * descendCenter I J' m).blowUp), CategoryTheory.CategoryStruct.comp e.hom (I * descendCenter I J' m).blowUpπ = CategoryTheory.CategoryStruct.comp J'.blowUpπ I.blowUpπ ∧ ∀ (ψ : J'.blowUp ⟶ (I * descendCenter I J' m).blowUp), CategoryTheory.CategoryStruct.comp ψ (I * descendCenter I J' m).blowUpπ = CategoryTheory.CategoryStruct.comp J'.blowUpπ I.blowUpπ → ψ = e.hom

The chain B_{IK_m}X ≅ B_{K_m𝒪_{X'}}X' = B_{J'𝓘_F^m}X' ≅ B_{J'}X' = X'' over X [Hir64, Ch. 0, §3, p. 133]; [TSPA, Tag 080B]: if K_m.comap b = J' · E^m, then blowUp J' ≅ blowUp (I * K_m) over X, by a unique isomorphism over X.

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.exists_comp_iso {X : Scheme} (I : X.IdealSheafData) (J' : I.blowUp.IdealSheafData) [IsNoetherian X] : ∃ (K : X.IdealSheafData), ↑K.support = ↑I.support ∪ ⇑I.blowUpπ '' ↑J'.support ∧ ∃ (e : J'.blowUp ≅ K.blowUp), CategoryTheory.CategoryStruct.comp e.hom K.blowUpπ = CategoryTheory.CategoryStruct.comp J'.blowUpπ I.blowUpπ ∧ ∀ (ψ : J'.blowUp ⟶ K.blowUp), CategoryTheory.CategoryStruct.comp ψ K.blowUpπ = CategoryTheory.CategoryStruct.comp J'.blowUpπ I.blowUpπ → ψ = e.hom

A composite of two blow-ups is a blow-up [Hir64, Ch. 0, §3, pp. 132–133]; [TSPA, Tag 080B]: for X Noetherian there is an ideal sheaf K on X, with |V(K)| = |Z| ∪ b(|Z'|) set-theoretically, such that the composite X'' → X' → X is the blow-up of X along K: blowUp J' ≅ blowUp K over X, by a unique isomorphism over X; K = I * K_{m₀} for the exponent m₀ of exists_comap_descendCenter_eq.