The universal property of the blow-up as a predicate

A morphism π : B ⟶ X is a blow-up of X along the ideal sheaf I [Hau14, Definition 4.4] if (i) the inverse image I·𝒪_B = I.comap π of the centre is an effective Cartier divisor — π is admissible for I — and (ii) π is universal for this property: every admissible f : Y ⟶ X (every f with I.comap f invertible) factors through π by a unique g : Y ⟶ B. Equivalently, the blow-up is a final object of the category of X-schemes on which the inverse image of the centre is an effective Cartier divisor [TSPA, Tag 0806].

IsBlowUp I π records exactly these two clauses. Every theorem of the blow-up calculus that the sources derive "from the universal property" — the trivial blow-up, flat base change, the product formula and the composite of blow-ups — is proved once for an arbitrary π with IsBlowUp I π (HironakaExamples.BlowUp.TrivialBlowUp, Hironaka.Scheme.BlowUp.FlatBaseChange, Hironaka.Scheme.BlowUp.ProductCenter) and instantiated at the blow-up through blowUp.isBlowUp (Hironaka.Scheme.BlowUp.Glue.Global). The predicate is Prop-valued (no data).

structure AlgebraicGeometry.IsBlowUp {X B : Scheme} (I : X.IdealSheafData) (π : B ⟶ X) : Prop

π : B ⟶ X is a blow-up of X along I [Hau14, Definition 4.4]; [TSPA, Tag 0806] if π is admissible for I (the inverse image ideal I.comap π is invertible) and every admissible f : Y ⟶ X factors uniquely through π.

• admissible : (I.comap π).IsInvertible

  Clause (i): the inverse image of the centre is an effective Cartier divisor.

• existsUnique_lift {Y : Scheme} (f : Y ⟶ X) : (I.comap f).IsInvertible → ∃! g : Y ⟶ B, CategoryTheory.CategoryStruct.comp g π = f

  Clause (ii): unique factorization of every admissible morphism.

theorem AlgebraicGeometry.IsBlowUp.exists_lift {X B : Scheme} {I : X.IdealSheafData} {π : B ⟶ X} (h : IsBlowUp I π) {Y : Scheme} (f : Y ⟶ X) (hf : (I.comap f).IsInvertible) : ∃ (g : Y ⟶ B), CategoryTheory.CategoryStruct.comp g π = f

Existence half of the universal property.

theorem AlgebraicGeometry.IsBlowUp.hom_ext {X B : Scheme} {I : X.IdealSheafData} {π : B ⟶ X} (h : IsBlowUp I π) {Y : Scheme} (f : Y ⟶ X) (hf : (I.comap f).IsInvertible) (g g' : Y ⟶ B) (e : CategoryTheory.CategoryStruct.comp g π = f) (e' : CategoryTheory.CategoryStruct.comp g' π = f) : g = g'

Uniqueness half of the universal property: two lifts of an admissible morphism coincide.

theorem AlgebraicGeometry.IsBlowUp.comap_comp_isInvertible_iff {X B : Scheme} {π : B ⟶ X} {Z : Scheme} (g : X ⟶ Z) (J : Z.IdealSheafData) : (J.comap (CategoryTheory.CategoryStruct.comp π g)).IsInvertible ↔ ((J.comap g).comap π).IsInvertible

Admissibility of π composed with any morphism into X for which I pulls back to an invertible ideal sheaf on the blow-up: I.comap (π ≫ g) = (I.comap g).comap π.