The total transform is snc: Kollár's conditions and the strict transforms #
The total-transform theorem of [Hau14, Proposition 5.3] in the unfolded form — families of ideal
sheaves with the snc data as explicit hypotheses, the family (π_*^{-1} E^i, F) as
totalTransformFamily; the forms on the predicates IsSnc, HasSncWith, IsSncAt,
totalTransform, strictTransform and exceptionalDivisor are in
Hironaka.Scheme.Snc.TotalTransformChartComputation:
- at a point
x'of the exceptional divisorF, Kollár's conditions (1)–(3) for the family(π_*^{-1} E^i, F)(exists_snc_data_totalTransform_of_mem_support), read offTotalTransformDataatx'(exists_totalTransformData_of_mem_supportofHironaka.Scheme.Snc.TotalTransformOnCentre) and the saturations(T : F^∞)ofTotalTransformData.iSup_colon_eq— the strict transform of a component throughx'is the coordinate hyperplane(z_a), the exceptional divisor is(z_j), the other members missx'; - at a point
x' ∈ Foverxwith snc coordinateszatx(D_x = (z_c),Z_x = (z_l : l ∈ s)): forc ∉ sthe strict transform ofDhas stalk(π^* z_c)(stalkIdeal_strictTransformAlong_of_notMem) and contains the fibre overZ ∩ D(mem_support_strictTransformAlong_iff_of_notMem); forc ∈ s,π^* z_c = u efor a generatoreofF_{x'}and the strict transform has stalk(u)(exists_stalkIdeal_strictTransformAlong_eq_span_of_mem); whereπ^* z_citself generatesF_{x'}the strict transform missesx'(notMem_support_strictTransformAlong_of_stalkIdeal_eq); - every member of the total transform is a smooth divisor (
isSmoothDivisor_totalTransformFamily), from the snc data at every point (on and offF) andisSmoothDivisor_of_snc_dataofHironaka.Scheme.Snc.Family.
Why the lemmas hold. At x' ∈ F the total transform of D is π^*(D_x) = (π^* z_c), and
TotalTransformData says it is (z'_a z'_j), (z'_a), (z'_j) or (1) in a regular system of
parameters z' of 𝒪_{B,x'} with F_{x'} = (z'_j). Whether D contains Z near x — c ∈ s,
by span_singleton_le_span_image_iff — decides between the shapes contained in F_{x'} (the first
and third) and the others, because a total transform inside the exceptional ideal comes from a
component containing the centre (the containment clause of
exists_totalTransformData_of_mem_support), and conversely D_x ⊆ Z_x gives π^*(D_x) ⊆ F_{x'}.
The saturations then compute the strict transforms (TotalTransformData.iSup_colon_eq), and two
generators of a principal ideal of a domain differ by a unit (Mathlib's
Ideal.span_singleton_eq_span_singleton).
Sources: [Hau14, Proposition 5.3] (the proof); [Hau14, Proposition 5.4; Definition 6.2]; [Hau03, Appendix C]; [Kol07, Definition 24; Definition 25].
The stalk of the strict transform is the saturation of the stalk of the total transform by the powers of the stalk of the exceptional ideal.
The strict transform contains the total transform, so its support lies over the support of
D.
The proof of [Hau14, Proposition 5.3] and [Hau14, Proposition 5.4] ([Hau03, Appendix C]):
Kollár's conditions (1)–(3) for (π_*^{-1} E^i, F) at a point x' of F — the stalk is
regular with a regular system of parameters z'; F takes the coordinate z'_j, the strict
transform of a component through x' takes its own coordinate z'_{a i}, and the assignment is
injective.
The local rings of B_Z X are regular (on F from the chart shape, off F from those of
X).
The total transform of D = (z_c = 0) at x' is (π^* z_c).
π^* is a local homomorphism: π^* z_c ∈ 𝔪_{x'} for z_c ∈ 𝔪_x.
[Hau14, Definition 6.2]: where π^* z_c generates the exceptional ideal, the strict transform
of D = (z_c = 0) misses x': (π^* z_c) : (π^* z_c)^∞ = (1).
The proof of [Hau14, Proposition 5.3]: for c ∉ s — the component transversal to Z — the
strict transform has stalk (π^* z_c): its total transform has the shape (z'_a) of a coordinate
hyperplane, unchanged by the saturation.
The strict transform of a component transversal to Z contains the whole fibre over Z ∩ D —
x' lies on it iff x = π(x') lies on D.
[Hau14, Proposition 5.4 (7); Definition 6.2]: for c ∈ s — the component containing Z near
x — and a generator e of the exceptional ideal at x', π^* z_c = u e and the strict transform
has stalk (u): the total transform has the shape (z'_a z'_j) (then u is z'_a up to a unit)
or (z'_j) (then u is a unit and the strict transform misses x').
Kollár's conditions (1)–(3) for (π_*^{-1} E^i, F) at every point of B_Z X (on F from the
chart shape, off F from the data of X).
[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 (IsSmoothDivisor):
regular, and generated at every point by a coordinate of a regular system of parameters.