The blow-up of a chart of étale coordinates

k a field, f : X ⟶ Spec k, E a chart of étale coordinates at x adapted to Z (EtaleCoordinatesAdapted): an affine open U ∋ x, sections v with g = toAffineSpace f U v : U ⟶ 𝔸ⁿ_k étale and Z ∩ U = g⁻¹(L), L = coordinateSubspace k n r. Three statements about B_{Z∩U} U:

• B_{Z∩U} U is the fibre product U ×_{𝔸ⁿ} B_L 𝔸ⁿ (exists_isPullback_blowUp): the flat base-change square isPullback_blowUpMap for the étale (hence flat) g, read along Z ∩ U = g⁻¹(L). A blow-up commutes with flat base change [TSPA, Tag 0805]; in general the blow-up of Y along φ⁻¹(Z) is the closure of p⁻¹(Y ∖ φ⁻¹(Z)) in the fibre product [Hau14, Proposition 5.1].
• The projection φ : B_{Z∩U} U ⟶ B_L 𝔸ⁿ is étale, as a base change of g (etale_of_isPullback_blowUp; Mathlib's IsStableUnderBaseChange for Etale).
• B_{Z∩U} U → Spec k is smooth of relative dimension n, the composite of the étale φ with B_L 𝔸ⁿ → 𝔸ⁿ → Spec k (smoothOfRelativeDimension_blowUpπ_comap). The last morphism is the smoothness of the affine model modelBlowUp k n r (smoothOfRelativeDimension_modelBlowUp), transported to the glued blowUp (coordinateSubspace k n r) by the uniqueness of the blow-up (IsBlowUp.exists_iso): coordinateSubspace k n r is by definition specIdealSheaf (centerIdeal k n r), and the affine model is a blow-up in the sense of the universal property (affineBlowUp.isBlowUp). The structure morphism of the chart is g ≫ (𝔸ⁿ → Spec k) = U.ι ≫ f (toAffineSpace_comp_structure).

This is the chart computation from which Hironaka/Scheme/Smooth/BlowUpSmooth.lean glues the smoothness of B_Z X: Kollár's "B_Z X is smooth" for a smooth blow-up [Kol07, Notation 19] read on one chart, whose coordinates are those of [Hau14, Proposition 5.4].

theorem AlgebraicGeometry.affineBlowUp.isBlowUp {R : Type u} [CommRing R] (I : Ideal R) : IsBlowUp (specIdealSheaf I) (π I)

The affine blow-up affineBlowUp I of Spec R along I is a blow-up in the sense of the universal property ([Hau14, Definition 4.4]; the predicate IsBlowUp): the exceptional ideal is invertible, and every morphism making I invertible lifts uniquely.

theorem AlgebraicGeometry.exists_iso_blowUp_coordinateSubspace (k : Type u) [Field k] (n r : ℕ) : ∃ (e : (coordinateSubspace k n r).blowUp ≅ CoordinateSubspace.modelBlowUp k n r), CategoryTheory.CategoryStruct.comp e.hom (affineBlowUp.π (CoordinateSubspace.centerIdeal k n r)) = (coordinateSubspace k n r).blowUpπ

The glued blow-up blowUp (coordinateSubspace k n r) of 𝔸ⁿ_k along L and the affine model modelBlowUp k n r are isomorphic over 𝔸ⁿ_k, by the uniqueness of the blow-up.

theorem AlgebraicGeometry.smoothOfRelativeDimension_blowUpπ_coordinateSubspace (k : Type u) [Field k] (n r : ℕ) : SmoothOfRelativeDimension n (CategoryTheory.CategoryStruct.comp (coordinateSubspace k n r).blowUpπ (Spec.map (CommRingCat.ofHom (algebraMap k (MvPolynomial (Fin n) k)))))

B_L 𝔸ⁿ_k → Spec k is smooth of relative dimension n, for the glued blow-up along the coordinate subspace L (transported from the affine model).

theorem AlgebraicGeometry.ofHom_algebraMap_comp_aeval {k : Type u} [Field k] {A : Type u} [CommRing A] [Algebra k A] {n : ℕ} (v : Fin n → A) : CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap k (MvPolynomial (Fin n) k))) (CommRingCat.ofHom (MvPolynomial.aeval v).toRingHom) = CommRingCat.ofHom (algebraMap k A)

k → k[t] → A, t_i ↦ v_i, is the structure map of the k-algebra A.

theorem AlgebraicGeometry.toAffineSpace_comp_structure {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) {n : ℕ} (U : X.Opens) (v : Fin n → ↑(X.presheaf.obj (Opposite.op U))) : CategoryTheory.CategoryStruct.comp (toAffineSpace f U v) (Spec.map (CommRingCat.ofHom (algebraMap k (MvPolynomial (Fin n) k)))) = CategoryTheory.CategoryStruct.comp U.ι f

The coordinate morphism is a morphism over k: g ≫ (𝔸ⁿ_k → Spec k) = U.ι ≫ f.

theorem AlgebraicGeometry.exists_isPullback_blowUp {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) : ∃ (φ : (Z.comap (↑E.U).ι).blowUp ⟶ (coordinateSubspace k n r).blowUp), CategoryTheory.IsPullback φ (Z.comap (↑E.U).ι).blowUpπ (coordinateSubspace k n r).blowUpπ (toAffineSpace f (↑E.U) E.v)

For a chart E of étale coordinates adapted to Z, B_{Z∩U} U is the fibre product U ×_{𝔸ⁿ} B_L 𝔸ⁿ: a blow-up commutes with flat base change ([TSPA, Tag 0805]; cf. [Hau14, Proposition 5.1]).

theorem AlgebraicGeometry.etale_of_isPullback_blowUp {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) {φ : (Z.comap (↑E.U).ι).blowUp ⟶ (coordinateSubspace k n r).blowUp} (H : CategoryTheory.IsPullback φ (Z.comap (↑E.U).ι).blowUpπ (coordinateSubspace k n r).blowUpπ (toAffineSpace f (↑E.U) E.v)) : Etale φ

The projection φ : B_{Z∩U} U ⟶ B_L 𝔸ⁿ of any cartesian square as in exists_isPullback_blowUp is étale, being the base change of the étale g along π_L.

theorem AlgebraicGeometry.smoothOfRelativeDimension_blowUpπ_comap {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.comap (↑E.U).ι).blowUpπ (CategoryTheory.CategoryStruct.comp (↑E.U).ι f))

B_{Z∩U} U → Spec k is smooth of relative dimension n: the composite of the étale φ with B_L 𝔸ⁿ → 𝔸ⁿ → Spec k (the chart form of "B_Z X is smooth", [Kol07, Notation 19]).