The rounds on the nonmonomial part: transport of one link of the descent

The second condition of [Kol07, 34.1] and the compatibility [Wlo09, Theorem 2.0.3 (4)] for one link of the descent of the rounds on the nonmonomial part ([Kol07, 111, Step 1]; [Wlo09, Theorem 7.4.1]): along a local analytic isomorphism h : N → M carrying an open W' ⊆ N into W ⊆ M, a descent state over W' for the pulled-back triple and a descent state over W at the same bound d, whose lists agree up to empty blow-ups after pulling back, keep that relation through one link (descentLink_rel; smaller opens V' ⊆ W', V ⊆ W with h(V') ⊆ V). This is ChainState.link_rel with the family read at the nonmonomial triple of the induced triple (nonmonomialFunctor): the list algebra is BlowUpSequence.shrinkAppend_eraseEmpty_pullback unchanged; the two appended values of the round are compared by AnalyticFamilyFunctor.inducedValue_rel for that functor, whose class proofs are the invariants of the descent (BState.nonmonomialClass), transported to the cleaned lists by nonmonomialClass_induced_eraseEmpty (the nonmonomial part is indifferent to empty members and commutes with pull-back: NonmonomialIndiff.lean, NonmonomialComap).

The relation is the inductive step of the compatibility of the values and of the independence of the value from the chain and the outer open; the alignment of two descents of different lengths (the empty links above the smaller bound) is StepAAlign.lean.

The class of the induced triple of the cleaned list

theorem Hironaka.Manifold.BMOmod.nonmonomialClass_induced_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) {X : AnalyticManifold 𝕜 (Fin n → 𝕜)} (TW : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X) (m : ℕ) (L : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X) (hL : L.toSuccession.IsOfOrderGe TW.I m TW.F.idealSheaf) (hLe : L.eraseEmpty.toSuccession.IsOfOrderGe TW.I m TW.F.idealSheaf) {d : ℕ} (hD : NonmonomialClass d (TW.induced m L hL)) : NonmonomialClass d (TW.induced m L.eraseEmpty hLe)

The invariant of the descent passes to the cleaned list ([Kol07, 32] and its counterpart for boundary members): the induced triple of the list is the induced triple of the cleaned list pulled back along eraseEmptyLast, up to empty boundary members (induced_eq_pullback_induced_eraseEmpty); the nonmonomial triple ignores the empty members (nonmonomialClass_of_isEmptyExtension) and commutes with the pull-back (NonmonomialComap); and the order bound and the finiteness of the nonempty members transport along the diffeomorphism (ord_pullback_of_isLocalDiffeomorphAt).

One link

theorem Hironaka.Manifold.BMOmod.BState.descentLink_L {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} {m : ℕ} (bo : (d : ℕ) → BOanFam 𝕜 n d) (hid : NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hT : Manifold.AnalyticTriple.BMOClass m T) (hm : 1 ≤ m) {W : TopologicalSpace.Opens M.carrier} {d : ℕ} (st : BState T m W d) {V : TopologicalSpace.Opens M.carrier} (hV : IsCompact (closure ↑V)) (hVW : closure ↑V ⊆ ↑W) (hmd : m ≤ d) : (descentLink ⋯ bo ⋯ st hV hVW hT hm hmd).L = st.L.shrinkAppend (M.restrictLE ⋯) ⋯ (roundValue bo st hV hVW hT ⋯)

One link is the shrink-and-append step with the value of the round.

theorem Hironaka.Manifold.BMOmod.descentLink_rel {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) {M N : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} {m : ℕ} (bo : (d : ℕ) → BOanFam 𝕜 n d) (hid : NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hT : Manifold.AnalyticTriple.BMOClass m T) (hm : 1 ≤ m) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑h) {T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N} (hT'eq : T' = T.pullback h hh) (hT' : Manifold.AnalyticTriple.BMOClass m T') {W : TopologicalSpace.Opens M.carrier} {W' : TopologicalSpace.Opens N.carrier} (hWW' : ⇑h '' ↑W' ⊆ ↑W) {d : ℕ} (st : BState T m W d) (st' : BState T' m W' d) (hrel : st'.L.eraseEmpty = (st.L.pullback (AnalyticMap.restrictMap h W' W hWW') ⋯).eraseEmpty) {V : TopologicalSpace.Opens M.carrier} (hV : IsCompact (closure ↑V)) (hVW : closure ↑V ⊆ ↑W) {V' : TopologicalSpace.Opens N.carrier} (hV' : IsCompact (closure ↑V')) (hV'W' : closure ↑V' ⊆ ↑W') (hVV' : ⇑h '' ↑V' ⊆ ↑V) (hmd : m ≤ d) : (BState.descentLink ⋯ bo ⋯ st' hV' hV'W' hT' hm hmd).L.eraseEmpty = ((BState.descentLink ⋯ bo ⋯ st hV hVW hT hm hmd).L.pullback (AnalyticMap.restrictMap h V' V hVV') ⋯).eraseEmpty

The second condition of [Kol07, 34.1] for one link of the descent: the relation "the cleaned list over W' is the cleaned pull-back of the list over W" along a local analytic isomorphism h with h(W') ⊆ W, between two states at the same bound d, is kept by one link, for smaller opens V ⊆ W, V' ⊆ W' with h(V') ⊆ V. The list algebra is shrinkAppend_eraseEmpty_pullback; the two values of the round are compared by inducedValue_rel for the family read at the nonmonomial triple (nonmonomialFunctor; the class proofs from the invariants, nonmonomialClass_induced_eraseEmpty for the cleaned list). The triple over N is any triple equal to the pull-back (hT'eq, substituted), so the case of one manifold reads with h the identity.