The morphism of blow-ups induced by a morphism of the base

The universal property of the blow-up [TSPA, Tag 0806] lifts every admissible f : Y ⟶ X (one along which I becomes invertible) to blowUp.lift I f hf : Y ⟶ blowUp I, the only morphism over f (blowUp.lift_π, blowUp.eq_lift). For a morphism h : Y ⟶ X and an ideal sheaf D on X, the composite π_Y ≫ h : B_{D·𝒪_Y} Y ⟶ X of the blow-up of Y along the inverse image ideal D.comap h with h is admissible for D: its inverse image of D is (D.comap h).comap π_Y, the exceptional ideal of B_{D·𝒪_Y} Y, which is invertible. Its lift is the morphism of blow-ups

blowUpMap h D : blowUp (D.comap h) ⟶ blowUp D with blowUpMap h D ≫ π_X = π_Y ≫ h

(blowUpMap_π), the morphism h^*π of the pull-back of a blow-up sequence along h [Kol07, Definition 30, 30.1] and the top arrow of the cartesian diagram of blow-ups under flat base change [TSPA, Tag 0805]: for flat h the square is cartesian (isPullback_blowUpMap).

The flat square uses that the blow-up satisfies the universal property in the form of the predicate IsBlowUp (blowUp.isBlowUp, Hironaka.Scheme.BlowUp.Glue.Global), through which the theorems of the blow-up calculus proved for an abstract IsBlowUp (Hironaka.Scheme.BlowUp.FlatBaseChange, Hironaka.Scheme.BlowUp.ProductCenter, Hironaka.Scheme.BlowUp.Transform.StrictTransform) instantiate at the blow-up.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.lift_π {X : Scheme} (I : X.IdealSheafData) {Y : Scheme} (f : Y ⟶ X) (hf : (I.comap f).IsInvertible) : CategoryTheory.CategoryStruct.comp (lift I f hf) I.blowUpπ = f

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.lift_π_assoc {X : Scheme} (I : X.IdealSheafData) {Y : Scheme} (f : Y ⟶ X) (hf : (I.comap f).IsInvertible) {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (lift I f hf) (CategoryTheory.CategoryStruct.comp I.blowUpπ h) = CategoryTheory.CategoryStruct.comp f h

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.eq_lift {X : Scheme} (I : X.IdealSheafData) {Y : Scheme} (f : Y ⟶ X) (hf : (I.comap f).IsInvertible) (g : Y ⟶ I.blowUp) (hg : CategoryTheory.CategoryStruct.comp g I.blowUpπ = f) : g = lift I f hf

@[simp]

theorem AlgebraicGeometry.blowUpMap_π {X Y : Scheme} (h : Y ⟶ X) (D : X.IdealSheafData) : CategoryTheory.CategoryStruct.comp (Scheme.Hom.blowUpMap h D) D.blowUpπ = CategoryTheory.CategoryStruct.comp (D.comap h).blowUpπ h

The defining equation: blowUpMap h D lies over h.

@[simp]

theorem AlgebraicGeometry.blowUpMap_π_assoc {X Y : Scheme} (h : Y ⟶ X) (D : X.IdealSheafData) {Z : Scheme} (h✝ : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (Scheme.Hom.blowUpMap h D) (CategoryTheory.CategoryStruct.comp D.blowUpπ h✝) = CategoryTheory.CategoryStruct.comp (D.comap h).blowUpπ (CategoryTheory.CategoryStruct.comp h h✝)

The defining equation: blowUpMap h D lies over h.

theorem AlgebraicGeometry.eqToHom_comp_blowUpπ {X : Scheme} {I J : X.IdealSheafData} (e : I = J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) J.blowUpπ = I.blowUpπ

Transport of the projection along an equality of centres.

theorem AlgebraicGeometry.eqToHom_comp_blowUpπ_assoc {X : Scheme} {I J : X.IdealSheafData} (e : I = J) {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp J.blowUpπ h) = CategoryTheory.CategoryStruct.comp I.blowUpπ h

Transport of the projection along an equality of centres.

theorem AlgebraicGeometry.exists_eqToHom_apply_eq {X : Scheme} {I J : X.IdealSheafData} (e : I = J) (t : ↥J.blowUp) : ∃ (s : ↥I.blowUp), (CategoryTheory.eqToHom ⋯) s = t

Points of a blow-up transport along an equality of centres e : I = J: every point of blowUp J is the image of a point of blowUp I under the eqToHom of eqToHom_comp_blowUpπ.

theorem AlgebraicGeometry.eq_blowUpMap {X Y : Scheme} (h : Y ⟶ X) (D : X.IdealSheafData) (g : (D.comap h).blowUp ⟶ D.blowUp) (hg : CategoryTheory.CategoryStruct.comp g D.blowUpπ = CategoryTheory.CategoryStruct.comp (D.comap h).blowUpπ h) : g = Scheme.Hom.blowUpMap h D

blowUpMap h D is the only morphism over h.

theorem AlgebraicGeometry.isPullback_blowUpMap {X Y : Scheme} (h : Y ⟶ X) (D : X.IdealSheafData) [Flat h] : CategoryTheory.IsPullback (Scheme.Hom.blowUpMap h D) (D.comap h).blowUpπ D.blowUpπ h

For flat h the square of blowUpMap h D over h is cartesian, B_{D·𝒪_Y} Y = Y ×_X B_D X [TSPA, Tag 0805] (from IsBlowUp.exists_isPullback_of_flat).