The monomial step of the marked order reduction as one link, and clause (1) of the theorem #
The last step of Kollár's proof of the marked order reduction theorem [Kol07, Theorem 107] runs
the monomial procedure on the monomial part M(I), once the separation step has made the
cosupports of (I, m) and of N(I) disjoint [Kol07, 111, Step 3]. Here the procedure enters
through the structure MonomialStep3Fam (a family functor for (M(𝓘), m) whose last marked
transform of (M(𝓘), m) has order < m), read at the induced triple of the exit state of the
separation step on the reading open and appended by ChainState.linkWith (SState.step3Link);
the order clause ≥ m for 𝓘 follows from the one for M(𝓘) and 𝓘 ⊆ M(𝓘).
Clause (1) of the theorem, max-ord I_r < m, for 𝓘 itself. Kollár replaces X by
X ∖ cosupp N(I) and assumes I = M(I) [Kol07, 111, Step 2]. Here the procedure runs on
(M(𝓘), m, E) on the whole last stage of the separation step, and the clause for 𝓘 is proved
pointwise (ord_markedTransformSeq_lt_of_sepOrdLe_zero):
- at a point of the last stage over
cosupp N(𝓘): by the exit of the separation step,ord 𝓘 < mthere, soord M(𝓘) < m; no centre of the procedure meets the fibre over such a point, since the centres lie where the marked transform of(M(𝓘), m)has order≥ m, while over the point that order is the order ofM(𝓘)(off the centres a blow-up is a local analytic isomorphism and the marked transform is the pull-back,IsBlowUp.isLocalDiffeomorphOn_compl,birationalTransform_stalkIdeal_of_notMem); so the marked transform of(𝓘, m)over the point is the pull-back of𝓘, of order< m(IsOfOrderGe.forall_notMem_center_of_ord_lt,ord_markedTransformSeq_eq_of_forall_notMem); - at a point off it:
𝓘 = M(𝓘)on the open complement ofcosupp N(𝓘)(stalkIdeal_eq_monomialPart_of_notMem_cosupport), so the marked transforms of(𝓘, m)and of(M(𝓘), m)agree over that open (BlowUpSequence.markedTransformSeq_last_pullbackLiftLast), and the exit property of the procedure bounds the latter.
Transported along the lift and through the concatenation this gives SState.step3Link_ord_lt.
The module ends with the terminal state of the three steps, step23ChainState, on the open
step23ChainOpen ⊇ closure U, with step23ChainState_ord_lt; the sequence over U (bmoSeqOn)
is its restriction to U with the empty blow-ups deleted. The scheme-theoretic counterpart of
the clause is Hironaka.BMO.maxOrd_markedTransformSeq_step3Seq_lt.
The iso-locus: off the centres, the marked transform is the pull-back #
One step of the iso-locus: at a point of stage i + 1 whose image is not in the centre Z_i,
the order of the marked transform is the order of the previous marked transform at the image —
the blow-up is a local analytic isomorphism there (IsBlowUp.isLocalDiffeomorphOn_compl) and the
marked transform's stalk is the pull-back's (birationalTransform_stalkIdeal_of_notMem).
If no centre of the list meets the fibre over x, the marked transform at any point of stage
i over x has the order of the ideal at x: ord_markedTransformSeq_succ_of_notMem along the
stages.
Along a list of order ≥ m for (J, m), no centre meets the fibre over a point x with
ord_x J < m: by induction along the stages the marked transform keeps the order ord_x J < m
over x (the iso-locus step), while a centre through a point has order ≥ m there
(ordAlongIdeal_le_ord_of_mem_support). This is "the center of any further blow-up is contained
in cosupp(I, m)" [Kol07, 111, Step 2].
Clause (1) of the theorem for 𝓘 from the exit property of the monomial procedure #
The separation invariant restricts along a local analytic isomorphism (pointwise;
NonmonomialComap for the nonmonomial part, ord_pullback_of_isLocalDiffeomorphAt).
Clause (1) of [Kol07, Theorem 107] from the exit property of the monomial procedure: for a
triple (M, 𝓘, E) at the exit of the separation step (SepOrdLe … m 0) and a list L of order
≥ m for (M(𝓘), m) whose last marked transform of (M(𝓘), m) has order < m everywhere, the
last marked transform of (𝓘, m) has order < m at every point. Over cosupp N(𝓘) no centre
meets the fibre and the marked transform is the pull-back of 𝓘, of order ord 𝓘 < m; off it,
𝓘 = M(𝓘) on the open complement, so the two marked transforms agree there.
The monomial procedure as one link on the exit state of the separation step #
The value of the monomial step: the procedure st3 at the induced triple of the exit state
of the separation step, read on the reading open (the lifted range of V ⊆ W).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The value is of order ≥ m for (M(𝓘), m) (st3.isOfOrderGe), hence for (𝓘, m) since
𝓘 ⊆ M(𝓘) (IsOfOrderGe.of_le); this is the order clause ChainState.linkWith requires.
The monomial procedure as one link on the exit state of the separation step
[Kol07, 111, Step 3]: its value appended to the list restricted to V.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The link is the shrink-and-append step with the value of the monomial step.
After the monomial step the marked transform of (𝓘, m) has order < m at every point of
the last stage (clause (1) of [Kol07, Theorem 107]): ord_markedTransformSeq_lt_of_sepOrdLe_zero
at the restricted induced triple (the exit invariant of the separation step restricted to the
reading open, and the two properties of st3), pulled back along the corestricted lift and passed
through the concatenation (pred_induced_concat).
The last two steps along an arbitrary shrinking chain, and the terminal state #
The continuation of the first step by the separation and monomial steps along an arbitrary
shrinking chain W 0 ⊇ closure (W 1) ⊇ ⋯ ⊇ W t: from a state of the first step at the exit
bound t − 1 on W 0, the t − 1 links of the descent of the separation step (to W (t − 1)),
then the link of the monomial step (to W t). The number of links is fixed, so two continuations
over different opens align link by link. The canonical instance is step23ChainState; the
alignment facts step23Aux_rel and step23Aux_L_indiff are stated on this general form.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Clause (1) of [Kol07, Theorem 107] along an arbitrary chain: the last marked transform of the
continuation has order < m at every point.
The open of the terminal state: the t-th member of the canonical chain of the separation
step, which contains closure U.
Equations
- Hironaka.Manifold.BMO.step23ChainOpen T t U hU = Hironaka.Manifold.BMO.step2ChainOpens T t U hU t
Instances For
The final state of the first step, read at its exit bound t − 1 (stepAChainState_bound).
Equations
- Hironaka.Manifold.BMO.stepAExitState T m hT bo hcomp hid t hm hmt U hU = { toChainState := (Hironaka.Manifold.BMOmod.stepAChainState T m hT bo ⋯ ⋯ t hm hmt U hU).toChainState, bound := ⋯ }
Instances For
The terminal chain state of the three steps [Kol07, 111] on the open
step23ChainOpen ⊇ closure U: the state of the first step, the descent of the separation step and
the link of the monomial step along the canonical chain (step23Aux at step2ChainOpens). The
sequence over U, bmoSeqOn, is its restriction to U with the empty blow-ups deleted. The
scheme-theoretic counterpart is Hironaka.BMO.bmoSeq before the restriction.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Clause (1) of [Kol07, Theorem 107] at the terminal state: the marked transform of (𝓘, m) has
order < m at every point of the last stage.