Clause (1) of Theorem 36 for the affine resolution #
The lemmas of Hironaka.Resolution.Algebraic.Kol07.Thm36.Absorption and
Hironaka.Resolution.Algebraic.Kol07.Thm36.AffineEndResult take the conclusions of Kollár's
principalization theorem [Kol07, Theorem 35] as hypotheses. Here they are supplied by the library's
proofs of that theorem for the sequence BP TA:
- clause (2),
Π^* I_Xis the ideal of a simple normal crossing divisor (BP_isIdealOfSncDivisor), hence invertible on the smooth end result (isInvertible_comap_composite_BP); - clause (1), every centre is smooth over
k(BP_center_smooth_hasSncWith), so the centre at the first containing index is; - the centres of
BP(A, I_X, ∅)lie overV(I_X)(stageMap_mem_support_of_mem_center_BP, Kollár'sπ_0 ⋯ π_{j−1}(Z_j) ⊂ X̄by (21.2) in the proof of [Kol07, Corollary 22]).
The results, for an integral algebraic k-scheme X embedded in the ambient of a triple TA
with empty boundary, with I_X = ker emb and X of codimension ≥ 2 at its generic point: some
centre of BP TA contains the strict transform of X, so the first-centre index is an index of
the sequence (exists_centerContains_BP_affine, firstCenterIndex_lt_length_BP_affine,
centerContains_firstCenterIndex_BP_affine, not_centerContains_of_lt_BP_affine); BR_affine
has exactly that many steps (length_BR_affine_of_integral); its end result embeds in the last
stage with kernel the strict transform (ker_pullbackStageHom_last_BR_affine'); and the end
result is smooth over k (smooth_composite_BR_affine_of_integral), which is clause (1) of
[Kol07, Theorem 36] for the affine resolution. Clauses (2) and (3) are
Hironaka.Resolution.Algebraic.Kol07.Thm36.AffineTheorem36IsoSnc.
The emptiness of the boundary enters only through the last item (the centres over V(I_X)); the
standing hypotheses of an algebraic k-scheme on X (locally of finite type, quasi-compact,
separated over k) are carried by every statement although not every proof uses them.
Theorem 35 read for the absorption argument #
Clause (1) of [Kol07, Theorem 35]: BP TA is a smooth blow-up sequence (every centre smooth
over k).
The end result of BP TA is smooth over k: the composite of smooth blow-ups of the smooth
ambient.
Clause (2) of [Kol07, Theorem 35] read as in the proof of [Kol07, Corollary 22]: Π^* I_X is
invertible, being the ideal of a simple normal crossing divisor on the smooth end result
(IsIdealOfSncDivisor.isInvertible).
The first containing centre, the length, and the smooth end result #
The theorems below are stated for an algebraic k-scheme X (locally of finite type,
quasi-compact and separated over k) embedded by emb over k, the setting of
[Kol07, Theorem 36], carried by all of them so that they read in one setting; the proofs need
only some of the instances.
Some centre of BP(A, I_X, ∅) contains the strict transform of X Kol07, Corollary 22,
proof: exists_centerContains_BP_of_isInvertible with clause (2) of [Kol07, Theorem 35]. The
hypothesis _hE of an empty boundary is present because Kollár runs the principalization on the
triple (A, I_X, ∅) and the statement keeps that setting; the proof does not need it, because
the argument is local at η_X and uses only clause (2) of Theorem 35.
The first containing index is an index of the sequence BP TA.
The centre at the first containing index contains the strict transform of X Kol07,
Corollary 22, proof.
No centre before the first containing index contains the strict transform of X.
The affine resolution has exactly firstCenterIndex (BP TA) TA.I steps.
The kernel of the last stage embedding of the affine resolution is the strict transform of I_X
[Kol07, Definition 30, 30.2]; ker_pullbackStageHom_last_BR_affine restated for a scheme X
over k.
Clause (1) of [Kol07, Theorem 36] for the affine resolution ("Z_j is smooth since we blow it
up", [Kol07, Corollary 22, proof]): the end result of BR_affine TA emb is smooth over k. This is
smooth_composite_BR_affine_of_smooth_center with clause (1) of [Kol07, Theorem 35] at the first
containing index and the centres of BP(A, I_X, ∅) over V(I_X)
(stageMap_mem_support_of_mem_center_BP, the one use of the empty boundary).