Blowing up the inverse image of the centre

Let I be an ideal sheaf on a scheme X and let g : X' ⟶ X be a morphism of schemes. The inverse image I.comap g cuts out the scheme-theoretic inverse image g⁻¹(V(I)). On the blowup Bl_{I.comap g} X' the centre V(I) pulls back to the exceptional divisor, an effective Cartier divisor, so the universal property of Bl_I X gives a morphism of blowups over g (AlgebraicGeometry.Scheme.IdealSheafData.blowupMap), and with it a comparison morphism

Bl_{I.comap g} X' ⟶ X' ×_X Bl_I X

over X' (AlgebraicGeometry.Scheme.IdealSheafData.blowupBaseChangeHom).

• It is always a closed immersion. Over affine opens U of X and U' of X' with g(U') ⊆ U, it is the comparison Proj S[(IS)t] ⟶ Spec S ×_{Spec R} Proj R[It] of affine blowups for R = Γ(X, U), S = Γ(X', U') and I = I(U), which is a closed immersion (TauCeti.AlgebraicGeometry.isClosedImmersion_affineBlowupBaseChangeHom); these opens cover X' ×_X Bl_I X.
• For flat g it is an isomorphism: then the centre also pulls back to an effective Cartier divisor on X' ×_X Bl_I X, and the universal property of Bl_{I.comap g} X' gives the inverse. So blowing up commutes with flat base change, in particular with restriction to open subschemes.

When g is a closed immersion, for instance the inclusion of a closed subscheme Z of X, the morphism Bl_{I.comap g} Z ⟶ Bl_I X is therefore a closed immersion. This closed subscheme of Bl_I X, the blowup of Z along the inverse image of the centre, is the strict transform of Z (Stacks Project, Definition 080D and Lemma 080E); its description as the scheme-theoretic closure of the inverse image of Z ∖ V(I) is in TauCeti/AlgebraicGeometry/Blowup/StrictTransform.lean.

Main definitions

• AlgebraicGeometry.Scheme.IdealSheafData.blowupMap I g: the morphism Bl_{I.comap g} X' ⟶ Bl_I X over g.
• AlgebraicGeometry.Scheme.IdealSheafData.blowupBaseChangeHom I g: the comparison morphism Bl_{I.comap g} X' ⟶ X' ×_X Bl_I X.

Main results

• AlgebraicGeometry.Scheme.IdealSheafData.isClosedImmersion_blowupBaseChangeHom: the comparison is a closed immersion.
• AlgebraicGeometry.Scheme.IdealSheafData.isIso_blowupBaseChangeHom: for flat g it is an isomorphism, and AlgebraicGeometry.Scheme.IdealSheafData.isPullback_blowupMap_of_flat: the square formed by the two blowups over g is cartesian.
• AlgebraicGeometry.Scheme.IdealSheafData.isClosedImmersion_blowupMap: for a closed immersion g, the morphism of blowups Bl_{I.comap g} X' ⟶ Bl_I X is a closed immersion; AlgebraicGeometry.Scheme.IdealSheafData.isOpenImmersion_blowupMap: for an open immersion g it is an open immersion, onto the preimage of the image of g (AlgebraicGeometry.Scheme.IdealSheafData.opensRange_blowupMap).

References

• The Stacks Project, Lemma 0805: the blowup of the inverse image of the centre is a closed subscheme of the base change of the blowup, equal to it for flat base change.
• The Stacks Project, Definition 080D: the strict transform.
• The Stacks Project, Lemma 080E: the strict transform of a closed subscheme is the blowup of that closed subscheme along the inverse image of the centre.

The morphism of blowups and the comparison morphism

theorem AlgebraicGeometry.Scheme.IdealSheafData.isEffectiveCartier_comap_blowupToBase_comp {X X' : Scheme} (I : X.IdealSheafData) (g : X' ⟶ X) : (I.comap (CategoryTheory.CategoryStruct.comp (I.comap g).blowupToBase g)).IsEffectiveCartier

The centre V(I) pulls back to an effective Cartier divisor on Bl_{I.comap g} X', along the structure morphism followed by g: it is the exceptional divisor of that blowup.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.blowupMap {X X' : Scheme} (I : X.IdealSheafData) (g : X' ⟶ X) : (I.comap g).blowup ⟶ I.blowup

The morphism of blowups over g: the morphism Bl_{I.comap g} X' ⟶ Bl_I X lifting Bl_{I.comap g} X' ⟶ X' ⟶ X (blowupMap_blowupToBase), the unique such lift (eq_blowupMap). It is a closed immersion when g is (isClosedImmersion_blowupMap), and an open immersion when g is (isOpenImmersion_blowupMap).

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowupMap_blowupToBase {X X' : Scheme} (I : X.IdealSheafData) (g : X' ⟶ X) : CategoryTheory.CategoryStruct.comp (I.blowupMap g) I.blowupToBase = CategoryTheory.CategoryStruct.comp (I.comap g).blowupToBase g

The morphism of blowups lies over g.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowupMap_blowupToBase_assoc {X X' : Scheme} (I : X.IdealSheafData) (g : X' ⟶ X) {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (I.blowupMap g) (CategoryTheory.CategoryStruct.comp I.blowupToBase h) = CategoryTheory.CategoryStruct.comp (I.comap g).blowupToBase (CategoryTheory.CategoryStruct.comp g h)

The morphism of blowups lies over g.

theorem AlgebraicGeometry.Scheme.IdealSheafData.eq_blowupMap {X X' : Scheme} (I : X.IdealSheafData) (g : X' ⟶ X) {h : (I.comap g).blowup ⟶ I.blowup} (hh : CategoryTheory.CategoryStruct.comp h I.blowupToBase = CategoryTheory.CategoryStruct.comp (I.comap g).blowupToBase g) : h = I.blowupMap g

Every morphism Bl_{I.comap g} X' ⟶ Bl_I X over g is the morphism of blowups.

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowupLift_blowupMap {X X' : Scheme} (I : X.IdealSheafData) (g : X' ⟶ X) {T : Scheme} (f : T ⟶ X') (hf : ((I.comap g).comap f).IsEffectiveCartier) (hfg : (I.comap (CategoryTheory.CategoryStruct.comp f g)).IsEffectiveCartier) : CategoryTheory.CategoryStruct.comp ((I.comap g).blowupLift f hf) (I.blowupMap g) = I.blowupLift (CategoryTheory.CategoryStruct.comp f g) hfg

Lifting through Bl_{I.comap g} X' and then mapping to Bl_I X is lifting the composite through Bl_I X.

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowupLift_blowupMap_assoc {X X' : Scheme} (I : X.IdealSheafData) (g : X' ⟶ X) {T : Scheme} (f : T ⟶ X') (hf : ((I.comap g).comap f).IsEffectiveCartier) (hfg : (I.comap (CategoryTheory.CategoryStruct.comp f g)).IsEffectiveCartier) {Z : Scheme} (h : I.blowup ⟶ Z) : CategoryTheory.CategoryStruct.comp ((I.comap g).blowupLift f hf) (CategoryTheory.CategoryStruct.comp (I.blowupMap g) h) = CategoryTheory.CategoryStruct.comp (I.blowupLift (CategoryTheory.CategoryStruct.comp f g) hfg) h

Lifting through Bl_{I.comap g} X' and then mapping to Bl_I X is lifting the composite through Bl_I X.

theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_comap_blowupMap {X X' : Scheme} (I : X.IdealSheafData) (g : X' ⟶ X) : (I.comap I.blowupToBase).comap (I.blowupMap g) = (I.comap g).comap (I.comap g).blowupToBase

The exceptional divisor of Bl_I X pulls back along the morphism of blowups to the exceptional divisor of Bl_{I.comap g} X'.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.blowupBaseChangeHom {X X' : Scheme} (I : X.IdealSheafData) (g : X' ⟶ X) : (I.comap g).blowup ⟶ CategoryTheory.Limits.pullback g I.blowupToBase

The comparison of blowups under base change: the morphism Bl_{I.comap g} X' ⟶ X' ×_X Bl_I X with components the structure morphism of the blowup of X' and the morphism of blowups. It is a closed immersion (isClosedImmersion_blowupBaseChangeHom), and an isomorphism for flat g (isIso_blowupBaseChangeHom).

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowupBaseChangeHom_fst {X X' : Scheme} (I : X.IdealSheafData) (g : X' ⟶ X) : CategoryTheory.CategoryStruct.comp (I.blowupBaseChangeHom g) (CategoryTheory.Limits.pullback.fst g I.blowupToBase) = (I.comap g).blowupToBase

The comparison is a morphism over X'.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowupBaseChangeHom_fst_assoc {X X' : Scheme} (I : X.IdealSheafData) (g : X' ⟶ X) {Z : Scheme} (h : X' ⟶ Z) : CategoryTheory.CategoryStruct.comp (I.blowupBaseChangeHom g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst g I.blowupToBase) h) = CategoryTheory.CategoryStruct.comp (I.comap g).blowupToBase h

The comparison is a morphism over X'.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowupBaseChangeHom_snd {X X' : Scheme} (I : X.IdealSheafData) (g : X' ⟶ X) : CategoryTheory.CategoryStruct.comp (I.blowupBaseChangeHom g) (CategoryTheory.Limits.pullback.snd g I.blowupToBase) = I.blowupMap g

The projection of the comparison to Bl_I X is the morphism of blowups.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowupBaseChangeHom_snd_assoc {X X' : Scheme} (I : X.IdealSheafData) (g : X' ⟶ X) {Z : Scheme} (h : I.blowup ⟶ Z) : CategoryTheory.CategoryStruct.comp (I.blowupBaseChangeHom g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g I.blowupToBase) h) = CategoryTheory.CategoryStruct.comp (I.blowupMap g) h

The projection of the comparison to Bl_I X is the morphism of blowups.

theorem AlgebraicGeometry.Scheme.IdealSheafData.pullback_blowupToBase_hom_ext {X X' : Scheme} (I : X.IdealSheafData) (g : X' ⟶ X) {T : Scheme} {u v : T ⟶ CategoryTheory.Limits.pullback g I.blowupToBase} (h : CategoryTheory.CategoryStruct.comp u (CategoryTheory.Limits.pullback.fst g I.blowupToBase) = CategoryTheory.CategoryStruct.comp v (CategoryTheory.Limits.pullback.fst g I.blowupToBase)) (hf : (I.comap (CategoryTheory.CategoryStruct.comp u (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst g I.blowupToBase) g))).IsEffectiveCartier) : u = v

Two morphisms into X' ×_X Bl_I X agree if they agree after projecting to X' and the centre V(I) pulls back to an effective Cartier divisor along their common composite to X.

Flat base change

instance AlgebraicGeometry.Scheme.IdealSheafData.isIso_blowupBaseChangeHom {X X' : Scheme} (I : X.IdealSheafData) (g : X' ⟶ X) [Flat g] : CategoryTheory.IsIso (I.blowupBaseChangeHom g)

Blowing up commutes with flat base change: for flat g, the comparison Bl_{I.comap g} X' ⟶ X' ×_X Bl_I X is an isomorphism. Its inverse is the lift of the projection X' ×_X Bl_I X ⟶ X' given by the universal property of Bl_{I.comap g} X'.

theorem AlgebraicGeometry.Scheme.IdealSheafData.isPullback_blowupMap_of_flat {X X' : Scheme} (I : X.IdealSheafData) (g : X' ⟶ X) [Flat g] : CategoryTheory.IsPullback (I.comap g).blowupToBase (I.blowupMap g) g I.blowupToBase

The blowup of X' along the inverse image of the centre is the base change of the blowup of X along V(I), for flat g: the square formed by the two blowups over g is cartesian.

instance AlgebraicGeometry.Scheme.IdealSheafData.isOpenImmersion_blowupMap {X X' : Scheme} (I : X.IdealSheafData) (g : X' ⟶ X) [IsOpenImmersion g] : IsOpenImmersion (I.blowupMap g)

Blowing up commutes with restriction to open subschemes: for an open immersion g, the morphism of blowups Bl_{I.comap g} X' ⟶ Bl_I X is an open immersion, with image the preimage of the image of g (opensRange_blowupMap).

theorem AlgebraicGeometry.Scheme.IdealSheafData.opensRange_blowupMap {X X' : Scheme} (I : X.IdealSheafData) (g : X' ⟶ X) [IsOpenImmersion g] : Hom.opensRange (I.blowupMap g) = (TopologicalSpace.Opens.map I.blowupToBase.base).obj (Hom.opensRange g)

For an open immersion g, the image of the morphism of blowups is the preimage in Bl_I X of the image of g.

The comparison is a closed immersion

instance AlgebraicGeometry.Scheme.IdealSheafData.isClosedImmersion_blowupBaseChangeHom {X X' : Scheme} (I : X.IdealSheafData) (g : X' ⟶ X) : IsClosedImmersion (I.blowupBaseChangeHom g)

The blowup of the inverse image of the centre is a closed subscheme of the base change of the blowup: for every morphism g : X' ⟶ X, the comparison Bl_{I.comap g} X' ⟶ X' ×_X Bl_I X is a closed immersion.

instance AlgebraicGeometry.Scheme.IdealSheafData.isClosedImmersion_blowupMap {X X' : Scheme} (I : X.IdealSheafData) (g : X' ⟶ X) [IsClosedImmersion g] : IsClosedImmersion (I.blowupMap g)

The blowup of a closed subscheme is a closed subscheme of the blowup: for a closed immersion g : X' ⟶ X, the morphism of blowups Bl_{I.comap g} X' ⟶ Bl_I X is a closed immersion. Its image is the strict transform of X' (Stacks Project, Lemma 080E).