The blow-up of a chart is the affine blow-up of its ring; the exceptional ideal on a chart #
For a chart E of étale coordinates adapted to Z on the affine open U ≅ Spec Γ(U), with
J = (x_1, …, x_r) = Z(U) the ideal of the center:
B_{Z∩U} Uis the affine blow-upaffineBlowUp JofΓ(U)alongJ(exists_iso_blowUp_affineBlowUp; [Hau14, Theorem 4.19] with [Hau14, Definition 4.16]): both are blow-ups in Hauser's sense along the same ideal sheaf (comap_toSpecΓ_specIdealSheaf, fromZ(U) = J), so they are isomorphic by the uniqueness of the blow-up (IsBlowUp.exists_iso, withIsBlowUp.comp_isoofHironaka/Scheme/BlowUp/ProductCenter.leantransporting the predicate alongU ≅ Spec Γ(U)).- On the chart of
x_j, from the chart-stalk lemmas ofHironaka/Scheme/BlowUp/AffineBlowUp/Universal/Membership.lean: the stalk of the exceptional ideal at a pointx'of the chart is generated byx_j(stalkIdeal_exceptionalIdeal_chart; the local equationu_m = yof the exceptional divisor in the proof of [Wlo05, Lemma 2.6.3]);π^*is the localized chart map on germs (stalkMap_π_specGerm); and the stalk at a point of the chart is the localization of the chart ring (exists_ringEquiv_stalk_localization, Mathlib'sSpec.stalkIso), Hauser's local blow-up [Hau14, Definitions 4.15, 4.16].
These identify the local rings of B_Z X at points of the standard charts with localizations of
the chart rings Γ(U)[J/x_j], the form in which the order of an ideal is computed after a blow-up
(Hironaka/Scheme/Snc/ChartStalk.lean).
The Γ(X, U)-algebra structure of Γ(U, ⊤) through U.toSpecΓ is the canonical
isomorphism.
The ideal sheaf Z ∩ U on the affine chart U ≅ Spec Γ(U) is the ideal sheaf of J = Z(U).
B_{Z∩U} U is the affine blow-up of Γ(U) along J, over U ≅ Spec Γ(U), by the uniqueness
of the blow-up ([Hau14, Theorem 4.19]).
At a point x' of the chart of x_j, the stalk of the exceptional ideal is generated by x_j
(= y_j), read in the stalk of the chart through the chart's stalk map (an isomorphism, the
chart being an open immersion): the local equation of the exceptional divisor on the chart of
[Kol07, Definition 60] and of the proof of [Wlo05, Lemma 2.6.3].
π^* : 𝒪_{X,x} → 𝒪_{B,x'} is the localization of the chart map (Hau14, Definitions 4.15,
4.16 and Remark 4.17): on the germ of a section s of U, π^*(s) read in the stalk of the
chart is the germ of (chart map)(s).
The stalk of B_{Z∩U} U at the point x' of the chart of x_j given by the prime 𝔭' is the
localization Γ(U)[J/x_j]_{𝔭'}, compatibly with germs through the chart's stalk map (Hauser's
local blow-up, [Hau14, Definitions 4.15, 4.16]).