Morphisms into blow-ups

The morphisms that the universal property of the blow-up provides [Hau14, Definition 4.4]; [TSPA, Tag 0806]. The blow-up map π : blowUp I ⟶ X is admissible for I — the inverse image of I is invertible — and every admissible f : Y ⟶ X factors through it:

• blowUp.lift I f hf : Y ⟶ blowUp I, the lift of an admissible f;
• Scheme.Hom.blowUpMap h D : blowUp (D.comap h) ⟶ blowUp D, the morphism of blow-ups over a morphism h : Y ⟶ X of the base, the lift of the admissible π_Y ≫ h: 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 square of blow-ups under flat base change [TSPA, Tag 0805];
• Scheme.Hom.pushforwardBlowUp j Z : Z.blowUp ⟶ (Z.map j).blowUp, for a closed immersion j : Y ⟶ X and a centre Z ⊆ Y, the morphism blowUpMap j (Z.map j) read with the source Z.blowUp, which is the blow-up of Y along (Z.map j).comap j because the ideal sheaves of Y are the ideal sheaves of X containing the ideal of Y (comap_map_of_isClosedImmersion): the push-forward of a blow-up sequence along a closed immersion [Kol07, Definition 30, 30.3].

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.blowUp.lift {X : Scheme} (I : X.IdealSheafData) {Y : Scheme} (f : Y ⟶ X) (hf : (I.comap f).IsInvertible) : Y ⟶ I.blowUp

The lift of an admissible f : Y ⟶ X to the blow-up.

Equations

• AlgebraicGeometry.Scheme.IdealSheafData.blowUp.lift I f hf = ⋯.choose

theorem AlgebraicGeometry.isInvertible_comap_π_comp {X Y : Scheme} (h : Y ⟶ X) (D : X.IdealSheafData) : (D.comap (CategoryTheory.CategoryStruct.comp (D.comap h).blowUpπ h)).IsInvertible

π_Y ≫ h : B_{D·𝒪_Y} Y ⟶ X is admissible for D — its inverse image of D is the exceptional ideal of B_{D·𝒪_Y} Y.

noncomputable def AlgebraicGeometry.Scheme.Hom.blowUpMap {X Y : Scheme} (h : Y ⟶ X) (D : X.IdealSheafData) : (D.comap h).blowUp ⟶ D.blowUp

The morphism of blow-ups induced by h : Y ⟶ X, blowUp (D.comap h) ⟶ blowUp D over h [Kol07, Definition 30, 30.1]; [TSPA, Tag 0805]: the lift of the admissible π_Y ≫ h through the universal property of B_D X. For an open immersion h = U.ι it is the restriction blowUp (D|_U) ⟶ blowUp D, an isomorphism onto π⁻¹(U) (blowUp.restrictIso).

Equations

• AlgebraicGeometry.Scheme.Hom.blowUpMap h D = AlgebraicGeometry.Scheme.IdealSheafData.blowUp.lift D (CategoryTheory.CategoryStruct.comp (D.comap h).blowUpπ h) ⋯

theorem AlgebraicGeometry.comap_map_of_isClosedImmersion {X Y : Scheme} (j : Y ⟶ X) [IsClosedImmersion j] (Z : Y.IdealSheafData) : (Z.map j).comap j = Z

For a closed immersion j : Y ⟶ X, the inverse image of the pushforward of Z is Z — the ideal sheaves of Y correspond to the ideal sheaves of X containing ker j, so that a centre of Y and its push-forward to X are the same subscheme [Kol07, Definition 30, 30.3]. The fibre product of the closed immersion V(j_* Z) → X (the scheme-theoretic image of V(Z) → Y → X) with j is V(Z), since j is a monomorphism and V(Z) ≅ V(j_* Z).

noncomputable def AlgebraicGeometry.Scheme.Hom.pushforwardBlowUp {X Y : Scheme} (j : Y ⟶ X) [IsClosedImmersion j] (Z : Y.IdealSheafData) : Z.blowUp ⟶ (Z.map j).blowUp

For a closed immersion j : Y ⟶ X and a centre Z ⊆ Y, the induced closed immersion Z.blowUp ⟶ blowUp X (j_* Z) onto the strict transform of Y Kol07, Definition 30, 30.2 and 30.3: the lift blowUpMap j (j_* Z), whose source blowUp Y ((j_* Z)·𝒪_Y) is Z.blowUp because (Z.map j).comap j = Z for a closed immersion (AlgebraicGeometry.comap_map_of_isClosedImmersion). The closed-immersion hypothesis is essential: for a general j the hom-set can be empty (the fold X ⊔ X ⟶ X with Z = (⊤, ⊥) has Z.blowUp ≅ X and (Z.map j).blowUp = blowUp X ⊥ = ∅).

Equations

• AlgebraicGeometry.Scheme.Hom.pushforwardBlowUp j Z = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (AlgebraicGeometry.Scheme.Hom.blowUpMap j (Z.map j))