The preimage of the singular locus is a simple normal crossing divisor #
Clause (3) of [Kol07, Theorem 36] for the resolution of an embedded affine scheme, following the
proof of [Kol07, Theorem 27]: since the last centre Z_j is smooth, the resolution
g : Z_j → X̄ is not an isomorphism over any singular point, so g⁻¹(Sing X̄) is the trace on
Z_j of the total exceptional divisor Ex_tot(π_0 ⋯ π_{j−1}), and Z_j has simple normal
crossings with Ex_tot, so the trace is a simple normal crossing divisor on Z_j. Here Z_j is
replaced by the end result X̄_j of the truncated restriction, an open subscheme of the centre
(Hironaka.Resolution.Algebraic.Kol07.Thm36.Identification), embedded in the ambient stage A_j by
the last stage lift ι of the closed immersion emb.
The witness family is F := (Ex_tot).comap ι, the restriction to X̄_j of the total transform of
the (empty) boundary at stage j:
Fhas simple normal crossings by the last sentence of [Kol07, Definition 24]:Ex_tothas simple normal crossings withZ_j[Kol07, Theorem 35 (1)], hence withX̄_j(the two ideals agree along the open subscheme), and no component ofEx_totcontainsX̄_jnear any of its points, because the generic point ofX̄_jlies over no centre (no earlier centre contains the strict transform ofX) and hence offEx_tot[Kol07, Definition 25].F.support = g⁻¹(Sing X): a pointpofX̄_jonEx_totlies over a restricted centreZ_m ∩ X̄_m[Kol07, Definition 25; Definition 30, 30.2], so its image is singular by clause (2) (the hypothesishno: no restricted centre over a smooth point); a pointpoffEx_totlies over no centre, so the ambient stage map is an isomorphism on stalks atι pcarryingI_Xonto the strict transform, the local ring ofXatg pis that ofX̄_jatp, regular sinceX̄_jis smooth by clause (1), sog pis a smooth point.
Main results #
exists_isSnc_comap_totalTransformSeq_last: the theorem for a blow-up sequenceTat its last stage, with hypotheses:Tis a smooth blow-up sequence, the total transform of the boundary at the last stage has simple normal crossings with a subschemeZccontainingX̄as an open subscheme, no centre ofTcontains the strict transform ofX,X̄is smooth overk, and no restricted centre has a point over a smooth point ofX.exists_isSnc_comap_totalTransformSeq_take: the same for the truncationS.take j, with the hypotheses stated at the indexjofS.
The hypotheses are discharged for the principalization sequence BP TA at the first-centre index
in Hironaka.Resolution.Algebraic.Kol07.Thm36.AffineTheorem36IsoSnc, giving clause (3) of Theorem
36 for BR_affine.
Bookkeeping: divisor-family supports and the last stage lift #
The support of a divisor family with no members is empty.
The last stage lift of a closed immersion along a blow-up sequence is a closed immersion
(isClosedImmersion_pullbackStageHom at the last index).
The kernel of the last stage lift of a closed immersion is the strict transform of its kernel
at the last stage [Kol07, Definition 30, 30.2] (ker_pullbackStageHom).
Theorem 36 (3) at the last stage of a sequence #
Clause (3) of [Kol07, Theorem 36] for the restriction of a blow-up sequence T on A to a
reduced closed subscheme X = V(I), after the proof of [Kol07, Theorem 27]: given a subscheme Zc
of the last stage containing the strict transform X̄ = V(strictTransformSeq I) as an open
subscheme, the total transform Ex_tot of the boundary having simple normal crossings with Zc,
through every point of X̄ an integral closed subscheme V(J) ⊆ X whose strict transform passes
through the point and which no centre of T contains (hcomp; for an integral X, V(J) = X
itself; for a reduced X, the component through the image of the point), X̄ smooth over k and
no restricted centre over a smooth point of X, the family Ex_tot|_{X̄} has simple normal
crossings and its support is the preimage of the singular locus of X. The generic point of the
strict transform of V(J) lies over no centre, hence off Ex_tot, so no member of Ex_tot
contains X̄ near the point (not_stalkIdeal_le_of_specializes_notMem).
Clause (3) of [Kol07, Theorem 36] for the restriction of a blow-up sequence T on A to an
INTEGRAL closed subscheme X = V(I): exists_isSnc_comap_totalTransformSeq_last_of_forall with
V(J) = X at every point.
Transport to the truncation S.take j #
Clause (3) of [Kol07, Theorem 36] on the truncation S.take j, for a reduced closed
subscheme X, with the hypotheses stated at the index j of S except hcomp, which is stated
on the truncation at its last stage (exists_isSnc_comap_totalTransformSeq_last_of_forall).
Clause (3) of [Kol07, Theorem 36] on the truncation S.take j, with the hypotheses stated at
the index j of S: the total transform at stage j has simple normal crossings with the centre
Z_j, which contains the strict transform X̄_j as an open subscheme; no earlier centre contains
the strict transform; X̄_j is smooth over k; no restricted centre lies over a smooth point.