The sequence over a relatively compact open: the terminal chain state and its value #
Kollár's proof of the marked order reduction theorem [Kol07, Theorem 107] runs three steps on the
marked triple (X, I, m, E) [Kol07, 111]: the first lowers the order of the nonmonomial part
N(I) below m, the second separates cosupp(I, m) from cosupp N(I), the third lowers the
order of the monomial part; each runs on the triple obtained at the end of the previous one, and
the proof ends with max-ord I_r < m, clause (1) of the theorem. On an analytic manifold the
value of the functor is read on each relatively compact open U [Wlo09, Theorem 2.0.3], and the
three steps cannot be composed as values on M.restrict U: a round of an order reduction functor
is read on a relatively compact open of the manifold at hand, which the last stage of a sequence
over M.restrict U is not. The steps are therefore composed as links of a chain (ChainState):
the list is built on a shrinking chain of relatively compact opens of M containing closure U,
every round is read on the lifted range of an inclusion, and the restriction to U with the
deletion of empty blow-ups [Kol07, 32] comes last.
This module joins the chain to the structure BMOanFam. The terminal chain state
TerminalState T m W is a ChainState whose induced triple has order < m at every point of the
last stage, the state the monomial step exits with; its value on U ≤ W,
TerminalState.valueOn, is the list of the state pulled back along the open inclusion and cleaned
of empty blow-ups. Its four exports are the facts BMOanFam reads on each open: no empty centres,
order ≥ m for the restricted triple (valueOn_isOfOrderGe), stability under the deletion of
empty blow-ups, and clause (1) pointwise (ord_lt_valueOn: the marked transform at the last stage
of the value has order < m at every point over U). The last is the terminal bound transported
along the pull-back (induced_pullback, pullback_inclusion_restrictLE,
ord_pullback_of_isLocalDiffeomorphAt) and through the deletion of empty blow-ups
(BlowUpSequence.markedTransformSeq_last_eraseEmpty: the marked transform of the cleaned list is
the pull-back of that of the list along the diffeomorphism eraseEmptyLast of the last stages).
Three further lemmas transport the naturality properties from the states to the values: if the
lists of two terminal states agree on U up to empty blow-ups, the values satisfy the
compatibility CompatibleFamily.compat; if a terminal state for a pulled-back triple has, up to
empty blow-ups, the pulled-back list, the values satisfy the commutation with local analytic
isomorphisms; equal cleaned lists give equal values. The alignment of two chains, the substance of
[Kol07, 34.1] and of [Wlo09, Theorem 2.0.3 (4)] for the composite of the three steps, is proved
for the first step by a virtual descent over a pair of opens and continued through the other two
in bmoSeqOn_compat, bmoSeqOn_pullback and bmoSeqOn_indiff.
The sequence bmoSeqOn is the value of the terminal state of the three steps along the canonical
chain of U (step23ChainState). The scheme-theoretic counterpart is Hironaka.BMO.bmoSeq.
The terminal chain state #
A terminal chain state: a chain state over the open W (a list on M.restrict W of order
≥ m for the restricted triple) whose induced triple at the last stage has order < m at every
point, clause (1) of [Kol07, Theorem 107] on the state. It is the state the three steps exit with,
before the restriction to the relatively compact open and the deletion of empty blow-ups.
- L : AnalyticManifold.BlowUpSequence ψ₀ (M.restrict W)
- hge : self.L.toSuccession.IsOfOrderGe (T.pullback (M.inclusion W) ⋯).I m (T.pullback (M.inclusion W) ⋯).F.idealSheaf
- ord_lt (x : ↑↧(self.L.stage (Fin.last self.L.length)).carrier) : Manifold.IdealSheaf.ord (ChainState.inducedTriple T m self.toChainState).I x < ↑m
Clause (1) of [Kol07, Theorem 107] on the state: the marked transform at the last stage has order
< meverywhere.
Instances For
The list of a chain state over W, pulled back to an open U ≤ W, is of order ≥ m for the
triple restricted to U (isOfOrderGe_pullback along the open inclusion,
pullback_inclusion_restrictLE).
The value on a relatively compact open #
The value of a terminal state on an open U ≤ W: its list pulled back along the open
inclusion and cleaned of empty blow-ups [Kol07, 32]. The sequence of the functor over U is this
value at the state the three steps exit with.
Equations
- st.valueOn hUW = (st.L.pullback (M.restrictLE hUW) ⋯).eraseEmpty
Instances For
The value has no empty blow-ups [Kol07, 32].
The deletion of empty blow-ups is the identity on the value (eraseEmpty_eraseEmpty).
The value is a smooth blow-up sequence of order ≥ m for the triple restricted to U
[Kol07, Definition 66 (2′)–(4′)]: the invariant of the chain along the inclusion, kept by the
deletion of empty blow-ups.
Clause (1) of [Kol07, Theorem 107] on the value, pointwise: the marked transform at the last
stage of the value has order < m at every point over U. The terminal bound of the state is
transported along the pull-back (induced_pullback: the induced triple of the pulled-back list is
the pull-back of the induced triple along the lift of the last stages;
ord_pullback_of_isLocalDiffeomorphAt) and through the deletion of empty blow-ups
(BlowUpSequence.markedTransformSeq_last_eraseEmpty).
The three naturality transports, from the states to the values #
The compatibility CompatibleFamily.compat on the values ([Wlo09, Theorem 2.0.3 (4)],
[Wlo09, Definition 3.2.6]; [Kol07, 34.1]): two terminal states whose lists agree on U ≤ V up to
empty blow-ups have compatible values (eraseEmpty_pullback_eraseEmpty).
The commutation with local analytic isomorphisms on the values [Kol07, 34.1]: a terminal state
for the triple pulled back along a local analytic isomorphism g, whose cleaned list is the
cleaned pull-back of the list of a terminal state along g|_{W'}, has on U' ≤ W' the value on
g(U') pulled back along g|_{U'} and cleaned (eraseEmpty_pullback_eraseEmpty, pullback_comp:
both sides are the list pulled back along the same map U' → W).
The indifference to empty boundary members on the values (the counterpart, for boundary
members, of [Kol07, 32]): two terminal states, for
two triples on M, with the same cleaned list have the same value on every U.
The sequence over a relatively compact open: the value and its four order/erase exports #
The sequence BMO_{n,m}(M, 𝓘, m, E) over the relatively compact open U
[Kol07, Theorem 107]: the three steps run as one chain of links on shrinking opens containing
closure U (the descent of the first step, stepAChainState, continued by the descent of the
separation step and the link of the monomial step, step23ChainState, at the threshold t = m),
and the terminal state, whose induced triple has order < m (step23ChainState_ord_lt), is
restricted to U and cleaned of empty blow-ups (TerminalState.valueOn). The order reductions
bo, the pull-back property of the nonmonomial part hcomp, the two transform identities hid
and hidN, and the monomial procedure st3 are parameters. The scheme-theoretic counterpart is
Hironaka.BMO.bmoSeq.
Equations
- Hironaka.Manifold.BMO.bmoSeqOn T m hT bo hcomp hid hidN st3 U hU = { toChainState := Hironaka.Manifold.BMO.step23ChainState T m hT bo ⋯ ⋯ ⋯ st3 m ⋯ ⋯ U hU, ord_lt := ⋯ }.valueOn ⋯
Instances For
The sequence over U is a smooth blow-up sequence of order ≥ m for the triple restricted to
U [Kol07, Definition 66 (2′)–(4′)] (TerminalState.valueOn_isOfOrderGe).
The sequence has no empty blow-ups [Kol07, 32].
The deletion of empty blow-ups is the identity on the sequence.
Clause (1) of [Kol07, Theorem 107] on the sequence over U, pointwise: the marked transform at
the last stage has order < m at every point (TerminalState.ord_lt_valueOn).