The separation step of the marked order reduction: the chain state, the link and the descent #
The second step of Kollár's proof of the marked order reduction theorem [Kol07, Theorem 107]
lowers the maximal order s of the nonmonomial part N(I) along cosupp(I, m) to 0, by
applying the order reduction BO_{n, ms} to N(I)^m + I^s and continuing with s − 1
[Kol07, 111, Step 2]. On an analytic manifold each application is a link of the chain of
relatively compact opens on which the sequence is built (ChainState), following the links of
the first step (the rounds of order reduction on N(𝓘), stepAChainState, with their states
BState). This module provides:
- the facts along a succession: along a list of order
≥ msforJ₁^m + J₂^sthe marked transforms of(J₁^m + J₂^s, ms)aremt(J₁, s)^m + mt(J₂, m)^sat every stage (markedTransformSeq_pow_add_pow), and such a list is of order≥ sfor(J₁, s)and of order≥ mfor(J₂, m)(IsOfOrderGe.left_of_pow_add_pow,IsOfOrderGe.right_of_pow_add_pow), Kollár's remark in [Kol07, 111, Step 2] that a sequence of ordermsfor the sum of powers is one of ordersfor the first ideal and of ordermfor the second; the order clause is antitone in the ideal (IsOfOrderGe.of_le); a pointwise predicate on the induced triple passes through a concatenation of lists (AnalyticTriple.pred_induced_concat); - the state
SState T m W s: a chain state whose induced triple satisfies the separation invariantSepOrdLe … m s, entered from the exit bound of the first step (SState.ofNonmonomialOrdLe); - the link
SState.sepLinkat a bounds ≥ 1: the value ofBO_{n, ms}at the separating triple of the induced triple (sepFunctor), read on the reading open and appended byChainState.linkWith; the order clause≥ mfor𝓘holds by the observation above, and the invariant descends tos − 1: at the last stage the transform of the separating ideal has order< ms, i.e.min(m · ord N_r, s · ord 𝓘_r) < ms, soord N_r < soncosupp(𝓘_r, m), and the transform identity moduloNgivesN(𝓘_r) = N(N_r) ⊇ N_r, henceord N(𝓘_r) ≤ ord N_r; - the descent
sepDescentAuxandsepDescentStateovers = S₀, …, 1, and its canonical instance after the first step,step2ChainState, along the chainstep2ChainOpens: the exit open of the first step, then the iterated shrinkings ofclosure Uinside it; aftert − 1links the separation bound is0, the disjointness of the cosupports (step2ChainState_sep).
The scheme-theoretic counterparts are Hironaka.BMO.step2Round and Hironaka.BMO.afterStep2
with Hironaka.BMO.sepOrder_afterStep2_eq_zero.
Facts along a succession #
Along a list of order ≥ ms for J₁^m + J₂^s (m, s ≥ 1), the marked transforms of
(J₁^m + J₂^s, ms) are mt(J₁, s)^m + mt(J₂, m)^s at every stage: at each centre the observation
of [Kol07, 111, Step 2] gives ord_Z mt(J₁) ≥ s and ord_Z mt(J₂) ≥ m, and the transform of a
sum of powers is the sum of the powers of the transforms (birationalTransform_add,
birationalTransform_pow). The scheme-theoretic counterpart is
Hironaka.Sequence.weakTransformSeq_pow_sup_pow.
A list of order ≥ ms for J₁^m + J₂^s is of order ≥ s for (J₁, s): the same centres and
boundaries, the order clause at every centre by the observation of [Kol07, 111, Step 2] ("also a
smooth blow-up sequence of order s starting with N(I)").
A list of order ≥ ms for J₁^m + J₂^s is of order ≥ m for (J₂, m) ("and a smooth blow-up
sequence of order m starting with I" [Kol07, 111, Step 2]).
The order clause is antitone in the ideal at a fixed mark: a list of order ≥ m for (J, m) is
of order ≥ m for (I, m) when I ≤ J, since mt(I, m) ≤ mt(J, m) at every stage
(markedTransformSeq_le_of_le) and the order along the centre is antitone (ordAlongIdeal_anti).
A pointwise predicate on the induced triple transports through a concatenation #
A predicate on triples which holds at the triple induced by L' from the triple induced by L
holds at the triple induced by the concatenation L.concat L'. Induction on L; the induced
triple is definitional at the constructors (induced_congr, induced_cons), so no cast across
stage_last_concat is needed. The separation invariant and the terminal bound of the monomial
step are its two instances.
Two facts about chain states #
The list of a chain state over W, restricted to V with closure V ⊆ W, is of order ≥ m
for (𝓘|V, m).
The induced triple of a chain state, restricted to the reading open and pulled back along the
corestricted lift, is the induced triple of the restricted list (pullback_pullback,
inclusion_comp_liftCorestrict, induced_pullback, pullback_inclusion_restrictLE).
The chain state of the separation step #
The state of the descent of the separation step at the separation bound s over the open
W: a chain state (a list on M.restrict W of order ≥ m for (𝓘|W, m)) whose induced triple
satisfies SepOrdLe … m s on its last stage, Kollár's s [Kol07, 111, Step 2] as an
invariant.
- L : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (M.restrict W)
- hge : self.L.toSuccession.IsOfOrderGe (T.pullback (M.inclusion W) ⋯).I m (T.pullback (M.inclusion W) ⋯).F.idealSheaf
- sep : SepOrdLe (ChainState.inducedTriple T m self.toChainState) m s
The invariant:
ord N(𝓘_ind) ≤ soncosupp(𝓘_ind, m), globally on the last stage.
Instances For
A chain state whose induced triple satisfies ord N(𝓘_ind) ≤ d everywhere (the exit bound of
the first step) is a state of the separation step at the separation bound d: the separation
step starts from the bound the first step exits with (stepAChainState_bound), with no new
supremum.
Equations
- Hironaka.Manifold.BMO.SState.ofNonmonomialOrdLe T m st h = { toChainState := st, sep := ⋯ }
Instances For
A state of the first step at the bound d (a BState) is a state of the separation step at
the separation bound d.
Equations
- Hironaka.Manifold.BMO.SState.ofBState T m st = { toChainState := st.toChainState, sep := ⋯ }
Instances For
The state at a weaker bound.
Equations
- Hironaka.Manifold.BMO.SState.weaken T m st h = { toChainState := st.toChainState, sep := ⋯ }
Instances For
The induced triple of any chain state of a triple of the marked class BMOClass m is again in
the class: the mark is unchanged, and finitely many members of the induced boundary are nonempty
(finite_nonempty_totalTransformSeqFrom).
The invariant puts the induced triple in the class of the round, SepClass m s, for s ≥ 1
(sepClass_of_sepOrdLe).
The value of the round of the separation step: BO_{n, ms} read at the separating triple
of the induced triple (sepFunctor), on the reading open, the lifted range of V ⊆ W ("we apply
order reduction to the ideal N(I)^m + I^s" [Kol07, 111, Step 2]).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The value is of order ≥ ms for the separating ideal of the restricted induced triple
(bo.isOfOrderGe; the separating triple commutes with the restriction).
The value is of order ≥ s for (N(𝓘'), s), where (M', 𝓘', E') is the restricted induced
triple ("also a smooth blow-up sequence of order s starting with N(I)" [Kol07, 111, Step 2]).
The value is of order ≥ m for the restricted induced triple itself ("and a smooth blow-up
sequence of order m starting with I" [Kol07, 111, Step 2]); this is the order clause
ChainState.linkWith requires.
One link of the descent of the separation step at the bound s ≥ 1 [Kol07, 111, Step 2]:
the value of the round appended to the list restricted to V (ChainState.linkWith, with the
order clause ≥ m for 𝓘 from the observation of the separation step), and the invariant
descends to s − 1. At the last stage of the value the transform of the separating ideal has
order < ms (bo.ord_lt at the mark ms) and equals mt(N', s)^m + mt(𝓘', m)^s
(markedTransformSeq_pow_add_pow), so min(m · ord N_r, s · ord 𝓘_r) < ms and hence
ord N_r < s wherever ord 𝓘_r ≥ m; the transform identity modulo N gives
N(𝓘_r) = N(N_r) ⊇ N_r, so ord N(𝓘_r) ≤ ord N_r < s. The bound is pulled back along the
corestricted lift (induced_pullback, ord_pullback_of_isLocalDiffeomorphAt) and passed through
the concatenation (pred_induced_concat). This is Kollár's "we stop … when
cosupp(I_r, m) ∩ cosupp(N(I_r), s) = ∅; we can continue with s − 1".
Equations
- One or more equations did not get rendered due to their size.
Instances For
One link is the shrink-and-append step with the round's value.
The descent of the separation step: j links from the state st₀ at the bound S₀ on
W 0, giving the state on W j at the bound S₀ − j ("we can continue with s − 1 and so on"
[Kol07, 111, Step 2]). The descent runs through every bound S₀, S₀ − 1, …, 1; a round at a bound
above the actual separation order is empty up to the deletion of empty blow-ups.
Equations
- One or more equations did not get rendered due to their size.
- Hironaka.Manifold.BMO.sepDescentAux hT bo hcomp hidN hm W hW r hWsub S₀ st₀ 0 x_3 x_4 = st₀
Instances For
The final state of the descent, after S₀ links, at the separation bound 0
("eventually we achieve a situation where the cosupports of N(I) and of (I, m) are disjoint"
[Kol07, 111, Step 2]).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical separation step: the chain inside the exit open of the first step #
The exit open of the first step, which contains closure U (the open of stepAChainState).
Equations
- Hironaka.Manifold.BMO.step2Outer T t U hU = Hironaka.Manifold.BMOmod.stepAChainOpens U hU (Hironaka.Manifold.BMOmod.stepALinks T t U hU)
Instances For
The canonical chain of the separation step: the exit open of the first step, then the iterated
shrinkings of closure U inside it (shrinkChain).
Equations
- Hironaka.Manifold.BMO.step2ChainOpens T t U hU 0 = Hironaka.Manifold.BMO.step2Outer T t U hU
- Hironaka.Manifold.BMO.step2ChainOpens T t U hU k.succ = Hironaka.Manifold.shrinkChain (closure ↑U) (Hironaka.Manifold.BMO.step2Outer T t U hU) hU ⋯ k
Instances For
The state after the separation step: the descent from the final state of the first step
(stepAChainState, whose exit bound t − 1 is the initial separation bound) along the canonical
chain, t − 1 links; at the exit the separation bound is 0, i.e.
cosupp(𝓘, m) ∩ cosupp N(𝓘) = ∅ [Kol07, 111, Step 2]. The scheme-theoretic counterpart is
Hironaka.BMO.afterStep2.
Equations
- One or more equations did not get rendered due to their size.
Instances For
At the exit of the separation step the cosupports of (𝓘, m) and of N(𝓘) are disjoint
[Kol07, 111, Step 2].