A blow-up is a closed subscheme of a projective bundle

For an ideal sheaf I on a scheme X whose sheaf of modules I.toModules is quasi-coherent, the blow-up Bl_I X = Proj_X (⨁ₙ Iⁿ) is a closed subscheme of the projective bundle P(I) = Proj_X (Sym I) over X [TSPA, Tag 02NS]: the surjection Sym I → ⨁ₙ Iⁿ, the identity of I in degree one, induces a closed immersion Bl_I X ⟶ P(I) over X (Scheme.IdealSheafData.blowUpToProjectiveBundle, isClosedImmersion_blowUpToProjectiveBundle). Over an affine open U it is Proj of the surjection Sym_{Γ(X, U)} I(U) → Rees(I(U)), a closed immersion (Proj.isClosedImmersion_map_of_surjective); these charts are natural in U, so they glue to a morphism of the glued schemes over X, and over the chart of U it is the chart morphism, so it is a closed immersion, being one is local on the target.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.toModulesToRees {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : ↑(I.toModules.presheaf.obj (Opposite.op ↑U)) →ₗ[↑(X.presheaf.obj (Opposite.op ↑U))] ↥(reesAlgebra (I.ideal U))

The degree-one map I(U) → Rees(I(U)), a ↦ a t, on the sections of I.toModules over an affine open U.

Equations

• I.toModulesToRees U = reesAlgebra.degreeOne (I.ideal U) ∘ₗ ↑(I.toModulesSectionsEquiv U)

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.symToRees {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : SymmetricAlgebra.grading ↑(X.presheaf.obj (Opposite.op ↑U)) ↑(I.toModules.presheaf.obj (Opposite.op ↑U)) →+*ᵍ reesAlgebra.grading (I.ideal U)

The graded surjection Sym_{Γ(X, U)} Γ(I.toModules, U) → Rees(I(U)), the lift of toModulesToRees.

Equations

• I.symToRees U = SymmetricAlgebra.gradedLift (reesAlgebra.grading (I.ideal U)) (I.toModulesToRees U) ⋯

theorem AlgebraicGeometry.Scheme.IdealSheafData.symToRees_ι {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) (s : ↑(I.toModules.presheaf.obj (Opposite.op ↑U))) : (I.symToRees U) ((SymmetricAlgebra.ι ↑(X.presheaf.obj (Opposite.op ↑U)) ↑(I.toModules.presheaf.obj (Opposite.op ↑U))) s) = (reesAlgebra.degreeOne (I.ideal U)) ((I.toModulesSectionsEquiv U) s)

theorem AlgebraicGeometry.Scheme.IdealSheafData.symToRees_algebraMap {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) (r : ↑(X.presheaf.obj (Opposite.op ↑U))) : (I.symToRees U) ((algebraMap (↑(X.presheaf.obj (Opposite.op ↑U))) (SymmetricAlgebra ↑(X.presheaf.obj (Opposite.op ↑U)) ↑(I.toModules.presheaf.obj (Opposite.op ↑U)))) r) = (algebraMap ↑(X.presheaf.obj (Opposite.op ↑U)) ↥(reesAlgebra (I.ideal U))) r

theorem AlgebraicGeometry.Scheme.IdealSheafData.degreeOne_mem_range {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) (a : ↥(I.ideal U)) : (reesAlgebra.degreeOne (I.ideal U)) a ∈ (↑(I.symToRees U)).range

theorem AlgebraicGeometry.Scheme.IdealSheafData.symToRees_surjective {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : Function.Surjective ⇑(I.symToRees U)

The graded map Sym I(U) → Rees(I(U)) is surjective: the Rees algebra is generated by its degree-one elements a t, a ∈ I(U).

theorem AlgebraicGeometry.Scheme.IdealSheafData.irrelevant_le_map_symToRees {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : HomogeneousIdeal.irrelevant (reesAlgebra.grading (I.ideal U)) ≤ HomogeneousIdeal.map (I.symToRees U) (HomogeneousIdeal.irrelevant (SymmetricAlgebra.grading ↑(X.presheaf.obj (Opposite.op ↑U)) ↑(I.toModules.presheaf.obj (Opposite.op ↑U))))

The Proj.map hypothesis for symToRees: the irrelevant ideal of Rees(I(U)), generated by the degree-one elements a t, lies in the ideal generated by the image of that of Sym I(U).

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.blowUpChart {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : affineBlowUp (I.ideal U) ⟶ affineProjectiveBundle ↑(X.presheaf.obj (Opposite.op ↑U)) ↑(I.toModules.presheaf.obj (Opposite.op ↑U))

The chart of the closed immersion of the blow-up in the projective bundle over an affine open U: Proj of the surjection Sym I(U) → Rees(I(U)).

Equations

• I.blowUpChart U = AlgebraicGeometry.Proj.map (I.symToRees U) ⋯

theorem AlgebraicGeometry.Scheme.IdealSheafData.isClosedImmersion_blowUpChart {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : IsClosedImmersion (I.blowUpChart U)

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUpChart_π {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : CategoryTheory.CategoryStruct.comp (I.blowUpChart U) (affineProjectiveBundle.π ↑(X.presheaf.obj (Opposite.op ↑U)) ↑(I.toModules.presheaf.obj (Opposite.op ↑U))) = affineBlowUp.π (I.ideal U)

Over the base: the chart lies over Spec Γ(X, U).

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUpChart_naturality {X : Scheme} (I : X.IdealSheafData) [SheafOfModules.IsQuasicoherent I.toModules] {U V : ↑X.affineOpens} (h : U ⟶ V) : CategoryTheory.CategoryStruct.comp ((affineBlowUpFunctor I).map h) (I.blowUpChart V) = CategoryTheory.CategoryStruct.comp (I.blowUpChart U) ((projectiveBundleFunctor I.toModules).map h)

The charts are natural in the affine open: Proj of the commutative square of graded maps Sym I(V) → Rees(I(V)) → Rees(I(U)), Sym I(V) → Sym I(U) → Rees(I(U)), checked on the generators and the constants.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.blowUpNatTrans {X : Scheme} (I : X.IdealSheafData) [SheafOfModules.IsQuasicoherent I.toModules] : (relativeGluingDataOf I ⋯).functor ⟶ (projectiveBundleGluingData I.toModules).functor

The charts blowUpChart, as a natural transformation from the affine blow-ups to the projective bundles of I.toModules over the affine opens.

Equations

• I.blowUpNatTrans = { app := I.blowUpChart, naturality := ⋯ }

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUpNatTrans_app_comp {X : Scheme} (I : X.IdealSheafData) [SheafOfModules.IsQuasicoherent I.toModules] (U : ↑X.affineOpens) : CategoryTheory.CategoryStruct.comp (I.blowUpNatTrans.app U) ((projectiveBundleNatTrans I.toModules).app U) = (affineBlowUpNatTrans I).app U

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.blowUpToProjectiveBundle {X : Scheme} (I : X.IdealSheafData) [SheafOfModules.IsQuasicoherent I.toModules] : I.blowUp ⟶ I.toModules.projectiveBundle

The closed immersion of the blow-up into the projective bundle Bl_I X ⟶ P(I) over X [TSPA, Tag 02NS], glued from the charts blowUpChart.

Equations

• I.blowUpToProjectiveBundle = CategoryTheory.Limits.colimMap I.blowUpNatTrans

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUpToProjectiveBundle_π {X : Scheme} (I : X.IdealSheafData) [SheafOfModules.IsQuasicoherent I.toModules] : CategoryTheory.CategoryStruct.comp I.blowUpToProjectiveBundle I.toModules.projectiveBundleπ = I.blowUpπ

theorem AlgebraicGeometry.Scheme.IdealSheafData.isClosedImmersion_blowUpToProjectiveBundle {X : Scheme} (I : X.IdealSheafData) [SheafOfModules.IsQuasicoherent I.toModules] : IsClosedImmersion I.blowUpToProjectiveBundle

theorem AlgebraicGeometry.IsProjective.isIso_comp {X X' Y : Scheme} (e : X' ⟶ X) [CategoryTheory.IsIso e] (f : X ⟶ Y) [hf : IsProjective f] : IsProjective (CategoryTheory.CategoryStruct.comp e f)

A projective morphism composed with an isomorphism on the source is projective.

theorem AlgebraicGeometry.Scheme.IdealSheafData.isProjective_blowUpπ {X : Scheme} (I : X.IdealSheafData) [IsLocallyNoetherian X] : IsProjective I.blowUpπ

A blow-up of a locally Noetherian scheme is projective [TSPA, Tag 02NS]: it is a closed subscheme of the projective bundle P(I) of its ideal sheaf (blowUpToProjectiveBundle), which is quasi-coherent of finite type (isFinitePresentation_toModules).