The affine blow-ups over the affine opens of a scheme, and their gluing

The blow-up of a scheme X along an ideal sheaf I is Proj_X (⨁ₙ Iⁿ), obtained by gluing the affine blow-ups Proj Rees(I(U)) over the affine opens U of X along the canonical isomorphisms π⁻¹(U) ≅ Proj Rees(I(U)) [TSPA, Tags 01OF and 0804]; the relative gluing lemma [TSPA, Tag 01LH] performs this from the functor affineBlowUpFunctor I : U ↦ affineBlowUp (I.ideal U) on the affine opens, the natural transformation affineBlowUpNatTrans I to the directed cover's diagram X.directedAffineCover.functorOfLocallyDirected, and a proof h that its naturality squares are pullbacks; the result is blowUpOf I h over X. This module supplies the rest of the construction.

• affineBlowUpFunctor_obj, affineBlowUpFunctor_map, affineBlowUpNatTrans_app: the functor and the components affineBlowUp.π ≫ U.isoSpec.inv : affineBlowUp (I.ideal U) ⟶ U, unfolded.
• Every naturality square is a pullback ((affineBlowUpNatTrans I).Equifibered, the hypothesis of the relative gluing lemma; [Hau14, Corollary 5.2 (b)]): equifibered_of_isPullback I H derives it from the open-restriction square H of the universal property of the affine blow-up (affineBlowUp.isPullback_mapHom of Hironaka.Scheme.BlowUp.AffineBlowUp.Universal.Restrict), pasted with the square of isomorphisms Spec Γ(X, U) ≅ U ⊆ V ≅ Spec Γ(X, V).
• For an arbitrary proof h of the pullback squares: the components blowUpOf.ι I h U of the gluing, and Mathlib's pullback squares blowUpOf.isPullback I h U — π⁻¹(U) ≅ affineBlowUp (I.ideal U) over U [TSPA, Tag 0804]. The blow-up itself, AlgebraicGeometry.Scheme.IdealSheafData.blowUp I, is blowUpOf I at the proof from the universal property.
• The side condition Quiver.IsThin X.affineOpens of the gluing (a preorder category), supplied here as fun _ _ => inferInstance.

instance AlgebraicGeometry.instIsThinElemOpensAffineOpens_hironaka {X : Scheme} : Quiver.IsThin ↑X.affineOpens

Morphisms of the preorder category X.affineOpens form a subsingleton (they are ULift (PLift (U ≤ V))); Mathlib has no Quiver.IsThin instance for preorder categories.

@[simp]

theorem AlgebraicGeometry.affineBlowUpFunctor_obj {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : (affineBlowUpFunctor I).obj U = affineBlowUp (I.ideal U)

theorem AlgebraicGeometry.affineBlowUpFunctor_map {X : Scheme} (I : X.IdealSheafData) {U V : ↑X.affineOpens} (h : U ⟶ V) : (affineBlowUpFunctor I).map h = affineBlowUp.mapHom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op) ⋯

@[simp]

theorem AlgebraicGeometry.affineBlowUpNatTrans_app {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : (affineBlowUpNatTrans I).app U = CategoryTheory.CategoryStruct.comp (affineBlowUp.π (I.ideal U)) ⋯.isoSpec.inv

theorem AlgebraicGeometry.specMap_presheaf_map_isoSpec_inv {X : Scheme} {U V : ↑X.affineOpens} (hle : U ≤ V) : CategoryTheory.CategoryStruct.comp (Spec.map (X.presheaf.map (CategoryTheory.homOfLE hle).op)) ⋯.isoSpec.inv = CategoryTheory.CategoryStruct.comp ⋯.isoSpec.inv (X.homOfLE ⋯)

For affine opens U ≤ V, Spec of the restriction Γ(X, V) → Γ(X, U) is Spec Γ(X, U) ≅ U ⊆ V ≅ Spec Γ(X, V) (Mathlib's Scheme.Opens.toSpecΓ_SpecMap_presheaf_map read through IsAffineOpen.isoSpec).

theorem AlgebraicGeometry.specMap_presheaf_map_eq {X : Scheme} {U V : ↑X.affineOpens} (hle : U ≤ V) : Spec.map (X.presheaf.map (CategoryTheory.homOfLE hle).op) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ⋯.isoSpec.inv (X.homOfLE ⋯)) ⋯.isoSpec.hom

instance AlgebraicGeometry.isOpenImmersion_specMap_presheaf_map {X : Scheme} {U V : ↑X.affineOpens} (hle : U ≤ V) : IsOpenImmersion (Spec.map (X.presheaf.map (CategoryTheory.homOfLE hle).op))

For affine opens U ≤ V of X, Spec Γ(X, U) → Spec Γ(X, V) is an open immersion (it is the inclusion U ⊆ V up to the isomorphisms isoSpec): the hypothesis under which the open-restriction square affineBlowUp.isPullback_mapHom applies to the restriction maps of the structure sheaf.

theorem AlgebraicGeometry.equifibered_of_isPullback {X : Scheme} (I : X.IdealSheafData) (H : ∀ {R S : CommRingCat} (φ : R ⟶ S) [IsOpenImmersion (Spec.map φ)] {I : Ideal ↑R} {J : Ideal ↑S} (hJ : Ideal.map (CommRingCat.Hom.hom φ) I = J), CategoryTheory.IsPullback (affineBlowUp.mapHom φ hJ) (affineBlowUp.π J) (affineBlowUp.π I) (Spec.map φ)) : CategoryTheory.NatTrans.Equifibered (affineBlowUpNatTrans I)

Given the open-restriction square H of the universal property for every ring map φ with Spec.map φ an open immersion, every naturality square of affineBlowUpNatTrans I is a pullback — the hypothesis of the relative gluing lemma [TSPA, Tag 01LH]; [Hau14, Corollary 5.2 (b)]. Proof: the square H for the restriction Γ(X, V) → Γ(X, U) (an open immersion on Spec by isOpenImmersion_specMap_presheaf_map), pasted vertically with the commutative square of isomorphisms Spec Γ(X, U) ≅ U, Spec Γ(X, V) ≅ V over U ⊆ V (a pullback because its vertical sides are isomorphisms).

noncomputable def AlgebraicGeometry.blowUpOf.ι {X : Scheme} (I : X.IdealSheafData) (h : CategoryTheory.NatTrans.Equifibered (affineBlowUpNatTrans I)) (U : ↑X.affineOpens) : affineBlowUp (I.ideal U) ⟶ blowUpOf I h

The component affineBlowUp (I.ideal U) ⟶ blowUpOf I h of the gluing, an open immersion.

Equations

• AlgebraicGeometry.blowUpOf.ι I h U = CategoryTheory.Limits.colimit.ι (AlgebraicGeometry.relativeGluingDataOf I h).functor U

theorem AlgebraicGeometry.blowUpOf.ι_π {X : Scheme} (I : X.IdealSheafData) (h : CategoryTheory.NatTrans.Equifibered (affineBlowUpNatTrans I)) (U : ↑X.affineOpens) : CategoryTheory.CategoryStruct.comp (ι I h U) (π I h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (affineBlowUp.π (I.ideal U)) ⋯.isoSpec.inv) (↑U).ι

Over the base, the component ι U is affineBlowUp.π followed by U ≅ Spec Γ(X, U) and the inclusion of U [TSPA, Tag 01LH].

theorem AlgebraicGeometry.blowUpOf.isPullback {X : Scheme} (I : X.IdealSheafData) (h : CategoryTheory.NatTrans.Equifibered (affineBlowUpNatTrans I)) (U : ↑X.affineOpens) : CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.comp (affineBlowUp.π (I.ideal U)) ⋯.isoSpec.inv) (ι I h U) (↑U).ι (π I h)

The local description of the blow-up [TSPA, Tag 0804]: over each affine open U, π⁻¹(U) ≅ affineBlowUp (I.ideal U), as Mathlib's pullback square isPullback_natTrans_ι_toBase.