The affine charts of the blow-up: covers, membership and overlaps as sets

The chart statements of Hironaka.Scheme.BlowUp.Glue.BlowUp with images and preimages as sets, together with two statements that rest on the universal property of the affine blow-up:

• the charts of any generating set of I(U) cover π⁻¹(U) — for generators g₁, …, g_k of I the blow-up is covered by the charts of the gᵢ [Hau14, Theorem 4.19] (from affineBlowUp.exists_mem_opensRange_chart_of_span_eq on the affine piece);
• the chart membership criterion for the blow-up [TSPA, Tag 0BFL]: a point x' over U lies in the chart of a ∈ I(U) iff the image of a in 𝒪_{B,x'} generates the stalk of the exceptional ideal — transported from the affine criterion (affineBlowUp.mem_chart_iff) along the open immersion ι U : affineBlowUp (I.ideal U) ⟶ B, whose stalk maps are isomorphisms, with the germ of a moved through Spec Γ(X, U) → X (IsAffineOpen.fromSpec_app_self).

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.iUnion_range_chart {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : ⋃ (a : ↥(I.ideal U)), Set.range ⇑(chart I U a) = ↑((TopologicalSpace.Opens.map I.blowUpπ.base).obj ↑U)

As sets: the charts of all a ∈ I(U) cover π⁻¹(U).

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.range_chart_subset {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) (a : ↥(I.ideal U)) : Set.range ⇑(chart I U a) ⊆ ↑((TopologicalSpace.Opens.map I.blowUpπ.base).obj ↑U)

Every chart of U lands in π⁻¹(U).

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.iUnion_range_chart_of_span_eq {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) (s : Set ↥(I.ideal U)) (hs : Ideal.span (Subtype.val '' s) = I.ideal U) : ⋃ a ∈ s, Set.range ⇑(chart I U a) = ↑((TopologicalSpace.Opens.map I.blowUpπ.base).obj ↑U)

The charts of any generating set of I(U) cover π⁻¹(U) [Hau14, Theorem 4.19].

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.preimage_range_chart {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) (a b : ↥(I.ideal U)) : ⇑(chart I U a) ⁻¹' Set.range ⇑(chart I U b) = ↑(PrimeSpectrum.basicOpen (affineBlowUpAlgebra.frac ⋯))

As sets: inside the chart of a the chart of b is D(b/a), with b/a the generator affineBlowUpAlgebra.frac.

theorem AlgebraicGeometry.fromSpec_stalkMap_germ {X : Scheme} (U : ↑X.affineOpens) (p : ↥(Spec (X.presheaf.obj (Opposite.op ↑U)))) (hp : ⋯.fromSpec p ∈ ↑U) (a : ↑(X.presheaf.obj (Opposite.op ↑U))) : (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap ⋯.fromSpec p)) ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (↑U) (⋯.fromSpec p) hp)) a) = (specGerm p) a

The stalk map of fromSpec : Spec Γ(X, U) ⟶ X sends the germ of a ∈ Γ(X, U) at fromSpec p to the germ of a read as a global section of Spec Γ(X, U) (fromSpec_app_self).

theorem AlgebraicGeometry.stalkMap_ι_stalkMap_π {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) (y : ↥(affineBlowUp (I.ideal U))) (hy : I.blowUpπ ((Scheme.IdealSheafData.blowUp.ι I U) y) ∈ ↑U) (a : ↑(X.presheaf.obj (Opposite.op ↑U))) : (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap (Scheme.IdealSheafData.blowUp.ι I U) y)) ((CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap I.blowUpπ ((Scheme.IdealSheafData.blowUp.ι I U) y))) ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (↑U) (I.blowUpπ ((Scheme.IdealSheafData.blowUp.ι I U) y)) hy)) a)) = (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap (affineBlowUp.π (I.ideal U)) y)) ((specGerm ((affineBlowUp.π (I.ideal U)) y)) a)

The image of a ∈ Γ(X, U) in 𝒪_{B, ι y}, transported to 𝒪_{affineBlowUp, y} along the stalk isomorphism of ι U, is the image of a under the affine blow-up map (the composite ι U ≫ π = affineBlowUp.π ≫ fromSpec).

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.mem_range_chart_iff {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) (a : ↥(I.ideal U)) (x' : ↥I.blowUp) (hx' : I.blowUpπ x' ∈ ↑U) : x' ∈ Set.range ⇑(chart I U a) ↔ I.exceptionalDivisor.stalkIdeal x' = Ideal.span {(CategoryTheory.ConcreteCategory.hom (Hom.stalkMap I.blowUpπ x')) ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (↑U) (I.blowUpπ x') hx')) ↑a)}

The chart membership criterion [TSPA, Tag 0BFL]: a point x' of the blow-up over U lies in the chart of a ∈ I(U) iff the image of a in 𝒪_{B,x'} generates the stalk of the exceptional ideal at x' (from the affine criterion affineBlowUp.mem_chart_iff along ι U).