Charts and properness of the glued blow-up

For the blow-up blowUpOf I h (glued from the affine blow-ups over the affine opens of X, given the pullback squares h):

• the components blowUpOf.ι I h U : affineBlowUp (I.ideal U) ⟶ blowUpOf I h are open immersions with image π⁻¹(U) (Mathlib's toBase_preimage_eq_opensRange_ι);
• the global charts blowUpOf.chart I h U a := affineBlowUp.chart (I.ideal U) a ≫ ι U [TSPA, Tag 0804]; [Hau14, Theorem 4.19]: open immersions, lying over Spec (Γ(X, U) → Γ(X, U)[I(U)/a]) followed by Spec Γ(X, U) ≅ U ⊆ X, covering π⁻¹(U) as a runs through I(U), and with the chart of b cut out of the chart of a by the basic open D(b/a) (from the affine statements of Hironaka.Scheme.BlowUp.AffineBlowUp.Chart and the local description blowUpOf.isPullback);
• properness of blowUpOf.π I h for X locally Noetherian [TSPA, Tag 02NS]: IsProper is Zariski-local on the target, over each affine open U the blow-up map restricts to affineBlowUp.π (I.ideal U) up to the isomorphisms of the local description, and I(U) is finitely generated because Γ(X, U) is Noetherian (affineBlowUp.isProper_π).

The membership criterion of the charts is in Hironaka.Scheme.BlowUp.Glue.GlobalCharts, transported from the affine criterion of the universal property.

instance AlgebraicGeometry.blowUpOf.isOpenImmersion_ι {X : Scheme} (I : X.IdealSheafData) (h : CategoryTheory.NatTrans.Equifibered (affineBlowUpNatTrans I)) (U : ↑X.affineOpens) : IsOpenImmersion (ι I h U)

The components of the gluing are open immersions: ι U is the base change of the open immersion U ⊆ X along π (the pullback square blowUpOf.isPullback).

theorem AlgebraicGeometry.blowUpOf.opensRange_ι {X : Scheme} (I : X.IdealSheafData) (h : CategoryTheory.NatTrans.Equifibered (affineBlowUpNatTrans I)) (U : ↑X.affineOpens) : Scheme.Hom.opensRange (ι I h U) = (TopologicalSpace.Opens.map (π I h).base).obj ↑U

The component ι U has image π⁻¹(U) [TSPA, Tag 0804] (Mathlib's toBase_preimage_eq_opensRange_ι).

noncomputable def AlgebraicGeometry.blowUpOf.chart {X : Scheme} (I : X.IdealSheafData) (h : CategoryTheory.NatTrans.Equifibered (affineBlowUpNatTrans I)) (U : ↑X.affineOpens) (a : ↥(I.ideal U)) : Spec ↧↥(affineBlowUpAlgebra (I.ideal U) ↑a) ⟶ blowUpOf I h

The global chart of a ∈ I(U), Spec Γ(X, U)[I(U)/a] ⟶ blowUpOf I h: the affine chart of affineBlowUp (I.ideal U) followed by the component ι U [TSPA, Tag 0804]; [Hau14, Theorem 4.19].

Equations

• AlgebraicGeometry.blowUpOf.chart I h U a = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.affineBlowUp.chart (I.ideal U) a) (AlgebraicGeometry.blowUpOf.ι I h U)

instance AlgebraicGeometry.blowUpOf.isOpenImmersion_chart {X : Scheme} (I : X.IdealSheafData) (h : CategoryTheory.NatTrans.Equifibered (affineBlowUpNatTrans I)) (U : ↑X.affineOpens) (a : ↥(I.ideal U)) : IsOpenImmersion (chart I h U a)

The global charts are open immersions (composites of open immersions).

theorem AlgebraicGeometry.blowUpOf.chart_π {X : Scheme} (I : X.IdealSheafData) (h : CategoryTheory.NatTrans.Equifibered (affineBlowUpNatTrans I)) (U : ↑X.affineOpens) (a : ↥(I.ideal U)) : CategoryTheory.CategoryStruct.comp (chart I h U a) (π I h) = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (algebraMap ↑(X.presheaf.obj (Opposite.op ↑U)) ↥(affineBlowUpAlgebra (I.ideal U) ↑a)))) (CategoryTheory.CategoryStruct.comp ⋯.isoSpec.inv (↑U).ι)

Over the base, the global chart of a is Spec (Γ(X, U) → Γ(X, U)[I(U)/a]) followed by Spec Γ(X, U) ≅ U ⊆ X [Hau14, Theorem 4.19] (from affineBlowUp.chart_π and ι_toBase).

theorem AlgebraicGeometry.blowUpOf.iSup_opensRange_chart {X : Scheme} (I : X.IdealSheafData) (h : CategoryTheory.NatTrans.Equifibered (affineBlowUpNatTrans I)) (U : ↑X.affineOpens) : ⨆ (a : ↥(I.ideal U)), Scheme.Hom.opensRange (chart I h U a) = (TopologicalSpace.Opens.map (π I h).base).obj ↑U

The global charts of U cover π⁻¹(U) [TSPA, Tag 0804] (from affineBlowUp.iSup_opensRange_chart and blowUpOf.opensRange_ι).

theorem AlgebraicGeometry.blowUpOf.chart_preimage_chart {X : Scheme} (I : X.IdealSheafData) (h : CategoryTheory.NatTrans.Equifibered (affineBlowUpNatTrans I)) (U : ↑X.affineOpens) (a b : ↥(I.ideal U)) : (TopologicalSpace.Opens.map (chart I h U a).base).obj (Scheme.Hom.opensRange (chart I h U b)) = PrimeSpectrum.basicOpen (affineBlowUpAlgebra.ratio (I.ideal U) a b)

Chart overlaps (from affineBlowUp.chart_preimage_chart): inside the global chart of a the chart of b is the basic open D(b/a).

theorem AlgebraicGeometry.blowUpOf.isProper_π {X : Scheme} (I : X.IdealSheafData) (h : CategoryTheory.NatTrans.Equifibered (affineBlowUpNatTrans I)) [IsLocallyNoetherian X] : IsProper (π I h)

For X locally Noetherian the blow-up map is proper [TSPA, Tag 02NS]. IsProper is Zariski-local on the target; over an affine open U the restriction of π is, up to the isomorphism π⁻¹(U) ≅ affineBlowUp (I.ideal U), the blow-up map affineBlowUp.π (I.ideal U) followed by Spec Γ(X, U) ≅ U, proper by affineBlowUp.isProper_π because I(U) is finitely generated (Γ(X, U) is Noetherian).