The separation and monomial steps: naturality of the links and of the continuation

Clause (2) of the marked order reduction theorem [Kol07, Theorem 107] and the compatibility of the sequences over different relatively compact opens [Wlo09, Theorem 2.0.3 (4)] require the runs of the three steps over two opens, or across a local analytic isomorphism, to agree up to the deletion of empty blow-ups [Kol07, 34.1]. For the first step this is proved by aligning two chains link by link (descentStateAux_rel, descentStateAux_L_indiff); this module continues the alignment through the links of the separation step and of the monomial step. Each fact is the corresponding fact for a link of the first step with the family of the round replaced, sepFunctor for the separation step and the functor of MonomialStep3Fam for the monomial step:

• commutation with local analytic isomorphisms for one link (SState.sepLink_rel, SState.step3Link_rel), the second condition of [Kol07, 34.1]: the relation "the list over W' with empty blow-ups deleted is the pull-back of the list over W with empty blow-ups deleted", along a local analytic isomorphism h with h(W') ⊆ W, is kept by one link, for V ⊆ W, V' ⊆ W' with h(V') ⊆ V. The list algebra is BlowUpSequence.shrinkAppend_eraseEmpty_pullback; the two values of the round are compared by AnalyticFamilyFunctor.inducedValue_rel for the family of the round (its two naturality properties and the closure of its class under pull-back), and the class of the induced triple of the cleaned list is sepClass_induced_eraseEmpty;
• indifference to empty boundary members for one link (SState.sepLink_L_indiff, SState.step3Link_L_indiff; the counterpart, for boundary members, of [Kol07, 32]): two states with the same list, for T and for T with its boundary replaced by an empty extension, link to the same list, since the family of the round is indifferent to empty members;
• the continuation step23Aux: both facts link by link, sepDescentAux_rel and sepDescentAux_L_indiff by induction along the descent, then step23Aux_rel and step23Aux_L_indiff through the link of the monomial step. Both continuations run the same number of links, so no offset of bounds is needed.

These are the inputs of bmoSeqOn_compat, bmoSeqOn_pullback and bmoSeqOn_indiff.

The class of the induced triple of the cleaned list

theorem Hironaka.Manifold.BMO.sepClass_induced_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (hcomp : BMOmod.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) {s : ℕ} (hD : SepClass m s (TW.induced m L hL)) : SepClass m s (TW.induced m L.eraseEmpty hLe)

The class of the round of the separation step passes to the cleaned list: the induced triple of a list is, up to empty boundary members, the induced triple of the list with empty blow-ups deleted, pulled back along the diffeomorphism eraseEmptyLast of the last stages (AnalyticTriple.induced_eq_pullback_induced_eraseEmpty); the separating triple ignores empty members (sepClass_of_isEmptyExtension) and commutes with pull-back (sepTripleAt_pullback), and the order bound and the finiteness of the nonempty members transport along the diffeomorphism.

theorem Hironaka.Manifold.BMO.bmoClass_induced_of_bmoClass {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticManifold 𝕜 (Fin n → 𝕜)} {m : ℕ} {T₀ : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X} (hT₀ : Manifold.AnalyticTriple.BMOClass m T₀) (L' : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X) (hL' : L'.toSuccession.IsOfOrderGe T₀.I m T₀.F.idealSheaf) : Manifold.AnalyticTriple.BMOClass m (T₀.induced m L' hL')

The induced triple of a triple of the marked class is in the marked class (the mark, and the finiteness of the nonempty members).

theorem Hironaka.Manifold.BMO.bmoClass_pullback_of_isLocalDiffeomorph {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticManifold 𝕜 (Fin n → 𝕜)} {m : ℕ} {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T₀ : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X} (hT₀ : Manifold.AnalyticTriple.BMOClass m T₀) (g : AnalyticMap N X) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g) : Manifold.AnalyticTriple.BMOClass m (T₀.pullback g hg)

The marked class is closed under pull-back along local analytic isomorphisms.

One link: commutation with local analytic isomorphisms

theorem Hironaka.Manifold.BMO.SState.sepLink_rel {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M N : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} {m : ℕ} (hT : Manifold.AnalyticTriple.BMOClass m T) (bo : (d : ℕ) → BOanFam 𝕜 n d) (hcomp : BMOmod.NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hidN : NonmonomialTransformIdentityMod (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (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) {s : ℕ} (st : SState T m W s) (st' : SState T' m W' s) (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) (hs : 1 ≤ s) : (sepLink hT' bo ⋯ ⋯ st' hV' hV'W' hm hs).L.eraseEmpty = ((sepLink hT bo ⋯ ⋯ st hV hVW hm hs).L.pullback (AnalyticMap.restrictMap h V' V hVV') ⋯).eraseEmpty

Commutation with local analytic isomorphisms for one link of the separation step (the second condition of [Kol07, 34.1]): the relation "the list over W' with empty blow-ups deleted is the pull-back along h|_{W'} of the list over W with empty blow-ups deleted", between two states at the same separation bound s, for T and for a triple equal to the pull-back of T along h, is kept by one link, for V ⊆ W, V' ⊆ W' with h(V') ⊆ V. The list algebra is BlowUpSequence.shrinkAppend_eraseEmpty_pullback; the two values of the round are compared by inducedValue_rel for sepFunctor (its two naturality properties, the closure of the class under pull-back, and sepClass_induced_eraseEmpty for the cleaned list).

theorem Hironaka.Manifold.BMO.SState.step3Link_rel {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M N : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} {m : ℕ} (hT : Manifold.AnalyticTriple.BMOClass m T) (st3 : MonomialStep3Fam 𝕜 n 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) (st : SState T m W 0) (st' : SState T' m W' 0) (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) : (step3Link hT' st3 st' hV' hV'W').L.eraseEmpty = ((step3Link hT st3 st hV hVW).L.pullback (AnalyticMap.restrictMap h V' V hVV') ⋯).eraseEmpty

The same for the link of the monomial step, with the functor of the procedure st3.functor in place of sepFunctor (inducedValue_rel with st3.commutesWithLocalIsos and st3.indifferentToEmptyMembers).

One link: indifference to empty boundary members

theorem Hironaka.Manifold.BMO.SState.sepLink_L_indiff {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} {m : ℕ} (hT : Manifold.AnalyticTriple.BMOClass m T) (bo : (d : ℕ) → BOanFam 𝕜 n d) (hcomp : BMOmod.NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hidN : NonmonomialTransformIdentityMod (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hm : 1 ≤ m) (F' : Manifold.HypersurfaceFamily M.carrier) (hsnc' : Manifold.HypersurfaceFamily.IsSnc (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) F') (e : F'.ι ↪o T.F.ι) (he : ∀ (i : F'.ι), T.F.hyp (e i) = F'.hyp i) (he' : ∀ b ∉ Set.range ⇑e, T.F.hyp b = ∅) (hT' : Manifold.AnalyticTriple.BMOClass m (BDan.withBoundary T F' hsnc')) {W : TopologicalSpace.Opens M.carrier} {s : ℕ} (st : SState T m W s) (st' : SState (BDan.withBoundary T F' hsnc') m W s) (hL : st.L = st'.L) {V : TopologicalSpace.Opens M.carrier} (hV : IsCompact (closure ↑V)) (hVW : closure ↑V ⊆ ↑W) (hs : 1 ≤ s) : (sepLink hT bo ⋯ ⋯ st hV hVW hm hs).L = (sepLink hT' bo ⋯ ⋯ st' hV hVW hm hs).L

Indifference to empty boundary members for one link of the separation step (the counterpart, for boundary members, of [Kol07, 32]): two states with the same list, for T and for T with its boundary replaced by an empty extension F', link to the same list. The restricted triples over W are again related by a boundary change along e, and the value of the round is the value of sepFunctor at the induced triples (IndifferentToEmptyMembers.seqOn_induced_indiff with sepFunctor_indifferentToEmptyMembers).

theorem Hironaka.Manifold.BMO.SState.step3Link_L_indiff {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} {m : ℕ} (hT : Manifold.AnalyticTriple.BMOClass m T) (st3 : MonomialStep3Fam 𝕜 n m) (F' : Manifold.HypersurfaceFamily M.carrier) (hsnc' : Manifold.HypersurfaceFamily.IsSnc (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) F') (e : F'.ι ↪o T.F.ι) (he : ∀ (i : F'.ι), T.F.hyp (e i) = F'.hyp i) (he' : ∀ b ∉ Set.range ⇑e, T.F.hyp b = ∅) (hT' : Manifold.AnalyticTriple.BMOClass m (BDan.withBoundary T F' hsnc')) {W : TopologicalSpace.Opens M.carrier} (st : SState T m W 0) (st' : SState (BDan.withBoundary T F' hsnc') m W 0) (hL : st.L = st'.L) {V : TopologicalSpace.Opens M.carrier} (hV : IsCompact (closure ↑V)) (hVW : closure ↑V ⊆ ↑W) : (step3Link hT st3 st hV hVW).L = (step3Link hT' st3 st' hV hVW).L

The same for the link of the monomial step (seqOn_induced_indiff with st3.indifferentToEmptyMembers).

The continuation along a chain: both facts link by link

theorem Hironaka.Manifold.BMO.sepDescentAux_rel {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M N : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} {m : ℕ} (hT : Manifold.AnalyticTriple.BMOClass m T) (bo : (d : ℕ) → BOanFam 𝕜 n d) (hcomp : BMOmod.NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hidN : NonmonomialTransformIdentityMod (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (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) (hW : ∀ (k : ℕ), IsCompact (closure ↑(W k))) (r : ℕ) (hWsub : ∀ k < r, closure ↑(W (k + 1)) ⊆ ↑(W k)) (X : ℕ → TopologicalSpace.Opens N.carrier) (hX : ∀ (k : ℕ), IsCompact (closure ↑(X k))) (hXsub : ∀ k < r, closure ↑(X (k + 1)) ⊆ ↑(X k)) (hXW : ∀ (j : ℕ), ⇑h '' ↑(X j) ⊆ ↑(W j)) (S₀ : ℕ) (st₀ : SState T m (W 0) S₀) (st₀' : SState T' m (X 0) S₀) (hrel : st₀'.L.eraseEmpty = (st₀.L.pullback (AnalyticMap.restrictMap h (X 0) (W 0) ⋯) ⋯).eraseEmpty) (j : ℕ) (hj : j ≤ r) (hjS : j ≤ S₀) : (sepDescentAux hT' bo ⋯ ⋯ hm X hX r hXsub S₀ st₀' j hj hjS).L.eraseEmpty = ((sepDescentAux hT bo ⋯ ⋯ hm W hW r hWsub S₀ st₀ j hj hjS).L.pullback (AnalyticMap.restrictMap h (X j) (W j) ⋯) ⋯).eraseEmpty

The descent of the separation step keeps the relation of SState.sepLink_rel link by link.

theorem Hironaka.Manifold.BMO.step23Aux_rel {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M N : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} {m : ℕ} (hT : Manifold.AnalyticTriple.BMOClass m T) (bo : (d : ℕ) → BOanFam 𝕜 n d) (hcomp : BMOmod.NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hidN : NonmonomialTransformIdentityMod (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (st3 : MonomialStep3Fam 𝕜 n m) (hm : 1 ≤ m) (t : ℕ) (ht : 1 ≤ t) (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) (hW : ∀ (k : ℕ), IsCompact (closure ↑(W k))) (hWsub : ∀ k < t, closure ↑(W (k + 1)) ⊆ ↑(W k)) (X : ℕ → TopologicalSpace.Opens N.carrier) (hX : ∀ (k : ℕ), IsCompact (closure ↑(X k))) (hXsub : ∀ k < t, closure ↑(X (k + 1)) ⊆ ↑(X k)) (hXW : ∀ (j : ℕ), ⇑h '' ↑(X j) ⊆ ↑(W j)) (st₀ : BMOmod.BState T m (W 0) (t - 1)) (st₀' : BMOmod.BState T' m (X 0) (t - 1)) (hrel : st₀'.L.eraseEmpty = (st₀.L.pullback (AnalyticMap.restrictMap h (X 0) (W 0) ⋯) ⋯).eraseEmpty) : (step23Aux hT' bo ⋯ ⋯ st3 hm t ht X hX hXsub st₀').L.eraseEmpty = ((step23Aux hT bo ⋯ ⋯ st3 hm t ht W hW hWsub st₀).L.pullback (AnalyticMap.restrictMap h (X t) (W t) ⋯) ⋯).eraseEmpty

Commutation with local analytic isomorphisms for the continuation: two continuations by the separation and monomial steps, over N and over M, along a local analytic isomorphism h with h(X j) ⊆ W j, from states of the first step whose lists with empty blow-ups deleted are related by pull-back along h, end in states whose lists are so related. Both continuations run the same number t of links, so no offset of bounds is needed.

theorem Hironaka.Manifold.BMO.sepDescentAux_L_indiff {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} {m : ℕ} (hT : Manifold.AnalyticTriple.BMOClass m T) (bo : (d : ℕ) → BOanFam 𝕜 n d) (hcomp : BMOmod.NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hidN : NonmonomialTransformIdentityMod (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hm : 1 ≤ m) (F' : Manifold.HypersurfaceFamily M.carrier) (hsnc' : Manifold.HypersurfaceFamily.IsSnc (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) F') (e : F'.ι ↪o T.F.ι) (he : ∀ (i : F'.ι), T.F.hyp (e i) = F'.hyp i) (he' : ∀ b ∉ Set.range ⇑e, T.F.hyp b = ∅) (hT' : Manifold.AnalyticTriple.BMOClass m (BDan.withBoundary T F' hsnc')) (W : ℕ → TopologicalSpace.Opens M.carrier) (hW : ∀ (k : ℕ), IsCompact (closure ↑(W k))) (r : ℕ) (hWsub : ∀ k < r, closure ↑(W (k + 1)) ⊆ ↑(W k)) (S₀ : ℕ) (st₀ : SState T m (W 0) S₀) (st₀' : SState (BDan.withBoundary T F' hsnc') m (W 0) S₀) (hL : st₀.L = st₀'.L) (j : ℕ) (hj : j ≤ r) (hjS : j ≤ S₀) : (sepDescentAux hT bo ⋯ ⋯ hm W hW r hWsub S₀ st₀ j hj hjS).L = (sepDescentAux hT' bo ⋯ ⋯ hm W hW r hWsub S₀ st₀' j hj hjS).L

The descent of the separation step is indifferent to empty boundary members link by link.

theorem Hironaka.Manifold.BMO.step23Aux_L_indiff {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} {m : ℕ} (hT : Manifold.AnalyticTriple.BMOClass m T) (bo : (d : ℕ) → BOanFam 𝕜 n d) (hcomp : BMOmod.NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hidN : NonmonomialTransformIdentityMod (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (st3 : MonomialStep3Fam 𝕜 n m) (hm : 1 ≤ m) (F' : Manifold.HypersurfaceFamily M.carrier) (hsnc' : Manifold.HypersurfaceFamily.IsSnc (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) F') (e : F'.ι ↪o T.F.ι) (he : ∀ (i : F'.ι), T.F.hyp (e i) = F'.hyp i) (he' : ∀ b ∉ Set.range ⇑e, T.F.hyp b = ∅) (hT' : Manifold.AnalyticTriple.BMOClass m (BDan.withBoundary T F' hsnc')) (t : ℕ) (ht : 1 ≤ t) (W : ℕ → TopologicalSpace.Opens M.carrier) (hW : ∀ (k : ℕ), IsCompact (closure ↑(W k))) (hWsub : ∀ k < t, closure ↑(W (k + 1)) ⊆ ↑(W k)) (st₀ : BMOmod.BState T m (W 0) (t - 1)) (st₀' : BMOmod.BState (BDan.withBoundary T F' hsnc') m (W 0) (t - 1)) (hL : st₀.L = st₀'.L) : (step23Aux hT bo ⋯ ⋯ st3 hm t ht W hW hWsub st₀).L = (step23Aux hT' bo ⋯ ⋯ st3 hm t ht W hW hWsub st₀').L

Indifference to empty boundary members for the continuation: two continuations along the same chain from states with the same list, for T and for T with its boundary replaced by an empty extension, have the same list.