The exceptional divisor is locally (Z ∩ U) ×_k ℙ^{r-1}_k

Over a chart E of étale coordinates adapted to Z, the exceptional divisor F_U of B_{Z∩U} U is isomorphic over Z ∩ U to (Z ∩ U) ×_k ℙ^{r-1}_k (exists_iso_exceptional_pullback_proj), and the fibre of F → Z over a point z of the center is ℙ^{r-1}_{κ(z)} (exists_iso_fiber_proj): the exceptional divisor of a smooth blow-up, smooth by [Kol07, Notation 19], is a projective bundle over the center (the description of the blow-up of affine space by secant lines, [Hau14, Definition 4.8]).

Why it holds. Three cartesian squares are pasted. (1) The chart square of Hironaka/Scheme/Smooth/ExceptionalChart.lean: F_U → Z ∩ U is the base change of the model's F_L → L along Z ∩ U → L (isPullback_exceptionalMapOfIsPullback_subschemeMap). (2) The model (Hironaka/Scheme/BlowUp/CoordinateSubspace/ExceptionalProj.lean): F_L ≅ ℙ^{r-1}_L = Proj 𝒪(L)[u] compatibly with the structure maps to L = Spec 𝒪(L) (exists_iso_exceptional_proj, for the model blow-up; transported to the glued blow-up of 𝔸ⁿ along L through the identification of the two blow-ups, comap_π_coordinateSubspace_eq). (3) The base change of projective space (AlgebraicGeometry.Proj.isPullback_projMap): ℙ^{r-1}_L = L ×_k ℙ^{r-1}_k. Pasting (2)–(3) gives F_L → L as the base change of ℙ^{r-1}_k → Spec k along L → Spec k, and pasting (1) on top gives F_U → Z ∩ U as the base change of ℙ^{r-1}_k → Spec k along Z ∩ U → L → Spec k = Z ∩ U → U → Spec k (toAffineSpace_comp_structure).

Main declarations

• AlgebraicGeometry.exists_iso_exceptional_coordinateSubspace_proj: F_L ≅ Proj 𝒪(L)[u] for the glued blow-up of 𝔸ⁿ_k along L, over L ≅ Spec 𝒪(L).
• AlgebraicGeometry.isPullback_exceptional_coordinateSubspace_proj: F_L → L is the base change of ℙ^{r-1}_k → Spec k.
• AlgebraicGeometry.exists_isPullback_exceptional_proj, exists_iso_exceptional_pullback_proj: F_U → Z ∩ U is the base change of ℙ^{r-1}_k → Spec k, and the isomorphism F_U ≅ (Z ∩ U) ×_k ℙ^{r-1}_k over Z ∩ U.
• AlgebraicGeometry.exists_iso_fiber_proj: the fibre of F → Z over z is ℙ^{r-1}_{κ(z)}, compatibly with the structure morphisms to Spec κ(z). A point z of the center lies in some chart U at a closed point (the Jacobson cover, as for exceptionalDivisorCover in ExceptionalDivisor.lean); the fibre of F → Z at z is the fibre of F_U → Z ∩ U at the point z' of Z ∩ U over z (Mathlib's isPullback_fiberToSpecResidueField_of_isPullback for the square F_U = F ×_Z (Z ∩ U), the residue fields agreeing along the open immersion); that fibre is Spec κ(z) ×_k ℙ^{r-1}_k by pasting the fibre square onto the chart square, and Spec κ(z) ×_k ℙ^{r-1}_k = ℙ^{r-1}_{κ(z)} is the base change of projective space along k → κ(z).

theorem AlgebraicGeometry.eqToHom_subschemeι {X : Scheme} {I J : X.IdealSheafData} (h : I = J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) J.subschemeι = I.subschemeι

The closed subscheme of an ideal sheaf is transported along an equality of ideal sheaves; the reassoc attribute gives the composed form.

theorem AlgebraicGeometry.eqToHom_subschemeι_assoc {X : Scheme} {I J : X.IdealSheafData} (h : I = J) {Z : Scheme} (h✝ : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp J.subschemeι h✝) = CategoryTheory.CategoryStruct.comp I.subschemeι h✝

The closed subscheme of an ideal sheaf is transported along an equality of ideal sheaves; the reassoc attribute gives the composed form.

noncomputable def AlgebraicGeometry.coordinateSubspaceIsoSpec (k : Type u) [Field k] (n r : ℕ) : (coordinateSubspace k n r).subscheme ≅ Spec ↧(MvPolynomial (Fin n) k ⧸ CoordinateSubspace.centerIdeal k n r)

L = V(t_0, …, t_{r-1}) ≅ Spec (k[t]/(t_0, …, t_{r-1})) (the inverse of specQuotientToSubscheme).

Equations

• AlgebraicGeometry.coordinateSubspaceIsoSpec k n r = (CategoryTheory.asIso (AlgebraicGeometry.specQuotientToSubscheme (AlgebraicGeometry.CoordinateSubspace.centerIdeal k n r))).symm

theorem AlgebraicGeometry.coordinateSubspaceIsoSpec_hom_SpecMap (k : Type u) [Field k] (n r : ℕ) : CategoryTheory.CategoryStruct.comp (coordinateSubspaceIsoSpec k n r).hom (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (CoordinateSubspace.centerIdeal k n r)))) = (coordinateSubspace k n r).subschemeι

theorem AlgebraicGeometry.coordinateSubspaceIsoSpec_hom_SpecMap_assoc (k : Type u) [Field k] (n r : ℕ) {Z : Scheme} (h : Spec ↧(MvPolynomial (Fin n) k) ⟶ Z) : CategoryTheory.CategoryStruct.comp (coordinateSubspaceIsoSpec k n r).hom (CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (CoordinateSubspace.centerIdeal k n r)))) h) = CategoryTheory.CategoryStruct.comp (coordinateSubspace k n r).subschemeι h

theorem AlgebraicGeometry.exists_iso_exceptional_coordinateSubspace_proj (k : Type u) [Field k] (n r : ℕ) (hrn : r ≤ n) : ∃ (e : ((coordinateSubspace k n r).comap (coordinateSubspace k n r).blowUpπ).subscheme ≅ Proj (MvPolynomial.homogeneousSubmodule (Fin r) (MvPolynomial (Fin n) k ⧸ CoordinateSubspace.centerIdeal k n r))), CategoryTheory.CategoryStruct.comp e.hom (Proj.projToSpec (Fin r) (MvPolynomial (Fin n) k ⧸ CoordinateSubspace.centerIdeal k n r)) = CategoryTheory.CategoryStruct.comp (((coordinateSubspace k n r).comap (coordinateSubspace k n r).blowUpπ).subschemeMap (coordinateSubspace k n r) (coordinateSubspace k n r).blowUpπ ⋯) (coordinateSubspaceIsoSpec k n r).hom

The exceptional divisor F_L of the glued blow-up B_L 𝔸ⁿ_k is ℙ^{r-1}_L = Proj 𝒪(L)[u_0, …, u_{r-1}], compatibly with the structure maps to L ≅ Spec 𝒪(L) (the computation for the model blow-up, transported along the identification of the two blow-ups).

theorem AlgebraicGeometry.isPullback_exceptional_coordinateSubspace_proj (k : Type u) [Field k] (n r : ℕ) (hrn : r ≤ n) : ∃ (q : ((coordinateSubspace k n r).comap (coordinateSubspace k n r).blowUpπ).subscheme ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin r) k)), CategoryTheory.IsPullback (((coordinateSubspace k n r).comap (coordinateSubspace k n r).blowUpπ).subschemeMap (coordinateSubspace k n r) (coordinateSubspace k n r).blowUpπ ⋯) q (CategoryTheory.CategoryStruct.comp (coordinateSubspace k n r).subschemeι (Spec.map (CommRingCat.ofHom (algebraMap k (MvPolynomial (Fin n) k))))) (Proj.projToSpec (Fin r) k)

F_L → L is the base change of ℙ^{r-1}_k → Spec k along L → 𝔸ⁿ_k → Spec k.

theorem AlgebraicGeometry.exists_isPullback_exceptional_proj {k : Type u} [Field k] {X : Scheme} {f : X ⟶ Spec ↧k} {n r : ℕ} {Z : X.IdealSheafData} {x : ↥X} (E : EtaleCoordinatesAdapted f n r Z x) (hrn : r ≤ n) : ∃ (q : ((Z.comap (↑E.U).ι).comap (Z.comap (↑E.U).ι).blowUpπ).subscheme ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin r) k)), CategoryTheory.IsPullback (((Z.comap (↑E.U).ι).comap (Z.comap (↑E.U).ι).blowUpπ).subschemeMap (Z.comap (↑E.U).ι) (Z.comap (↑E.U).ι).blowUpπ ⋯) q (CategoryTheory.CategoryStruct.comp (Z.comap (↑E.U).ι).subschemeι (CategoryTheory.CategoryStruct.comp (↑E.U).ι f)) (Proj.projToSpec (Fin r) k)

Over a chart E, F_U → Z ∩ U is the base change of ℙ^{r-1}_k → Spec k along the structure morphism Z ∩ U → U → Spec k.

theorem AlgebraicGeometry.exists_iso_exceptional_pullback_proj {k : Type u} [Field k] {X : Scheme} {f : X ⟶ Spec ↧k} {n r : ℕ} {Z : X.IdealSheafData} {x : ↥X} (E : EtaleCoordinatesAdapted f n r Z x) (hrn : r ≤ n) : ∃ (e : ((Z.comap (↑E.U).ι).comap (Z.comap (↑E.U).ι).blowUpπ).subscheme ≅ CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (Z.comap (↑E.U).ι).subschemeι (CategoryTheory.CategoryStruct.comp (↑E.U).ι f)) (Proj.projToSpec (Fin r) k)), CategoryTheory.CategoryStruct.comp e.hom (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (Z.comap (↑E.U).ι).subschemeι (CategoryTheory.CategoryStruct.comp (↑E.U).ι f)) (Proj.projToSpec (Fin r) k)) = ((Z.comap (↑E.U).ι).comap (Z.comap (↑E.U).ι).blowUpπ).subschemeMap (Z.comap (↑E.U).ι) (Z.comap (↑E.U).ι).blowUpπ ⋯

Over a chart E of étale coordinates adapted to Z, the exceptional divisor F_U of B_{Z∩U} U is isomorphic over Z ∩ U to (Z ∩ U) ×_k ℙ^{r-1}_k (cf. [Hau14, Definition 4.8], the blow-up of affine space by secant lines).

theorem AlgebraicGeometry.isPullback_restrictHom {X : Scheme} (Z : X.IdealSheafData) (U : X.Opens) : CategoryTheory.IsPullback (Z.comap U.ι).blowUpπ (Scheme.Hom.blowUpMap U.ι Z) U.ι Z.blowUpπ

B_{Z∩U} U → B_Z X is the base change of U → X (the restriction of a blow-up to an open, as a cartesian square).

theorem AlgebraicGeometry.isPullback_exceptionalRestrictPiece_subschemeMap {X : Scheme} (Z : X.IdealSheafData) (U : X.Opens) : CategoryTheory.IsPullback (exceptionalRestrictPiece Z U) (((Z.comap U.ι).comap (Z.comap U.ι).blowUpπ).subschemeMap (Z.comap U.ι) (Z.comap U.ι).blowUpπ ⋯) ((Z.comap Z.blowUpπ).subschemeMap Z Z.blowUpπ ⋯) ((Z.comap U.ι).subschemeMap Z U.ι ⋯)

The piece F_U → F over the piece Z ∩ U → Z: the square F_U → F, F_U → Z ∩ U, F → Z, Z ∩ U → Z is cartesian (F_U = F ×_Z (Z ∩ U)).

theorem AlgebraicGeometry.exists_adaptedChart_mem {k : Type u} [Field k] [PerfectField k] {X : Scheme} (f : X ⟶ Spec ↧k) (n r : ℕ) [SmoothOfRelativeDimension n f] (Z : X.IdealSheafData) [SmoothOfRelativeDimension (n - r) (CategoryTheory.CategoryStruct.comp Z.subschemeι f)] (hrn : r ≤ n) (z : ↥Z.subscheme) : ∃ (x : { x : ↥X // IsClosed {x} ∧ x ∈ Z.support }), Z.subschemeι z ∈ ↑(adaptedChart f n r Z hrn x).U

Every point of the center Z lies in an adapted chart at a closed point of V(Z) (the Jacobson cover, as for the pieces of F in Hironaka/Scheme/Smooth/ExceptionalDivisor.lean).

theorem AlgebraicGeometry.exists_subschemeMap_comap_ι_eq {X : Scheme} (Z : X.IdealSheafData) (U : X.Opens) (z : ↥Z.subscheme) (hz : Z.subschemeι z ∈ U) : ∃ (z' : ↥(Z.comap U.ι).subscheme), ((Z.comap U.ι).subschemeMap Z U.ι ⋯) z' = z

A point of Z lying in U is the image of a point of Z ∩ U.

theorem AlgebraicGeometry.exists_iso_fiber_proj {k : Type u} [Field k] [PerfectField k] {X : Scheme} (f : X ⟶ Spec ↧k) (n r : ℕ) [SmoothOfRelativeDimension n f] (Z : X.IdealSheafData) [SmoothOfRelativeDimension (n - r) (CategoryTheory.CategoryStruct.comp Z.subschemeι f)] (hrn : r ≤ n) (z : ↥Z.subscheme) : ∃ (e : Scheme.Hom.fiber ((Z.comap Z.blowUpπ).subschemeMap Z Z.blowUpπ ⋯) z ≅ Proj (MvPolynomial.homogeneousSubmodule (Fin r) ↑(Z.subscheme.residueField z))), CategoryTheory.CategoryStruct.comp e.hom (Proj.projToSpec (Fin r) ↑(Z.subscheme.residueField z)) = Scheme.Hom.fiberToSpecResidueField ((Z.comap Z.blowUpπ).subschemeMap Z Z.blowUpπ ⋯) z

For a smooth blow-up over the perfect field k and a point z of the center, the fibre of F → Z over z is ℙ^{r-1}_{κ(z)} = Proj κ(z)[u_0, …, u_{r-1}], compatibly with the structure morphisms to Spec κ(z).