The blow-up of a scheme along an ideal sheaf: charts #
The interface of the gluing blowUpOf restated for the blow-up blowUp I of a scheme X along
an ideal sheaf I [TSPA, Tag 01OF]: its components
blowUp.ι I U : affineBlowUp (I.ideal U) ⟶ blowUp I, the pullback squares
π⁻¹(U) ≅ affineBlowUp (I.ideal U), its affine charts blowUp.chart I U a with their base maps,
covering and overlaps, and properness of the blow-up map IdealSheafData.blowUpπ I for locally
Noetherian X. The exceptional ideal I·𝒪_B = I.comap (blowUpπ I), the ideal sheaf of the
exceptional divisor π⁻¹(Z), is IdealSheafData.exceptionalDivisor I (BlowUp/Defs.lean).
The component affineBlowUp (I.ideal U) ⟶ blowUp I of the gluing, an open immersion with
image π⁻¹(U).
Equations
Instances For
The global chart of a ∈ I(U), Spec Γ(X, U)[I(U)/a] ⟶ blowUp I [TSPA, Tag 0804];
[Hau14, Theorem 4.19].
Equations
Instances For
Over the base, the component ι U is affineBlowUp.π followed by Spec Γ(X, U) ≅ U ⊆ X
[TSPA, Tag 01LH].
Over every affine open U, π⁻¹(U) ≅ affineBlowUp (I.ideal U) as a pullback square
[TSPA, Tag 0804].
The component ι U has image π⁻¹(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].
The global charts of U cover π⁻¹(U) [TSPA, Tag 0804].
Chart overlaps: inside the global chart of a the chart of b is D(b/a).
For X locally Noetherian the blow-up map is proper [TSPA, Tag 02NS].