The strict transform as a scheme-theoretic closure

Let I be an ideal sheaf on a scheme X, let b : Bl_I X ⟶ X be the blowup of X along V(I), and let g : X' ⟶ X be a morphism of schemes. The strict transform of X' is the scheme-theoretic closure, in the base change X' ×_X Bl_I X, of the open part lying over the complement X ∖ V(I) of the centre, that is, of the complement of the inverse image of the exceptional divisor (Stacks Project, Definition 080D). When g is the inclusion of a closed subscheme Z, the base change is the inverse image b⁻¹(Z), and the strict transform is the scheme-theoretic closure in Bl_I X of b⁻¹(Z) ∖ b⁻¹(V(I)).

This file proves that the strict transform is the blowup of X' along the inverse image of the centre (Stacks Project, Lemma 080E): the closed immersion Bl_{I.comap g} X' ⟶ X' ×_X Bl_I X of TauCeti/AlgebraicGeometry/Blowup/Pullback.lean (AlgebraicGeometry.Scheme.IdealSheafData.blowupBaseChangeHom) has the same kernel as the inclusion of the open part over X ∖ V(I). Consequently the kernel of the morphism of blowups Bl_{I.comap g} X' ⟶ Bl_I X, which is a closed immersion when g is, is the ideal sheaf of the scheme-theoretic closure of b⁻¹(Z) ∖ b⁻¹(V(I)) in Bl_I X.

The proof compares the two morphisms into X' ×_X Bl_I X through factorizations.

• The open part over X ∖ V(I) factors through Bl_{I.comap g} X': the centre pulls back to the empty closed subscheme on it, which is an effective Cartier divisor, so the universal property of the blowup applies.
• Conversely, the restriction of Bl_{I.comap g} X' ⟶ X' ×_X Bl_I X to the complement of the exceptional divisor factors through the open part over X ∖ V(I), and this complement is scheme-theoretically dense, because the exceptional divisor is an effective Cartier divisor (IsEffectiveCartier.isSchemeTheoreticallyDominant_support_compl_ι).

No finiteness, Noetherianity or flatness hypothesis is needed.

Main results

• AlgebraicGeometry.Scheme.IdealSheafData.ker_blowupBaseChangeHom: the blowup of X' along the inverse image of the centre is the scheme-theoretic closure, in X' ×_X Bl_I X, of the open part lying over X ∖ V(I).
• AlgebraicGeometry.Scheme.IdealSheafData.ker_blowupMap: the image of Bl_{I.comap g} X' in Bl_I X is the scheme-theoretic closure of the image of that open part.

References

• The Stacks Project, Definition 080D: the strict transform.
• The Stacks Project, Lemma 080E: the strict transform is the blowup along the inverse image of the centre.

theorem AlgebraicGeometry.Scheme.IdealSheafData.ker_blowupBaseChangeHom {X X' : Scheme} (I : X.IdealSheafData) (g : X' ⟶ X) : Hom.ker (I.blowupBaseChangeHom g) = Hom.ker ((TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst g I.blowupToBase) g).base).obj I.support.compl).ι

The strict transform is the blowup along the inverse image of the centre. The closed immersion Bl_{I.comap g} X' ⟶ X' ×_X Bl_I X has the same kernel as the inclusion of the open part of X' ×_X Bl_I X lying over X ∖ V(I): the blowup of X' along the inverse image of the centre is the scheme-theoretic closure of that open part.

theorem AlgebraicGeometry.Scheme.IdealSheafData.ker_blowupMap {X X' : Scheme} (I : X.IdealSheafData) (g : X' ⟶ X) : Hom.ker (I.blowupMap g) = Hom.ker (CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst g I.blowupToBase) g).base).obj I.support.compl).ι (CategoryTheory.Limits.pullback.snd g I.blowupToBase))

The strict transform as a scheme-theoretic closure in the blowup. The morphism of blowups Bl_{I.comap g} X' ⟶ Bl_I X has the same kernel as the open part of X' ×_X Bl_I X lying over X ∖ V(I), mapped to Bl_I X. For a closed immersion g, the morphism of blowups is a closed immersion (isClosedImmersion_blowupMap), so its image, the blowup of X' along the inverse image of the centre, is the scheme-theoretic closure in Bl_I X of b⁻¹(X') ∖ b⁻¹(V(I)), the strict transform of X'.