Lifts of closed immersions to blow-ups #
For a closed subscheme j : S ↪ X and a centre Z ⊆ X, the blow-up B_{Z ∩ S} S is naturally
identified with the strict transform π⁻¹_* S ⊂ B_Z X, and conversely a centre Z ⊆ S pushed
forward to X gives the closed immersion B_Z S ↪ B_{j_* Z} X Kol07, Definition 30, 30.2 and
30.3. This module holds the blow-up calculus behind both, in a form the vocabulary of the main
theorems can use (AlgebraicGeometry.Scheme.Hom.pushforwardBlowUp, the morphism
B_Z S ⟶ B_{j_* Z} X built from (Z.map j).comap j = Z, comap_map_of_isClosedImmersion):
isClosedImmersion_blowUpMap,ker_blowUpMap_subschemeι: forj = J.subschemeιthe liftblowUpMap j D : B_{D ∩ V(J)} V(J) ⟶ B_D Xis a closed immersion with kernel the strict transform ofV(J)(the identification ofB_{D ∩ V(J)} V(J)with the strict transform,exists_iso_strictTransform_subscheme, and the uniqueness of lifts).isIso_blowUpMap_of_isIso,isClosedImmersion_blowUpMap_of_isClosedImmersion,ker_blowUpMap_of_isClosedImmersion: the same for any closed immersionj, through its scheme-theoretic imagej = j.toImage ≫ j.ker.subschemeι(blowUpMapof an isomorphism is an isomorphism, the top arrow of the flat base-change square); hencepushforwardBlowUp j Zis a closed immersion (the instanceScheme.instIsClosedImmersionPushforwardBlowUp).- Cartesian squares: pushing forward along a closed immersion commutes with pulling back along a
flat morphism, and the induced square of blow-ups over a cartesian square of the bases is
cartesian (
comap_map_of_isPullback,isPullback_blowUpMap_of_isPullback).
For a closed subscheme V(J) ⊆ X and a centre D, the induced morphism of blow-ups
blowUpMap J.subschemeι D : B_{D ∩ V(J)} V(J) ⟶ B_D X is a closed immersion — the isomorphism of
B_{D ∩ V(J)} V(J) onto the strict transform of V(J) (exists_iso_strictTransform_subscheme)
followed by the strict transform's inclusion, by the uniqueness of lifts
[Kol07, Definition 30, 30.2].
The lift blowUpMap J.subschemeι D has kernel the strict transform of V(J): its image is
π⁻¹_* V(J).
The lift along an isomorphism is an isomorphism: the top arrow of the flat base-change square
isPullback_blowUpMap.
The lift along a composite factors through the lifts of the factors (the uniqueness clause of the universal property).
One step for any closed immersion j : Y ⟶ X, written j = e ≫ J.subschemeι with e an
isomorphism (its scheme-theoretic image): the lift blowUpMap j D is a closed immersion.
One step for any closed immersion written j = e ≫ J.subschemeι: the kernel of the lift is the
strict transform of V(J).
For any closed immersion j, blowUpMap j D is a closed immersion.
For any closed immersion j, the kernel of blowUpMap j D is the strict transform of the
image of j.
The induced morphism of blow-ups along a closed immersion is a closed immersion
(AlgebraicGeometry.isClosedImmersion_blowUpMap_of_isClosedImmersion).
Cartesian squares: ideal sheaves and blow-ups over a base change #
Transport of a cartesian square along equalities of its four objects and heterogeneous
equalities of its four morphisms (bookkeeping for the eqToHom identifications of blow-up
sources).
The inverse image along a commutative square: (I.comap h).comap j' = (I.comap j).comap hS
when j' ≫ h = hS ≫ j (comap_comp twice) — pulling back by h and then restricting gives the
same result as restricting and then pulling back, as in the proof of [Kol07, Lemma 102].
The square of a closed subscheme V(Z) and its inverse image V(Z.comap f) is cartesian,
with Mathlib's subschemeMap as the induced map (isPullback_of_isClosedImmersion; the kernels
are Z and Z.comap f by ker_subschemeι).
On a cartesian square j' ≫ h = hS ≫ j with j a closed immersion, pushing forward along
j then pulling back along h is pulling back along hS then pushing forward along j':
(Z.map j).comap h = (Z.comap hS).map j' — both are the ideal of Z ×_X X' = (Z ×_Y Y') in X'
(pasting isPullback_subschemeι_comap with the square, ker_fst_of_isClosedImmersion).
For h flat and a cartesian square j' ≫ h = hS ≫ j, the induced square of the blow-ups
along D, D.comap h, D.comap j and (D.comap h).comap j' = (D.comap j).comap hS is cartesian
(flat base change [TSPA, Tag 0805] over a cartesian square):
B_{D'} Y' = Y' ×_Y B_{D_Y} Y = (X' ×_X Y) ×_Y B_{D_Y} Y = B_{D_Y} Y ×_{B_D X} (X' ×_X B_D X), by
pasting the flat base-change squares (isPullback_blowUpMap, for h and for its base change
hS) with the given square and cancelling (IsPullback.of_right); the commutativity of the
blow-up square is the uniqueness clause of the universal property (blowUp.hom_ext).