Step 1 of marked order reduction: reducing the order of the nonmonomial part below the mark #
Step 1 of the proof of [Kol07, Theorem 107] ([Kol07, 111, Step 1]) reduces the order of the
nonmonomial part: if ord N(I) ≥ m, order reduction for ideals ([Kol07, Theorem 68]) is applied to
N(I) until its order drops below m, reaching some Π_1 : X^1 → X; the birational transforms
(Π_1)^{-1}_* N(I) and (Π_1)^{-1}_*(I, m) differ only by an ideal sheaf of exceptional divisors,
hence only in their monomial part, so N((Π_1)^{-1}_*(I, m)) = (Π_1)^{-1}_* N(I) and the maximal
order of the nonmonomial part is now < m.
Conventions #
"Until its order drops below m" is read as a loop. The functor BO_d of [Kol07, Theorem 68] is
defined only on triples with max-ord ≤ d, so a round applies BO_{n,d}(X, N(I), E) at the
current d := max-ord N(I) ≥ m; the round is a smooth blow-up sequence of order d ≥ m for
N(I), hence of order ≥ m for (I, m); after it the nonmonomial part of the induced marked
ideal has maximal order < d; and the loop repeats, terminating on the strictly decreasing natural
number d. The input is order reduction for ideals in dimension n at every mark,
bo : ∀ d, BOData n d, since the orders d that occur are not bounded in terms of m. Kollár's
equation N((Π_1)^{-1}_*(I, m)) = (Π_1)^{-1}_* N(I) without the outer N on the right is not
asserted; what Step 1 uses is the equality of the nonmonomial parts and
max-ord N(J) ≤ max-ord J.
nonmonomialTriple T: the unmarked triple(X, N(I), E)of a marked triple(X, I, m, E).roundOrder T: the loop variabled = max-ord N(I), a natural number (the maximal order is finite on a triple's Noetherian scheme for an ideal sheaf nonzero on every component;coe_roundOrder).step1Round bo T hT hd: one round,BO_{n,d}(X, N(I), E)form ≤ d(boClass_nonmonomialTriple:(X, N(I), E)lies inBOClass n d); it is a smooth blow-up sequence of order≥ mfor(X, I, m, E)(step1Round_isOrderGeSeq, sinceI ⊆ N(I)givesord_Z I ≥ ord_Z N(I)at every centre) without empty blow-ups.roundTriple bo T hT hd: the marked triple(X^1, (Π_1)^{-1}_*(I, m), m, (Π_1)^{-1}_{tot} E)induced at the end of the round (MarkedTriple.induced), again ofBMOClass n m(bmoClass_roundTriple), withmax-ord N((Π_1)^{-1}_*(I, m)) < d(maxOrd_nonmonomialPart_roundTriple_lt,roundOrder_roundTriple_lt): along the round,N(Π^{-1}_{i *}(I, m)) = N(Π^{-1}_{i *} N(I))at every stage (nonmonomialPart_markedTransformSeq_last_eq, iteratingnonmonomialPart_markedTransformfor the marked triples(X_i, I_i, m, E_i)and(X_i, J_i, d, E_i)), andmax-ord N(J_r) ≤ max-ord J_r < dbymaxOrd_antiand clause (1) of [Kol07, Theorem 103].step1 bo T hT: Step 1, by well-founded recursion onroundOrder T: the empty sequence onced < m, and otherwise the round followed by Step 1 of the induced marked triple (concat); carried with it, it is a smooth blow-up sequence of order≥ mfor(X, I, m, E)(isOrderGeSeq_concat) without empty blow-ups (noEmptyCenters_concat). The unfolding equations arestep1_of_ltandstep1_of_le, and the result of Step 1 ismaxOrd_nonmonomialPart_step1_lt:max-ord N((Π_1)^{-1}_*(I, m)) < mat the end.
Step 1 is followed by Step 2
(Hironaka/Resolution/Algebraic/MarkedOrderReduction/Step2Separation.lean) and Step 3
(Hironaka/Resolution/Algebraic/MarkedOrderReduction/Step3Input.lean) in the assembly of the
functor (Hironaka/Resolution/Algebraic/MarkedOrderReduction/Assembly.lean).
The nonmonomial part is idempotent, N(N(I)) = N(I): N(I) is I with the monomial M(I)
divided out, and the nonmonomial part ignores monomials (nonmonomialPart_monomial_mul). Not in
the sources.
The recursion behind nonmonomialPart_markedTransformSeq_last_eq, by induction on the length
of the sequence (the marked triple advances to blowUpTriple at each step, so the induction is on
the length, not structural on a sequence over a fixed scheme).
Along a smooth blow-up sequence S of order d for (X, J, E) which is also of order ≥ m
for the marked triple T = (X, I, m, E), if N(I) = N(J) then the nonmonomial parts of the
induced marked ideal Π^{-1}_*(I, m) and of the induced birational transform Π^{-1}_* J agree at
the end of S, with respect to the induced boundary ([Kol07, 111, Step 1]:
"N((Π_1)^{-1}_*(I, m)) = (Π_1)^{-1}_* N(I)", read modulo N at every stage and iterated). One
stage applies nonmonomialPart_markedTransform twice: to (X_i, I_i, m, E_i), giving
N(I_{i+1}) = N(π^* N(I_i)), and to (X_i, J_i, d, E_i), whose marked transform at the exact
order d is the birational transform (weakTransform_eq_markedTransform_of_smooth), giving
N(J_{i+1}) = N(π^* N(J_i)). By recursion on S, the marked triple advancing to blowUpTriple.
The unmarked triple (X, N(I), E) of the marked triple (X, I, m, E) ([Kol07, 111]: "we write
I = M(I) · N(I) and try to deal with the two parts separately"; Step 1 applies (68) "to N(I)"):
the ambient scheme and the boundary of T, the ideal its nonmonomial part, nonzero on every
component by isNonzeroEverywhere_nonmonomialPart.
Equations
- Hironaka.BMO.nonmonomialTriple T = { X := T.X, smoothOfRelativeDimension := ⋯, I := Hironaka.BMO.nonmonomialPart T.I T.E, isNonzeroEverywhere := ⋯, E := T.E, isSnc := ⋯ }
Instances For
The loop variable of Step 1, d = max-ord N(I), as a natural number (coe_roundOrder: the
maximal order is finite).
Equations
Instances For
(roundOrder T : ℕ∞) = max-ord N(I): the maximal order of an ideal sheaf nonzero on every
component is finite on the Noetherian scheme of a triple (maxOrd_ne_top).
For m ≤ d = max-ord N(I), the triple (X, N(I), E) lies in the domain BOClass n d of
BO_{n,d} ([Kol07, Theorem 68]: "defined on triples (X, I, E) with max-ord I ≤ m"): the mark
d ≥ m ≥ 1, the dimension bound of T, and max-ord N(I) ≤ d by definition of d.
One round of Step 1 ([Kol07, 111, Step 1]: "apply order reduction (68) to N(I)"): the
value of BO_{n,d} at the current order d = max-ord N(I) ≥ m on the triple (X, N(I), E).
Equations
- Hironaka.BMO.step1Round bo T hT hd = ((bo (Hironaka.BMO.roundOrder T)).functor k).seq (Hironaka.BMO.nonmonomialTriple T) ⋯
Instances For
The round is a smooth blow-up sequence of order d for (X, N(I), E) (the functor's field;
[Kol07, Theorem 68]).
The round contains no empty blow-up (the functor's field; [Kol07, 32]).
The birational transform of N(I) at the end of the round has maximal order < d (clause (1)
of [Kol07, Theorem 103] for the round at order d; BOData.maxOrd_lt).
The round is a smooth blow-up sequence of order ≥ m starting with (X, I, m, E)
([Kol07, 111, Step 1]): the same centres, smooth and with normal crossings with the same boundaries
E_i, and ord_{Z_i} I_i ≥ ord_{Z_i} J_i = d ≥ m at every stage since I_i ⊆ J_i
(isOrderGeSeq_of_isOrderSeq_of_le with I ⊆ N(I) = (I : M(I))).
The marked triple (X^1, (Π_1)^{-1}_*(I, m), m, (Π_1)^{-1}_{tot} E) induced at the end of one
round ([Kol07, 111, Step 1]: "this happens at some Π_1 : X^1 → X"; MarkedTriple.induced through
step1Round_isOrderGeSeq).
Equations
- Hironaka.BMO.roundTriple bo T hT hd = T.induced (Hironaka.BMO.step1Round bo T hT hd) ⋯ (Fin.last (Hironaka.BMO.step1Round bo T hT hd).length)
Instances For
The induced marked triple after a round is again of BMOClass n m: the stages of a smooth
blow-up sequence are smooth of the same relative dimension
(IsSmooth.stageMap_smoothOfRelativeDimension), and the mark is unchanged.
After a round at order d, the nonmonomial part of the induced marked ideal has maximal
order < d ([Kol07, 111, Step 1]: the nonmonomial part of the marked transform after Π_1 is
the marked transform of N(I), which reduces the proof to the case max-ord N(I) < m; here the
drop of one round): N(Π_1^{-1}_*(I, m)) = N(Π_1^{-1}_* N(I)) along the round
(nonmonomialPart_markedTransformSeq_last_eq at J = N(I), with N(N(I)) = N(I)), N(J) ⊇ J
gives max-ord N(J) ≤ max-ord J (maxOrd_anti), and clause (1) of [Kol07, Theorem 103] gives
max-ord Π_1^{-1}_* N(I) < d.
The loop variable strictly decreases along a round: the termination measure of Step 1.
Step 1 of the proof of [Kol07, Theorem 107], Π_1 : X^1 → X ([Kol07, 111, Step 1]: order
reduction for ideals, [Kol07, Theorem 68], is applied to N(I) until its order drops below m,
which happens at some Π_1 : X^1 → X), by well-founded recursion on the loop variable
d = max-ord N(I): the empty
sequence once d < m, and otherwise one round BO_{n,d}(X, N(I), E) followed by Step 1 of the
induced marked triple (X^1, (Π_1)^{-1}_*(I, m), m, (Π_1)^{-1}_{tot} E), whose loop variable is
smaller (roundOrder_roundTriple_lt). Carried with the sequence: it is a smooth blow-up sequence
of order ≥ m starting with (X, I, m, E) (isOrderGeSeq_concat with step1Round_isOrderGeSeq)
without empty blow-ups (noEmptyCenters_concat). BO_{n,d} is called only for d ≥ m ≥ 1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Below the mark, Step 1 is the empty sequence ([Kol07, 111, Step 1]: "if ord N(I) ≥ m";
otherwise nothing is done).
At or above the mark, Step 1 is one round followed by Step 1 of the induced marked triple (the loop unrolled once).
Step 1 is a smooth blow-up sequence of order ≥ m starting with (X, I, m, E)
([Kol07, Definition 66] for Π_1).
Step 1 contains no empty blow-up ([Kol07, 32]).
The induction behind maxOrd_nonmonomialPart_step1_lt, on a bound l for the loop variable,
following the recursion of step1.
At the end of Step 1, max-ord N((Π_1)^{-1}_*(I, m)) < m with respect to the induced
boundary (Π_1)^{-1}_{tot} E ([Kol07, 111, Step 1]: "we have reduced to the case where the maximal
order of the nonmonomial part is < m"). By induction along the loop: below the mark the sequence
is empty and max-ord N(I) < m is the exit condition; otherwise the end data of round ++ rest
are the end data of rest for the induced marked triple (markedEnd_concat_iff), where the
statement holds by induction.
The loop variable of the marked triple induced at the end of Step 1 is below the mark: the form
in which Step 2 receives the result ([Kol07, 111]: "from now on we may assume that
max-ord N(I) < m").