The rounds on the nonmonomial part: the empty-link lemma and the alignment of two descents #
The empty-link lemma: the value of the order reduction BO_{n,d} on an open where the ideal has
order < d everywhere is the empty list, since its centres lie where the order is ≥ d
([Kol07, Definition 66 (4′)], the order clause of the family) and none of them is empty
([Kol07, 32], the absence of empty centres), so there is no first centre (BOanFam.seqOn_eq_nil,
BState.roundValue_eq_nil). Hence a link of the descent at a bound d above the maximal order of
N(𝓘) appends nothing: the list of the state is only restricted
(BState.descentLink_eraseEmpty_of_roundValue_nil).
The alignment of two descents (descentStateAux_rel): along a local analytic isomorphism
h : N → M, a descent over N for the pulled-back triple from a bound DX along a chain X, and
a descent over M from a bound D ≤ DX along a chain W with h(X j) ⊆ W (j − (DX − D)),
produce lists which agree up to empty blow-ups after pulling back: the first DX − D links over
N are empty (the bound D holds on X j through h), and from then on the two descents run at
the same bound and descentLink_rel carries the relation link by link (the bounds identified by
BState.castBound). This is the inductive engine of the compatibility of the values, of the
independence of the value from the outer open and the chain, and of the commutation with local
isomorphisms (the second condition of [Kol07, 34.1]); the applications are in StepACompat.lean,
StepAIndep.lean and StepAComm.lean.
The empty-link lemma #
The empty-link lemma ([Kol07, Definition 66 (4′)] with [Kol07, 32]): the value of BO_{n,d}
on an open where ord 𝓘 < d everywhere is the empty list, since a first centre would lie where the
order is ≥ d (isOfOrderGe, ordAlongIdeal_le_ord_of_mem_support) and be nonempty
(noEmptyCenters).
The empty-link lemma at a link of the descent: when the invariant holds at a bound D < d, the
value of the round is the empty list.
A link whose round has the empty value restricts the list (shrinkAppend with the empty list,
concat_nil_right); up to empty blow-ups it is the cleaned list restricted.
The invariant through eraseEmpty and along pull-backs #
The order bound on N(𝓘) pulls back along local analytic isomorphisms (NonmonomialComap,
ord_pullback_of_isLocalDiffeomorphAt).
The bound transports along an equality of lists (a subst).
The bound at the induced triple of the empty list is the bound on the triple
(induced_nil).
The ideal N of the induced triple is the pull-back of the ideal N of the induced triple of
the cleaned list along eraseEmptyLast ([Kol07, 32] and its counterpart for boundary members):
the induced triple is that
pull-back up to empty boundary members (induced_eq_pullback_induced_eraseEmpty), N ignores them
(nonmonomialTriple_eq_of_isEmptyExtension) and commutes with the pull-back (NonmonomialComap).
Every identification goes through the projection lemmas by congrArg.
The bound at the induced triple of the cleaned list gives the bound at the induced triple of the
list (nonmonomialTriple_induced_I_eq_pullback_eraseEmpty,
ord_pullback_of_isLocalDiffeomorphAt).
The converse: the bound at the induced triple of the list gives the bound at the induced triple
of the cleaned list (eraseEmptyLast is onto).
Re-typing a state at an equal bound #
The same state at a propositionally equal bound (the bounds of two aligned descents are equal natural numbers, not the same terms).
Equations
- Hironaka.Manifold.BMOmod.BState.castBound T m e st = { toChainState := st.toChainState, bound := ⋯ }
Instances For
The link of a re-typed state is the re-typed link (a substitution).
The alignment of two descents #
The right-hand side of the alignment: the k-th state of the descent over M, pulled back
along h to the j-th open of the chain over N and cleaned of empty blow-ups (its type does not
depend on k).
Equations
- One or more equations did not get rendered due to their size.
Instances For
alignRHS depends on the index k only through its value (a substitution).
At k = 0 the right-hand side is nil (the initial state has no blow-ups).
The alignment of two descents (the inductive engine of the compatibility of the values and
of the second condition of [Kol07, 34.1] for the rounds): the j-th state of the descent over N
(bound DX, chain X) and the (j − (DX − D))-th state of the descent over M (bound D ≤ DX,
chain W), pulled back along h, agree up to empty blow-ups. For j < DX − D the link over N
runs at a bound above D, which bounds ord N on X j through h, so its value is the empty list
(the empty-link lemma) and both sides stay empty; from j = DX − D on the two descents run at the
same bound and descentLink_rel carries the relation.