The loop through a smooth window #
Clause (b) of [Wlo05, Theorem 1.0.2] for the embedded desingularization sequence
(Hironaka.Resolution.Algebraic.Wlo05.Embedded): no centre of BED(X, I_Y, ∅) has a point over
Reg(Y), the set of smooth points of Y. The proof ([Wlo05, 4.6]: at a smooth point of Y "the
generic points would be transformed isomorphically") runs the core lemma of the smooth case
(Hironaka.Resolution.Algebraic.Wlo05.EmbeddedNilCore) LOCALLY, on an open immersion j : W ⟶ X
through which Y is seen as ONE smooth irreducible component c — a smooth window
(SmoothWindow):
- every member of the boundary is empty over
W; - over
Wthe ideal is either the unit ideal or the restriction of a single membercof the loop's component set, integral, withV(c) ∩ Wsmooth overk, no other member meetingW.
The round lemma (smoothWindow_round_one): the run BMO_1(T) pulled back to W and stripped of
its empty blow-ups is BMO_1(W, I|_W, 1, ∅) (the second clause of [Kol07, 34.1],
dimFreeBMO_commutesWithSmooth; indifferentToEmptyMembers removes the empty boundary members),
whose first centre contains the generic point of V(c) ∩ W (core_bmoOneRun); so the FIRST
centre of BMO_1(T) with a point over W lies over the generic point of c, is the first centre
containing the strict transform of c (firstCenterIndex), and every earlier centre misses W.
The isolation lemma (smoothWindow_isolated): the loop's truncation index n₀ is at most that
first index (Nat.find_min'), and the isolated marked triple at n₀ seen through the lifted
window W_{n₀} ≅ W is again a smooth window — the ideal there is 𝒪 if c was absorbed at n₀
(the colon I_c : I_c), else the strict transform of c (the colon by the other absorbed
members, all empty over W); the boundary members, exceptional divisors of centres missing W,
are empty over W. The induction on the number of members (centersMiss_bedAux_of_smoothWindow)
then gives a form of (b) stronger than Włodarczyk's: every centre of BED misses the preimage of
W outright, whether or not the point lies on the strict transform of Y. The window at a smooth
point of Y and the clause itself are in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedRegWindow.
A smooth window j : W ⟶ T.X.left for the marked triple T and the member set C — every
boundary member is empty over W; over W the ideal is the unit ideal or the restriction of ONE
member c ∈ C, which is integral, smooth over k on W, and the only member meeting W
([Wlo05, 4.6]: near a smooth point Y is smooth and irreducible).
- ideal : T.I.comap j = ⊤ ∨ ∃ c ∈ C, T.I.comap j = c.comap j ∧ AlgebraicGeometry.IsIntegral c.subscheme ∧ AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp (c.comap j).subschemeι (CategoryTheory.CategoryStruct.comp j (T.X.left ↘ AlgebraicGeometry.Spec ↧k))) ∧ ∀ c' ∈ C, c'.comap j ≠ ⊤ → c' = c
Instances For
The run through the window #
The run of BMO_1 on T pulled back through a smooth window and stripped of its empty
blow-ups begins with a centre containing a generic point of V(I) ∩ W (the second clause of
[Kol07, 34.1] through dimFreeBMO_commutesWithSmooth, indifferentToEmptyMembers, and the core
lemma core_bmoOneRun).
The round lemma ([Wlo05, 4.6]: "otherwise the generic points would be transformed
isomorphically"; the proof of [Kol07, Corollary 22]) — through a smooth window on which the ideal
is not the unit ideal, the distinguished member c is absorbed by the run of BMO_1 on T (some
centre contains its strict transform), and every centre before the first containing one misses
W. The first centre of the run over W lies over the generic point of V(c) (the core lemma on
(W, I|_W, 1, ∅) transported through eraseEmpty), so its index is at least firstCenterIndex
(notMem_center_support_of_stageMap_eq_of_lt_firstCenterIndex), while all earlier centres of the
pullback are empty.
The isolated triple through the lifted window #
The boundary of the isolated triple is empty over the lifted window: the total transform of
an all-empty family along a prefix all of whose centres miss W ([Kol07, 34.1] on the divisor
families, totalTransformSeq_pullback).
The marked transform of I at the end of the prefix, seen through the lifted window, is the
inverse image of I|_W under the (isomorphic) stage map of the pulled-back prefix
(IsOrderGeSeq.markedTransformSeq_comap_pullbackStageHom; all centres empty).
The strict transform of a member at the end of the prefix, seen through the lifted window, is
the inverse image of its restriction under the stage map of the pulled-back prefix
(strictTransformSeq_pullback; all centres empty).
On the prefix: no centre of the prefix take n₀ contains the strict transform of c when
n₀ ≤ firstCenterIndex run c.
The proof of [Kol07, Corollary 22] on the prefix: the strict transform of an integral member at the end of a prefix before its first containing centre is integral.
The reduced ideal of the union of the strict transforms of members all empty over W is the
unit ideal over the lifted window (vanishingIdeal_iSup; strict transforms lie over V(c')).
The isolated ideal through the window, c not yet absorbed: the colon by the reduced ideal
of the absorbed members — all empty over W — is the marked transform itself there, which is the
strict transform of c (Włodarczyk's isolation read through the window).
The isolated ideal through the window, c absorbed at n₀: the colon I_c : I_c is the
unit ideal over W — the reduced ideal of the absorbed members is contained in the (reduced) strict
transform of c, which is the marked transform over W.
The strict transform of c seen through the lifted window is smooth over k when V(c) ∩ W
is: it is the inverse image of c|_W under an isomorphism (smooth_comap_subschemeι_comp).
A remaining member meeting the lifted window is the strict transform of c: its points lie
over points of the original member over W, and c is the only member meeting W.
The isolation lemma — the isolated marked triple at an index n₀ at most the first index
containing c, with the remaining members, seen through the lifted window, is again a smooth
window.
The loop through a smooth window #
No centre of the loop has a point over a smooth window (clause (b) of
[Wlo05, Theorem 1.0.2] in a stronger form; [Wlo05, 4.6]) — by strong induction on the number of
members: over a window on which the ideal is the unit ideal every centre, lying over V(I)
(stageMap_mem_support_of_mem_center on the order-≥ 1 sequence of clause (a)), misses W;
otherwise the round lemma places the truncation index n₀ = Nat.find at or before the first
centre containing c (Nat.find_min'), the prefix misses W, and the isolation lemma hands the
rest of the loop to the induction hypothesis through the lifted window.
The loop BED TX through a smooth window for the loop's component set has no centre with a
point over the window.