The end result of the affine resolution is smooth #
Clause (1) of [Kol07, Theorem 36] for the resolution of an embedded affine scheme, after the proof
of [Kol07, Corollary 22]: the centre Z_j is smooth, being the centre of a smooth blow-up, so
g : Z_j → X̄ is a resolution. The last stage of the truncated restriction
BR_affine TA emb embeds in the ambient stage A_j with kernel the strict transform X̄_j
(ker_pullbackStageHom); at the first index j whose centre Z_j contains X̄_j, the inclusion
X̄_j → Z_j is an open immersion (Hironaka.Resolution.Algebraic.Kol07.Thm36.Identification), so
the smoothness of Z_j over k (clause (1) of [Kol07, Theorem 35]) descends to X̄_j and to the
end result.
comap_stageMap_le_strictTransformSeq: the strict transform lies overV(I);stageMap_mem_support_of_mem_center_support_of_isOrderSeq: the centres of a sequence of order1lie overV(I)(Kollár'sπ_0 ⋯ π_{j−1}(Z_j) ⊂ X̄by (21.2) in the proof of [Kol07, Corollary 22], the hypothesis of the identification), which holds forBP TAwith empty boundary;isRegular_of_smooth: a scheme smooth over a field of characteristic zero is regular;smooth_subschemeι_comp_of_heq: transport of smoothness across the identifications of the stages of a truncated sequence with those of the sequence;smooth_composite_pullback_take: the general form; the composite of the restriction of a truncated sequence is smooth over the base once the last centre contains the strict transform by an open immersion;smooth_composite_BR_affine_of_smooth_center: clause (1) forBR_affine, with the smoothness of the centre at the first index (clause (1) of [Kol07, Theorem 35]) as the hypothesis, whichHironaka.Resolution.Algebraic.Kol07.Thm36.AffineTheorem36discharges.
The strict transform lies over V(I) #
The strict transform at stage n contains the total transform I·𝒪_{A_n}, in the ⟨n, hn⟩
form (each step: π^* J ≤ (π^* J : E^∞), le_saturate).
The strict transform at stage i contains the total transform I·𝒪_{A_i}.
A point of the strict transform lies over V(I).
The centres lie over V(I) — Kollár's π_0 ⋯ π_{j−1}(Z_j) ⊂ X̄ by (21.2) in the proof of
[Kol07, Corollary 22] — the hypothesis of the identification of the end result with a component of
the centre: the centres of a blow-up
sequence of order 1 for (I, E) (IsOrderSeq; the output of BMO_1 on (A, I, ∅), which is
BP TA when the boundary is empty) lie over V(I), since a point of a centre has ord I ≥ 1
(le_ord_stageMap_of_mem_center).
Regularity from smoothness #
A scheme smooth over a field of characteristic zero (a perfect field) is regular.
Transport across the take identifications #
Smoothness of V(J) → W → V is invariant under the heterogeneous identifications of the stages
of a truncated sequence with those of the sequence (stage_take_mk and the _take_heq_mk lemmas of
Hironaka.Scheme.BlowUpSequence.Truncate).
The end result of the truncated restriction #
The end result of the truncated restriction is smooth, general form Kol07, Corollary 22,
proof: for a closed immersion emb : X → A with kernel I, if the centre Z_j of S contains
the strict transform X̄_j of X and the inclusion X̄_j → Z_j is an open immersion, then the
composite of the restriction to X of the first j steps, followed by emb and a morphism
g : A → B under which Z_j is smooth, is smooth: the end result X_j is X̄_j
(ker_pullbackStageHom), an open subscheme of Z_j.
Clause (1) of [Kol07, Theorem 36] for the affine resolution, with the smoothness of the centre
at the first index as the hypothesis: for an integral X ↪ A with kernel I_X, if the
first-centre index j is an index of BP TA, the centre Z_j is smooth over k and lies over
V(I_X) (Kollár's π_0 ⋯ π_{j−1}(Z_j) ⊂ X̄ by (21.2), [Kol07, Corollary 22, proof]; for
BP TA with empty boundary this comes from the order property of the centres of BMO_1), then
the end result of BR_affine TA emb is smooth over k.