Blowing up a product centre is the iterated blow-up

The general theorems of Hironaka.Scheme.BlowUp.ProductCenter, for the blow-up AlgebraicGeometry.Scheme.IdealSheafData.blowUp: for ideal sheaves I, J on X, with b = blowUp.π I : X' ⟶ X and b' = blowUp.π (J.comap b) : X'' ⟶ X',

• blowUp.isInvertible_comap_of_isInvertible: b pulls invertible ideal sheaves back to invertible ones (isInvertible_comap_of_charts at the charts blowUp.chart I U a);
• blowUp.isInvertible_comap_mul_π_comp: b' ≫ b is admissible for I * J;
• blowUp.existsUnique_lift_comp: b' ≫ b is universal for I * J;
• blowUp.exists_mulIso, blowUp.mulIso [TSPA, Tag 080A]: X'' ≅ blowUp (I * J) over X, uniquely;
• blowUp.exists_powIso: blowUp (I ^ m) ≅ blowUp I over X for m ≥ 1 [Hau14, Definition 4.6 and Example 4.52], through blowUp.exists_mulIso I (I ^ (m - 1)) and the trivial blow-up of the invertible (I ^ (m - 1)).comap b (blowUp.isIso_π_of_isInvertible);
• blowUp.isBlowUp_comp: the composite b' ≫ b satisfies the predicate IsBlowUp of Hironaka.Scheme.BlowUp.UniversalProperty, the universal property of [Hau14, Definition 4.4] (as the blow-up does, blowUp.isBlowUp of Hironaka.Scheme.BlowUp.Glue.Global).

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.isInvertible_comap_of_isInvertible {X : Scheme} (I K : X.IdealSheafData) (hK : K.IsInvertible) : (K.comap I.blowUpπ).IsInvertible

The inverse image along IdealSheafData.blowUpπ I of an invertible ideal sheaf is invertible [TSPA, Tags 080A and 0809].

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.isInvertible_comap_π_comp {X : Scheme} (I J : X.IdealSheafData) : (I.comap (CategoryTheory.CategoryStruct.comp (J.comap I.blowUpπ).blowUpπ I.blowUpπ)).IsInvertible

I pulls back along b' ≫ b to an invertible ideal sheaf (I.comap b is the exceptional ideal of b, invertible by blowUp.isInvertible_comap_π).

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.isInvertible_comap_mul_π_comp {X : Scheme} (I J : X.IdealSheafData) : ((I * J).comap (CategoryTheory.CategoryStruct.comp (J.comap I.blowUpπ).blowUpπ I.blowUpπ)).IsInvertible

b' ≫ b is admissible for I * J.

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.existsUnique_lift_comp {X : Scheme} (I J : X.IdealSheafData) {Y : Scheme} (f : Y ⟶ X) (hf : ((I * J).comap f).IsInvertible) : ∃! g : Y ⟶ (J.comap I.blowUpπ).blowUp, CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp (J.comap I.blowUpπ).blowUpπ I.blowUpπ) = f

b' ≫ b is universal for I * J: every morphism along which I * J becomes invertible lifts uniquely through it.

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.isBlowUp_comp {X : Scheme} (I J : X.IdealSheafData) : IsBlowUp (I * J) (CategoryTheory.CategoryStruct.comp (J.comap I.blowUpπ).blowUpπ I.blowUpπ)

The composite b' ≫ b is a blow-up along I * J in the sense of the universal property.

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

The blow-up of X' along J.comap b is isomorphic over X to the blow-up of X along I * J, by a unique isomorphism over X [TSPA, Tag 080A].

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.blowUp.mulIso {X : Scheme} (I J : X.IdealSheafData) : (J.comap I.blowUpπ).blowUp ≅ (I * J).blowUp

The canonical isomorphism blowUp (J.comap b) ≅ blowUp (I * J) over X.

Equations

• AlgebraicGeometry.Scheme.IdealSheafData.blowUp.mulIso I J = ⋯.choose

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.mulIso_hom_π {X : Scheme} (I J : X.IdealSheafData) : CategoryTheory.CategoryStruct.comp (mulIso I J).hom (I * J).blowUpπ = CategoryTheory.CategoryStruct.comp (J.comap I.blowUpπ).blowUpπ I.blowUpπ

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.eq_mulIso_hom {X : Scheme} (I J : X.IdealSheafData) (ψ : (J.comap I.blowUpπ).blowUp ⟶ (I * J).blowUp) (hψ : CategoryTheory.CategoryStruct.comp ψ (I * J).blowUpπ = CategoryTheory.CategoryStruct.comp (J.comap I.blowUpπ).blowUpπ I.blowUpπ) : ψ = (mulIso I J).hom

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.exists_powIso {X : Scheme} (I : X.IdealSheafData) (m : ℕ) (hm : 1 ≤ m) : ∃ (e : (I ^ m).blowUp ≅ I.blowUp), CategoryTheory.CategoryStruct.comp e.hom I.blowUpπ = (I ^ m).blowUpπ ∧ ∀ (ψ : (I ^ m).blowUp ⟶ I.blowUp), CategoryTheory.CategoryStruct.comp ψ I.blowUpπ = (I ^ m).blowUpπ → ψ = e.hom

For m ≥ 1, blowUp (I ^ m) ≅ blowUp I over X, uniquely: the Rees algebras of I and I ^ m have isomorphic Proj [Hau14, Definition 4.6 and Example 4.52]. Write I ^ m = I * I ^ (m - 1); blowUp.exists_mulIso identifies blowUp (I * I ^ (m - 1)) with the blow-up of X' along (I ^ (m - 1)).comap b = (I.comap b) ^ (m - 1), a power of the invertible exceptional ideal, whose blow-up map is an isomorphism (blowUp.isIso_π_of_isInvertible).