The total-transform theorem on the predicates #
The total transform of a simple normal crossing divisor under the blow-up along a centre having
simple normal crossings with it is again snc ([Hau14, Proposition 5.3]; [Kol07, Definition 25]).
This module states the theorem's ingredients on the predicates IsSnc, HasSncWith, IsSncAt
and on totalTransform, strictTransform, exceptionalDivisor, proved from the modules of
Hironaka.Snc, which are stated over families of ideal sheaves with the snc data as explicit
hypotheses (totalTransformFamily Z E for the total transform). The passage is definitional:
(E.totalTransform Z).component (toLex k) is Sum.elim (strictTransform Z ∘ E.component) (fun _ => exceptionalDivisor X Z) k, strictTransform Z D is strictTransformAlong (blowUp.π Z) (Z.comap (blowUp.π Z)) D and IsRegularSystemOfParameters z is span (range z) = 𝔪 ∧ n = dim;
hasSncWith_data and isSnc_data unfold the two predicates.
Hironaka.Scheme.Snc.TotalTransformSmoothBlowUp assembles the theorem
totalTransform_isSnc from the three statements exists_isSncAt_totalTransform_of_mem_support,
exists_isSncAt_totalTransform_of_notMem_support and isSmoothDivisor_totalTransform_component;
the section on strict transforms restates the pointwise description of the strict transforms of
Hironaka.Scheme.Snc.TotalTransformSnc on the predicates.
The mathematics, module by module ([Hau14, Proposition 5.3; Proposition 5.4; Definition 6.2]; [Hau03, Appendix C]; [Kol07, Definition 24; Definition 25; Definition 60]):
Hironaka.Scheme.Snc.TotalTransformOffCentre: overX ∖ Zthe blow-up is an isomorphism, soπ^*is an isomorphism of stalks, the strict transforms have stalksπ^*(D_x), and Kollár's data atx = π(x')transport tox'with the entryFabsent.Hironaka.Scheme.Snc.EtaleParameters: for étale coordinatesyof ak-algebraAand any primeq,A_qis regular and the coordinates vanishing atqextend to a regular system of parameters — the coordinate derivations detect independence modulo𝔪_q².Hironaka.Scheme.Snc.SpreadSnc: the snc data at a closed pointx₀ ∈ Zspread to a chart of étale coordinates adapted toZon which the components throughx₀are coordinate hyperplanes and the others are absent.Hironaka.Scheme.Snc.ChartStalk,Hironaka.Scheme.Snc.ChartSncData: the stalk at any point ofB_{Z∩U} Uis a localization of a chart ringΓ(U)[J/x_j], in which the exceptional ideal is(y_j)and the total transform of a component is(y_c y_j),(y_j),(y_c)or(1); with the étale parameters this is the shapeTotalTransformData.Hironaka.Scheme.Snc.TotalTransformData: the shape, its transport along ring isomorphisms and the saturations(y_c y_j) : y_j^∞ = (y_c),(y_c) : y_j^∞ = (y_c),(y_j) : y_j^∞ = (1)that compute the strict transforms.Hironaka.Scheme.Snc.TotalTransformOnCentre: every pointx'ofFis reached — a closed point of the closure ofπ(x')is onZ(Jacobson), an affine neighbourhood of constant relative dimension, the chart, the pointx'over the chart — and the shape transports back to𝒪_{B,x'}; a total transform inside the exceptional ideal comes from a component containingZ.Hironaka.Scheme.Snc.TotalTransformSnc: Kollár's (1)–(3) at the points ofF, the strict transforms of transversal components and of components containing the centre, regular stalks ofB_Z X, and every member of the total transform a smooth divisor.
The data of [Kol07, Definition 24 (4)] behind E.HasSncWith Z, unfolded: at every point of Z
a regular system of parameters, the injective assignment of coordinates to the components through
the point, and the index set cutting out Z.
The data of [Kol07, Definition 24 (1)–(3)] behind E.IsSnc at every point, unfolded.
[Hau14, Proposition 5.3; Proposition 5.4] ([Hau03, Appendix C]) at every point of the exceptional divisor, not only the closed ones: there are local coordinates for which the total transform satisfies Kollár's conditions (1)–(3).
[Kol07, Definition 25], the proof of [Hau14, Proposition 5.3]: at every point x' off the
exceptional divisor the blow-up is a local isomorphism and the total transform restricts to E, so
there are local coordinates for which it satisfies Kollár's (1)–(3).
[Hau14, Proposition 5.3]: every member of the total transform — the strict transforms of the
components and the exceptional divisor — is a smooth divisor of B_Z X (regular, and principal at
every point with a generator in 𝔪 ∖ 𝔪²).
On the predicates: at x' ∈ F over x with snc coordinates z at x and a component
E^i = (z_c = 0) transversal to Z (c ∉ s), the strict transform has stalk (π^* z_c) —
stalkIdeal_strictTransformAlong_of_notMem of Hironaka.Scheme.Snc.TotalTransformSnc.
On the predicates: the strict transform of a component transversal to Z contains the whole
fibre over Z ∩ E^i — mem_support_strictTransformAlong_iff_of_notMem of
Hironaka.Scheme.Snc.TotalTransformSnc.
On the predicates: for a component E^i = (z_c = 0) containing Z near x (c ∈ s) and a
generator e of the exceptional ideal at x', π^* z_c = u e and the strict transform has stalk
(u) ([Hau14, Proposition 5.4 (7)]) — exists_stalkIdeal_strictTransformAlong_eq_span_of_mem of
Hironaka.Scheme.Snc.TotalTransformSnc.
On the predicates: where π^* z_c generates the exceptional ideal, the strict transform of
E^i = (z_c = 0) misses x' ([Hau14, Definition 6.2]) —
notMem_support_strictTransformAlong_of_stalkIdeal_eq of Hironaka.Scheme.Snc.TotalTransformSnc.