The rounds on the nonmonomial part: one link of the descent #
One round of order reduction on the nonmonomial part N(π) at the bound d ([Kol07, 111, Step 1];
the first phase of the modified algorithm of [Wlo09, Theorem 7.4.1]), as one link of a shrinking
chain W β closure V of relatively compact opens (the shape of ChainState.link): the state
carries, besides the list and its order clause, the invariant that the nonmonomial part of the
induced ideal has order β€ d everywhere on the last stage (BState). So the nonmonomial triple of
the induced triple lies in the domain of BO_{n,d} globally (BState.boClass_nonmonomial), the
order reduction bo d is read on the lifted range of the inclusion V β W (liftRange, relatively
compact), the list is restricted to V and the value appended (shrinkAppend), and
- the order clause
β₯ mfor(π|V, m)holds by the order transfer (isOfOrderGe_of_nonmonomial: the value is of orderβ₯ dfor(N, d), hence of orderβ₯ mfor(π, m), the transform identity and the invariant supplying its hypotheses) andisOfOrderGe_shrinkAppend; - the invariant descends to
d β 1: at the last stage of the value,bo.ord_ltbounds the marked transform of(N, d)by< d; the transform identity at the last stage turns this into the bound on the nonmonomial part of the marked transform of(π, m), which is pulled back along the corestricted lift (induced_pullback,ord_pullback_of_isLocalDiffeomorphAt) and passed through the concatenation (nonmonomialOrdLe_induced_concat).
The descent d = D, D β 1, β¦, t (StepAChain.lean) visits every d; at a d above the current
maximal order of N(π) the order clause and the absence of empty centres force the value to be the
empty list (BOanFam.seqOn_eq_nil), so the nonempty links are the rounds of the sources at
d = max-ord N(π), in their order.
The nonmonomial part commutes with pull-back along a local analytic isomorphism
(NonmonomialComap, a parameter here, proved in nonmonomialComap_inhabitant). Every
identification of (nonmonomialTriple X).F with X.F goes through the projection lemma
nonmonomialTriple_F by congrArg before any exact: otherwise the elaborator unfolds
nonmonomialTriple X against X through the structures, and elaboration becomes very slow.
The nonmonomial part commutes with pull-back along a local analytic isomorphism: the
nonmonomial triple of a pulled-back triple is the pull-back of the nonmonomial triple (the
decomposition of [Kol07, DefinitionβLemma 110] is local). The rounds take the predicate as a
parameter; nonmonomialComap_inhabitant proves it at the standard model.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The boundary of a pulled-back nonmonomial triple is the boundary of the pulled-back triple: the
nonmonomial part keeps the boundary (nonmonomialTriple_F), transported by congrArg rather than
by rfl, which would unfold the triple against its nonmonomial triple through the structures.
A member of the pulled-back family is nonempty only if the member is, so finitely many nonempty
members pull back to finitely many (the boundary clause of BOClass pulls back).
The state of the descent at the bound d over the open W: a chain state (the list built
so far on M.restrict W, of order β₯ m for (π|W, m)) whose induced triple has nonmonomial part
of order β€ d at every point of the last stage.
- 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
- bound : NonmonomialOrdLe (ChainState.inducedTriple T m self.toChainState) d
The invariant:
max-ord N(π_ind) β€ dglobally on the last stage.
Instances For
The initial state on W β Uβ: the empty list, the bound roundOrderOn T Uβ (the maximum of
ord N(π) on the closure of Uβ, ord_le_roundOrderOn).
Equations
- Hironaka.Manifold.BMOmod.BState.initial T m hcomp hUβ hWU = { toChainState := Hironaka.Manifold.ChainState.init T m W, bound := β― }
Instances For
The invariant puts the nonmonomial triple of the induced triple in the domain of BO_{n,d}
globally on the last stage (the boundary clause from the marked class BMOClass, through
finite_nonempty_totalTransformSeqFrom).
The reading open of the link: the lifted range of the inclusion V β W at the last stage.
Equations
- st.liftOpen hVW = st.L.liftRange (M.restrictLE β―) β―
Instances For
The invariant restricted to the reading open (the maximal-order hypothesis of the transform identity).
The value of the round: the order reduction BO_{n,d} of the nonmonomial triple of the
induced triple, read on the reading open ("apply order reduction (68) to N(I)",
[Kol07, 111, Step 1]).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The value is of order β₯ d for the nonmonomial triple of the restricted induced triple
(bo.isOfOrderGe; the identifications of ideal and boundary rewritten by their lemmas before the
exact).
The order transfer at the round: the value is of order β₯ m for the restricted induced triple
itself (isOfOrderGe_of_nonmonomial, with m β€ d).
The list restricted to V is of order β₯ m for (π|V, m) (the input of
induced_pullback).
The restricted induced triple pulled back along the corestricted lift is the induced triple of
the restricted list (pullback_pullback, inclusion_comp_liftCorestrict, induced_pullback,
pullback_inclusion_restrictLE).
One link of the descent at the bound d β₯ m ([Kol07, 111, Step 1];
[Wlo09, Theorem 7.4.1]): the value of the round, read on the lifted range of V β W, is appended
to the list restricted to V (shrinkAppend); the order clause by the order transfer and
isOfOrderGe_shrinkAppend; the invariant descends to d β 1 (bo.ord_lt at the last stage, the
transform identity, the transport along the lift and through the concatenation).
Equations
- One or more equations did not get rendered due to their size.