Trivial blow-ups, the isomorphism off the centre, degenerate centres, isomorphisms of the base

Consequences of the universal property of the blow-up (blowUp.lift, blowUp.hom_ext) and of the affine degenerate case (affineBlowUp.isEmpty_bot):

• Trivial blow-ups [Kol07, Warning 20]: if the centre is a Cartier divisor (I invertible) the blow-up map is an isomorphism — 𝟙 X is admissible and lifts, and the two composites are identities by uniqueness — and then the exceptional divisor is the centre ((I.comap π).map π = I). In particular the empty blow-up (I = ⊤) is an isomorphism [TSPA, Tag 02OS].
• The blow-up map is an isomorphism over the complement W of the centre [TSPA, Tag 02OS]: I·𝒪_W = 𝒪_W (the support of I.comap W.ι is empty), so W → X is admissible, lifts into π⁻¹(W), and the two composites with π ∣_ W are identities by uniqueness. Hence every point off the centre has a preimage in the blow-up.
• The blow-up along the zero ideal sheaf (the centre is all of X) is empty [Hau14, Definition 6.2]: every point lies in some π⁻¹(U) ≅ affineBlowUp (I.ideal U), which is empty by affineBlowUp.isEmpty_bot.
• An isomorphism e : X ≅ Y with I = J.comap e.hom induces a canonical isomorphism of blow-ups over e [Hau14, Corollary 5.2 (d)], the lift of π ≫ e.hom, unique among the morphisms over e.

theorem AlgebraicGeometry.Scheme.IdealSheafData.map_comap_of_isIso {Y Z : Scheme} (J : Z.IdealSheafData) (e : Y ⟶ Z) [CategoryTheory.IsIso e] : (J.comap e).map e = J

For an isomorphism e, map · e inverts comap · e.

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.isIso_π_of_isInvertible {X : Scheme} (I : X.IdealSheafData) (h : I.IsInvertible) : CategoryTheory.IsIso I.blowUpπ

For a trivial blow-up — the centre a Cartier divisor, I invertible — the blow-up map is an isomorphism, its inverse being the lift of 𝟙 X [Kol07, Warning 20].

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.map_exceptionalDivisor_of_isInvertible {X : Scheme} (I : X.IdealSheafData) (h : I.IsInvertible) : I.exceptionalDivisor.map I.blowUpπ = I

For a trivial blow-up the exceptional divisor is the centre [Kol07, Warning 20 (2)]: the scheme-theoretic image of I·𝒪_B under the isomorphism π is I.

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.isIso_π_top {X : Scheme} : CategoryTheory.IsIso ⊤.blowUpπ

The empty blow-up [Kol07, Warning 20]; [TSPA, Tag 02OS]: the blow-up along the unit ideal sheaf is an isomorphism.

theorem AlgebraicGeometry.comap_ι_compl_support_eq_top {X : Scheme} (I : X.IdealSheafData) : I.comap (Scheme.Opens.ι I.support.compl) = ⊤

The inverse image of I on the complement W of its support is the unit ideal sheaf.

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.isIso_π_restrict_compl_support {X : Scheme} (I : X.IdealSheafData) : CategoryTheory.IsIso (I.blowUpπ ∣_ I.support.compl)

The blow-up is an isomorphism off the centre [TSPA, Tag 02OS]: over W = X ∖ Z the inverse image of I is the unit ideal sheaf, so W → X is admissible and its lift into π⁻¹(W) inverts π ∣_ W.

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.isEmpty_of_forall {X : Scheme} (I : X.IdealSheafData) (h : ∀ (U : ↑X.affineOpens), IsEmpty ↥(affineBlowUp (I.ideal U))) : IsEmpty ↥I.blowUp

If every affine piece is empty, so is the blow-up.

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.isEmpty_bot {X : Scheme} : IsEmpty ↥⊥.blowUp

The blow-up along the zero ideal sheaf — the centre is all of X — is empty [Hau14, Definition 6.2].

theorem AlgebraicGeometry.exists_π_eq_of_notMem_support {X : Scheme} (Z : X.IdealSheafData) {x : ↥X} (hx : x ∉ Z.support) : ∃ (x' : ↥Z.blowUp), Z.blowUpπ x' = x

A point off the centre has a preimage in the blow-up: the blow-up is an isomorphism over the complement of the centre.

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

An isomorphism e : X ≅ Y carrying I to J (I = J.comap e.hom) induces a canonical isomorphism of the blow-ups over e — the lift of π ≫ e.hom, the only morphism over e [Hau14, Corollary 5.2 (d)].