The blow-up commutes with restriction to opens

For a morphism h : Y ⟶ X, the universal property lifts π_Y ≫ h to the morphism of blow-ups blowUpMap h D : blowUp (D.comap h) ⟶ blowUp D over h. For an open immersion it is the restriction to π⁻¹(U):

Blowing up commutes with restriction to open subschemes [TSPA, Tag 02OS]; [Hau14, Corollary 5.2 (b)]: for an open U ⊆ X, the blow-up of the open subscheme U along I|_U = I.comap U.ι is π⁻¹(U), as a pullback square blowUp (I.comap U.ι) ⟶ blowUp I over U ⟶ X.

The argument is Hauser's universal-property proof of the behaviour of blow-ups under base change [Hau14, Proposition 5.1], as in Hironaka.Scheme.BlowUp.AffineBlowUp.Universal.Restrict but with the global universal property (blowUp.lift, blowUp.hom_ext): π⁻¹(U) → U is admissible for I|_U (the exceptional ideal of X restricted to an open), so it lifts to blowUp (I.comap U.ι); blowUp (I.comap U.ι) → U → X is admissible for I (its inverse image of I is the exceptional ideal of the blow-up of U), so it lifts to blowUp I, landing in π⁻¹(U); the two composites are identities by uniqueness over X and over U, and the resulting isomorphism carries Mathlib's restriction square isPullback_morphismRestrict to the square of the lift.

theorem AlgebraicGeometry.range_restrictHom_subset {X : Scheme} (I : X.IdealSheafData) (U : X.Opens) : Set.range ⇑(Scheme.Hom.blowUpMap U.ι I) ⊆ Set.range ⇑((TopologicalSpace.Opens.map I.blowUpπ.base).obj U).ι

blowUpMap U.ι I lands in π⁻¹(U).

noncomputable def AlgebraicGeometry.restrictHomToPreimage {X : Scheme} (I : X.IdealSheafData) (U : X.Opens) : (I.comap U.ι).blowUp ⟶ ↑((TopologicalSpace.Opens.map I.blowUpπ.base).obj U)

blowUpMap U.ι I as a morphism to π⁻¹(U).

Equations

• AlgebraicGeometry.restrictHomToPreimage I U = AlgebraicGeometry.IsOpenImmersion.lift ((TopologicalSpace.Opens.map I.blowUpπ.base).obj U).ι (AlgebraicGeometry.Scheme.Hom.blowUpMap U.ι I) ⋯

@[simp]

theorem AlgebraicGeometry.restrictHomToPreimage_ι {X : Scheme} (I : X.IdealSheafData) (U : X.Opens) : CategoryTheory.CategoryStruct.comp (restrictHomToPreimage I U) ((TopologicalSpace.Opens.map I.blowUpπ.base).obj U).ι = Scheme.Hom.blowUpMap U.ι I

@[simp]

theorem AlgebraicGeometry.restrictHomToPreimage_ι_assoc {X : Scheme} (I : X.IdealSheafData) (U : X.Opens) {Z : Scheme} (h : I.blowUp ⟶ Z) : CategoryTheory.CategoryStruct.comp (restrictHomToPreimage I U) (CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map I.blowUpπ.base).obj U).ι h) = CategoryTheory.CategoryStruct.comp (Scheme.Hom.blowUpMap U.ι I) h

theorem AlgebraicGeometry.isInvertible_comap_morphismRestrict {X : Scheme} (I : X.IdealSheafData) (U : X.Opens) : ((I.comap U.ι).comap (I.blowUpπ ∣_ U)).IsInvertible

π⁻¹(U) → U is admissible for I|_U: the exceptional ideal restricted to an open.

noncomputable def AlgebraicGeometry.preimageToRestrict {X : Scheme} (I : X.IdealSheafData) (U : X.Opens) : ↑((TopologicalSpace.Opens.map I.blowUpπ.base).obj U) ⟶ (I.comap U.ι).blowUp

The lift π⁻¹(U) ⟶ blowUp (I|_U) over U.

Equations

• AlgebraicGeometry.preimageToRestrict I U = AlgebraicGeometry.Scheme.IdealSheafData.blowUp.lift (I.comap U.ι) (I.blowUpπ ∣_ U) ⋯

@[simp]

theorem AlgebraicGeometry.preimageToRestrict_π {X : Scheme} (I : X.IdealSheafData) (U : X.Opens) : CategoryTheory.CategoryStruct.comp (preimageToRestrict I U) (I.comap U.ι).blowUpπ = I.blowUpπ ∣_ U

@[simp]

theorem AlgebraicGeometry.preimageToRestrict_π_assoc {X : Scheme} (I : X.IdealSheafData) (U : X.Opens) {Z : Scheme} (h : ↑U ⟶ Z) : CategoryTheory.CategoryStruct.comp (preimageToRestrict I U) (CategoryTheory.CategoryStruct.comp (I.comap U.ι).blowUpπ h) = CategoryTheory.CategoryStruct.comp (I.blowUpπ ∣_ U) h

theorem AlgebraicGeometry.preimageToRestrict_restrictHom {X : Scheme} (I : X.IdealSheafData) (U : X.Opens) : CategoryTheory.CategoryStruct.comp (preimageToRestrict I U) (Scheme.Hom.blowUpMap U.ι I) = ((TopologicalSpace.Opens.map I.blowUpπ.base).obj U).ι

theorem AlgebraicGeometry.preimageToRestrict_restrictHomToPreimage {X : Scheme} (I : X.IdealSheafData) (U : X.Opens) : CategoryTheory.CategoryStruct.comp (preimageToRestrict I U) (restrictHomToPreimage I U) = CategoryTheory.CategoryStruct.id ↑((TopologicalSpace.Opens.map I.blowUpπ.base).obj U)

theorem AlgebraicGeometry.restrictHomToPreimage_morphismRestrict {X : Scheme} (I : X.IdealSheafData) (U : X.Opens) : CategoryTheory.CategoryStruct.comp (restrictHomToPreimage I U) (I.blowUpπ ∣_ U) = (I.comap U.ι).blowUpπ

theorem AlgebraicGeometry.restrictHomToPreimage_preimageToRestrict {X : Scheme} (I : X.IdealSheafData) (U : X.Opens) : CategoryTheory.CategoryStruct.comp (restrictHomToPreimage I U) (preimageToRestrict I U) = CategoryTheory.CategoryStruct.id (I.comap U.ι).blowUp

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.blowUp.restrictIso {X : Scheme} (I : X.IdealSheafData) (U : X.Opens) : (I.comap U.ι).blowUp ≅ ↑((TopologicalSpace.Opens.map I.blowUpπ.base).obj U)

blowUp (I|_U) ≅ π⁻¹(U).

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.isPullback_restrictHom {X : Scheme} (I : X.IdealSheafData) (U : X.Opens) : CategoryTheory.IsPullback (Hom.blowUpMap U.ι I) (I.comap U.ι).blowUpπ I.blowUpπ U.ι

The blow-up commutes with restriction to opens [TSPA, Tag 02OS]; [Hau14, Corollary 5.2 (b)]: the square of blowUpMap U.ι I : blowUp (I|_U) ⟶ blowUp I over U ⟶ X is a pullback.

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.exists_isPullback_restrict {X : Scheme} (I : X.IdealSheafData) (U : X.Opens) : ∃ (φ : (I.comap U.ι).blowUp ⟶ I.blowUp), CategoryTheory.IsPullback φ (I.comap U.ι).blowUpπ I.blowUpπ U.ι

Existentially: some morphism blowUp (I|_U) ⟶ blowUp I makes a pullback square over U ⟶ X.