Open restriction of the affine blow-up is a pullback #
The blow-up of an open subscheme U of X along U ∩ Z is the restriction of the blow-up of
X along Z to π⁻¹(U) [Hau14, Corollary 5.2 (b)], a special case of the behaviour of blow-ups
under base change [Hau14, Proposition 5.1], proved here through the universal property: for an
affine open U = Spec S ⊆ Spec R and J = I S, the square of
affineBlowUp.mapHom φ : affineBlowUp J ⟶ affineBlowUp I over Spec.map φ : Spec S ⟶ Spec R is
a pullback, and affineBlowUp J ≅ π⁻¹(U) over U.
The argument. Let P = π⁻¹(U) ⊆ B = affineBlowUp I. The map P → U ≅ Spec S is admissible
for J — J·𝒪_P is the exceptional ideal of B restricted to the open P, invertible by
affineBlowUp.isInvertible_exceptionalIdeal — so the universal property gives
ψ : P ⟶ B' = affineBlowUp J over Spec S. The morphism mapHom φ : B' ⟶ B lies over
Spec.map φ, hence lands in P, as m' : B' ⟶ P (IsOpenImmersion.lift). Both ψ ≫ m' ≫ P.ι
and P.ι are lifts of P → Spec R (admissible for I), so they agree by uniqueness and
ψ ≫ m' = 𝟙 (P.ι is a monomorphism); both m' ≫ ψ and 𝟙 are lifts of π' : B' → Spec S
(admissible for J), so m' ≫ ψ = 𝟙. Thus m' is an isomorphism B' ≅ P with
m' ≫ P.ι = mapHom φ, and the pullback square isPullback_morphismRestrict of P transports
along it. Openness of U is used three times (to restrict the exceptional ideal, to factor
mapHom φ through P, and to transport the restriction square); for an arbitrary base change
the blow-up of the base change is only the strict transform inside the fibre product
[Hau14, Proposition 5.1]. A chartwise proof is also possible [TSPA, Tag 0805].
The ideal sheaf of J = I S on Spec S is the inverse image of the ideal sheaf of I along
Spec.map φ.
The isomorphism Spec S ≅ U onto the image U of the open immersion Spec.map φ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The open P = π⁻¹(U) ⊆ affineBlowUp I, for U the image of Spec.map φ.
Equations
Instances For
mapHom φ lands in π⁻¹(U) (it lies over Spec.map φ, whose image is U).
mapHom φ as a morphism to π⁻¹(U).
Equations
Instances For
The structure map π⁻¹(U) → U ≅ Spec S.
Equations
- One or more equations did not get rendered due to their size.
Instances For
π⁻¹(U) → Spec R is admissible for I: the exceptional ideal restricted to an open is
invertible.
π⁻¹(U) → Spec S is admissible for J.
The lift π⁻¹(U) ⟶ affineBlowUp J over Spec S.
Equations
Instances For
affineBlowUp (I S) ≅ π⁻¹(U) over U, the isomorphism composed with the inclusion being
mapHom φ.
Equations
- AlgebraicGeometry.blowUpIsoPreimage φ hJ = { hom := AlgebraicGeometry.mapHomToPreimage φ hJ, inv := AlgebraicGeometry.preimageToBlowUp φ hJ, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
Open restriction is a pullback [Hau14, Proposition 5.1 and Corollary 5.2 (b)]: for
Spec S ⊆ Spec R an affine open and J = I S, the square of affineBlowUp.mapHom φ over
Spec.map φ is a pullback (isPullback_morphismRestrict transported along
blowUpIsoPreimage).
Existentially: affineBlowUp (I S) is π⁻¹(U), compatibly with mapHom φ.