The blow-up of a scheme along an ideal sheaf

The blow-up blowUp I of a scheme X along an ideal sheaf I is Proj_X (⨁ Iⁿ) [TSPA, Tag 01OF], built by the relative gluing lemma [TSPA, Tag 01LH] from the affine blow-ups Proj Rees(I(U)) over the affine opens U of X (blowUpOf). The gluing hypothesis — that the naturality squares of affineBlowUpNatTrans I are pullbacks — is the open-restriction square of the universal property of the affine blow-up (affineBlowUp.isPullback_mapHom), pasted with the isomorphisms Spec Γ(X, U) ≅ U (affineBlowUpNatTrans_equifibered). It is Hauser's blow-up [Hau14, Definitions 4.4 and 4.7], Kollár's B_Z X [Kol07, Notation 19] and Hironaka's monoidal transformation of X with centre the closed subscheme defined by I [Hir64, Ch. 0, §2], with its blow-up map IdealSheafData.blowUpπ I : blowUp I ⟶ X and its exceptional divisor IdealSheafData.exceptionalDivisor I, the inverse image ideal sheaf of the centre Z = V(I), whose closed subscheme is π⁻¹(Z).

theorem AlgebraicGeometry.affineBlowUpNatTrans_equifibered {X : Scheme} (I : X.IdealSheafData) : CategoryTheory.NatTrans.Equifibered (affineBlowUpNatTrans I)

The naturality squares of the affine blow-ups over the affine opens are pullbacks — the open-restriction square affineBlowUp.isPullback_mapHom pasted with the isomorphisms Spec Γ(X, U) ≅ U.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.blowUp {X : Scheme} (I : X.IdealSheafData) : Scheme

The blow-up of X along I [TSPA, Tag 01OF]; [Hau14, Definition 4.4]; [Kol07, Notation 19]: glued from the affine blow-ups Proj Rees(I(U)) over the affine opens U of X.

Relation to the source.

• Translation. D.blowUp is Hironaka's monoidal transformation of $X$ with centre $D$ [Hir64, Ch. 0, §2], and D.blowUpπ its projection $f$; "blow-up" and "monoidal transformation" are used interchangeably. The centre is any closed subscheme, not necessarily non-singular or nonempty: the main theorems state the conditions on their centres as clauses.

Equations

• I.blowUp = AlgebraicGeometry.blowUpOf I ⋯

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.blowUpπ {X : Scheme} (I : X.IdealSheafData) : I.blowUp ⟶ X

The blow-up map π : blowUp I ⟶ X.

Equations

• I.blowUpπ = AlgebraicGeometry.blowUpOf.π I ⋯

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.exceptionalDivisor {X : Scheme} (D : X.IdealSheafData) : D.blowUp.IdealSheafData

The ideal sheaf of the exceptional divisor f⁻¹(D): the inverse image ideal sheaf of the centre under the projection [Hir64, Ch. 0, §5, p. 142]; [Kol07, Notation 19].

Equations

• D.exceptionalDivisor = D.comap D.blowUpπ