The blow-up of a smooth center in a smooth scheme is smooth

k a perfect field, f : X ⟶ Spec k smooth of relative dimension n, Z an ideal sheaf whose closed subscheme V(Z) is smooth over k of relative dimension n − r (r ≤ n). Kollár's "if π_{Z,X} is a smooth blow-up, then … B_Z X [is] smooth" [Kol07, Notation 19], proved here in the form B_Z X → Spec k is smooth of relative dimension n (smoothOfRelativeDimension_blowUpπ_comp).

The argument. Smoothness of relative dimension n is Zariski-local on the source (IsZariskiLocalAtSource.of_iSup_eq_top); B_Z X is covered by π⁻¹(U) for the charts U of étale coordinates adapted to Z at the closed points of V(Z) (EtaleCoordinatesAdapted), where π⁻¹(U) ≅ B_{Z∩U} U (blowUp.restrictIso) is smooth by the chart computation of Hironaka/Scheme/Smooth/BlowUpSmoothChart.lean, and by π⁻¹(X ∖ V(Z)), where π is an isomorphism (isIso_π_restrict_compl_support). These opens cover X because X is a Jacobson space (locally of finite type over a field, LocallyOfFiniteType.jacobsonSpace): the complement of their union is a closed subset of X without closed points, hence empty (nonempty_inter_closedPoints, iSup_eq_top_of_forall_isClosed). Forgetting the relative dimension, B_Z X is smooth over k (smooth_blowUpπ_comp). Every morphism out of an empty scheme is smooth (smooth_of_isEmpty), as for the empty center Z = ∅ of [Kol07, Warning 20].

This is the step that keeps the ambient scheme smooth along a sequence of smooth blow-ups (Hironaka/Scheme/BlowUpSequence/Basic.lean, Hironaka/Scheme/BlowUpSequence/SmoothCenter.lean).

theorem AlgebraicGeometry.smoothOfRelativeDimension_restrict_compl_support {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (Z : X.IdealSheafData) : SmoothOfRelativeDimension n (CategoryTheory.CategoryStruct.comp (Z.blowUpπ ∣_ Z.support.compl) (CategoryTheory.CategoryStruct.comp (Scheme.Opens.ι Z.support.compl) f))

Over the complement of the center the blow-up is an isomorphism (isIso_π_restrict_compl_support), so π ≫ f restricted there is smooth of relative dimension n when f is.

theorem AlgebraicGeometry.smoothOfRelativeDimension_restrict_of_etaleCoordinates {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) : SmoothOfRelativeDimension n (CategoryTheory.CategoryStruct.comp (Z.blowUpπ ∣_ ↑E.U) (CategoryTheory.CategoryStruct.comp (↑E.U).ι f))

Over a chart U of étale coordinates adapted to Z, π⁻¹(U) ≅ B_{Z∩U} U (preimageToRestrict) is smooth of relative dimension n over k (smoothOfRelativeDimension_blowUpπ_comap).

theorem AlgebraicGeometry.iSup_eq_top_of_forall_isClosed {X : Scheme} [JacobsonSpace ↥X] (Z : X.IdealSheafData) (U : { x : ↥X // IsClosed {x} ∧ x ∈ Z.support } → X.Opens) (hU : ∀ (x : { x : ↥X // IsClosed {x} ∧ x ∈ Z.support }), ↑x ∈ U x) : (⨆ (x : { x : ↥X // IsClosed {x} ∧ x ∈ Z.support }), U x) ⊔ Z.support.compl = ⊤

Opens U x ∋ x given at every closed point x of V(Z), together with the complement of V(Z), cover the Jacobson space X: the complement of their union is a closed set without closed points, hence empty.

theorem AlgebraicGeometry.smooth_of_isEmpty {X Y : Scheme} [IsEmpty ↥Y] (g : Y ⟶ X) : Smooth g

Every morphism out of an empty scheme is smooth (the empty open cover).

theorem AlgebraicGeometry.smoothOfRelativeDimension_blowUpπ_comp {k : Type u} [Field k] {X : Scheme} [PerfectField k] (f : X ⟶ Spec ↧k) (n r : ℕ) [SmoothOfRelativeDimension n f] (Z : X.IdealSheafData) [SmoothOfRelativeDimension (n - r) (CategoryTheory.CategoryStruct.comp Z.subschemeι f)] (hrn : r ≤ n) : SmoothOfRelativeDimension n (CategoryTheory.CategoryStruct.comp Z.blowUpπ f)

The blow-up of a smooth center in a smooth scheme is smooth [Kol07, Notation 19]: for X smooth over the perfect field k of relative dimension n and V(Z) smooth of relative dimension n − r, B_Z X → Spec k is smooth of relative dimension n. Glued from the chart computation over the charts of adapted étale coordinates at the closed points of V(Z) and the complement of V(Z), which cover X because X is Jacobson.

theorem AlgebraicGeometry.smooth_blowUpπ_comp {k : Type u} [Field k] {X : Scheme} [PerfectField k] (f : X ⟶ Spec ↧k) (n r : ℕ) [SmoothOfRelativeDimension n f] (Z : X.IdealSheafData) [SmoothOfRelativeDimension (n - r) (CategoryTheory.CategoryStruct.comp Z.subschemeι f)] (hrn : r ≤ n) : Smooth (CategoryTheory.CategoryStruct.comp Z.blowUpπ f)

In Kollár's words [Kol07, Notation 19]: B_Z X is smooth over k.