The total transform at a point of the exceptional divisor #
At a point x' of the exceptional divisor F of the blow-up π : B_Z X → X of a smooth variety
along a centre Z having simple normal crossings with a divisor E, the stalk 𝒪_{B,x'} together
with the stalks of F and of the total transforms π^{-1}(E^i) has the shape TotalTransformData
(exists_totalTransformData_of_mem_support): a regular local ring, a regular system of parameters
z, F = (z_j), each total transform of one of the four shapes of Hauser's chart computation. This
is the chart computation of the proof of [Hau14, Proposition 5.3] and of [Hau14, Proposition 5.4]
([Hau03, Appendix C]) read at an arbitrary, possibly non-closed, point;
Hironaka.Scheme.Snc.TotalTransformSnc reads Kollár's conditions off it.
Why the theorem holds. Let x = π(x'). A closed point x₀ of the closure of x exists because
X is Jacobson (locally of finite type over a field), and x₀ ∈ Z as Z is closed.
[Kol07, Definition 24 (4)] gives snc coordinates at x₀; on an affine neighbourhood V₀ of x₀ on
which f has constant relative dimension they spread to a chart U ∋ x₀ of étale coordinates
adapted to Z on which the components through x₀ are coordinate hyperplanes and the others are
absent (exists_etaleCoordinatesAdapted_of_snc of Hironaka.Scheme.Snc.SpreadSnc); U contains
x because x ⤳ x₀. The point x' lies over U, hence in B_{Z∩U} U ≅ π^{-1}(U)
(exists_restrictHom_eq), in the chart of some x_j as a prime p of the chart ring
(exists_chart_point_map_stalkIdeal_eq of Hironaka.Scheme.Snc.ChartStalk), and the chart
computation (totalTransformData_chart of Hironaka.Scheme.Snc.ChartSncData) gives the shape in
Γ(U)[J/x_j]_p, which transports along the isomorphisms of stalks back to 𝒪_{B,x'}
(TotalTransformData.of_ringEquiv, TotalTransformData.of_comap_isOpenImmersion).
Sources: [Hau14, Proposition 5.3] (the proof); [Hau14, Proposition 5.4]; [Hau03, Appendix C]; [Kol07, Definition 24; Definition 60].
The total-transform shape transports along an open immersion: the stalk map is an isomorphism carrying the stalks of the inverse images to the stalks.
Every point of B_I X over U comes from B_{I|_U} U along blowUpMap U.ι I.
The inverse image along π of an ideal sheaf D, pulled back to B_{I|_U} U, is the inverse
image of D|_U along π_U (blowUpMap U.ι I ≫ π = π_U ≫ U.ι; the general form of
comap_restrictHom).
A smooth morphism to Spec k has, around every point, an affine open on which it is smooth of
a constant relative dimension — the dimension of a standard smooth presentation of the section
ring (Mathlib's Smooth.exists_isStandardSmooth, read with
smoothOfRelativeDimension_of_forall_exists_affineOpen).
Every point of a Jacobson space specializes to a closed point (Mathlib's
nonempty_inter_closedPoints on the closure of the point).
Snc data at a point x₀ = ι y₀ of X transport to the point y₀ of an open V ⊆ X for the
restricted ideal sheaves.
An ideal sheaf whose restriction to an affine open U is the unit ideal sheaf has
D(U) = ⊤.
Containments of stalk ideals transport along an open immersion (in both directions).
The chart computation of the proofs of [Hau14, Proposition 5.3] and [Hau14, Proposition 5.4]
([Hau03, Appendix C]) at a possibly non-closed point: at a point x' of the exceptional divisor of
the blow-up of X along a centre Z with simple normal crossings with the family D
([Kol07, Definition 24 (4)], given as data), the stalks of the exceptional divisor and of the total
transforms of the components have Hauser's chart shape TotalTransformData; moreover a component
whose total transform lies in the exceptional ideal at x' contains Z near π(x').
The pointwise form: the snc data are needed only at the points of Z to which π(x') specializes —
the proof uses them at ONE closed point x₀ with π(x') ⤳ x₀ — so the hypothesis asks for them
there only; exists_totalTransformData_of_mem_support (data at every point of Z) is the corollary
below.
The chart computation of the proofs of [Hau14, Proposition 5.3] and [Hau14, Proposition 5.4]
([Hau03, Appendix C]) at a possibly non-closed point: at a point x' of the exceptional divisor of
the blow-up of X along a centre Z with simple normal crossings with the family D
([Kol07, Definition 24 (4)], given as data at every point of Z), the stalks of the exceptional
divisor and of the total transforms of the components have Hauser's chart shape
TotalTransformData; moreover a component whose total transform lies in the exceptional ideal at
x' contains Z near π(x'). The corollary of the pointwise
exists_totalTransformData_of_mem_support_of_specializes.