The local blow-up as a base change #
Hauser defines the local blow-up of X along Z at x' ∈ π⁻¹(x) as the morphism of germs
(X', x') → (X, x) [Hau14, Definition 4.15], and as the localization R → R[Ig⁻¹]_𝔭 of a chart of
the blow-up of the local ring R = 𝒪_{X,x} [Hau14, Definition 4.16]. The two agree because the
blow-up of Spec 𝒪_{X,x} along the stalk I_x of Z is the base change of B_Z X along
Spec 𝒪_{X,x} → X (exists_isPullback_fromSpecStalk; blow-ups commute with flat base change,
[TSPA, Tag 0805], since X.fromSpecStalk x is flat, being a localization on an affine
neighbourhood (flat_fromSpecStalk), and the pullback of Z along it is the ideal sheaf of I_x
(comap_fromSpecStalk_eq_specIdealSheaf)). The file also relates the origin of the chart of x_ρ
of the local blow-up, chartOrigin of Hironaka/Algebra/Local/Chart.lean, to a point of B_Z X
over x whose stalk is the localization of the chart ring at the origin
(exists_stalk_equiv_localization_chartOrigin_of_isIso), granted that the stalks of the local
blow-up are those of B_Z X (proved in Hironaka/Scheme/Smooth/LocalBlowUpStalk.lean).
Used for the charts of the local blow-up (LocalBlowUpChart.lean) and for the order of an ideal
along the exceptional divisor (Hironaka/Scheme/IdealSheaf/Order/ExceptionalOrder.lean).
Spec 𝒪_{X,x} → X is flat: on an affine open U ∋ x it is Spec of the localization
Γ(X, U) → 𝒪_{X,x} followed by the open immersion Spec Γ(X, U) ≅ U ⊆ X.
The pullback of Z along Spec 𝒪_{X,x} → X is the ideal sheaf of the stalk I_x of Z.
The blow-up of Spec 𝒪_{X,x} along the stalk I_x of Z, the affine blow-up of the local
ring, is the base change of B_Z X along Spec 𝒪_{X,x} → X: the local blow-up as a morphism of
germs ([Hau14, Definition 4.15]; [TSPA, Tag 0805]).
Germs along a base change of Spec 𝒪_{X,x} → X: for g = ψ ≫ X.fromSpecStalk x, the stalk map
of g at q sends the germ of a section s at g q to ψ^♯ of the germ at ψ q of the
"constant" s_x ∈ 𝒪_{X,x} = Γ(Spec 𝒪_{X,x}, ⊤) (Mathlib's fromSpecStalk_app).
A point of Spec S lying over the maximal ideal of a local ring R is sent by Spec of
R → S to the closed point.
The ring-level data of the origin of the chart of x_ρ of the local blow-up: on the chart ring
R[I/x_ρ] = chartRing x ρ (affineBlowUpAlgebra_span_eq_chartRing), the origin
𝔪' = chartOrigin x ρ is a point of Spec R[I/x_ρ] lying over the closed point of Spec R
(comap_chartOrigin), and the localization of R[I/x_ρ] at it is R'_{𝔪'}, compatibly with the
maps from R.
Granted that the stalks of the local blow-up are those of B_Z X (the hypothesis hiso, proved
in LocalBlowUpStalk.lean): the origin of the chart of y_ρ of the local blow-up is a point x'
of B_Z X over x whose stalk is Localization.AtPrime (chartOrigin y ρ), compatibly with π^*
on germs (Kollár's chart coordinates (60.2), [Kol07, Definition 60]; Hauser's local blow-up,
[Hau14, Definitions 4.15, 4.16]).