The naturality of the sequence over an open: compatibility, local isomorphisms, indifference

Beyond the order and erasure facts, the structure BMOanFam reads three properties of the sequence bmoSeqOn over a relatively compact open:

• compatibility (CompatibleFamily.compat): the sequence over U ≤ V is the sequence over V restricted to U and cleaned of empty blow-ups ([Wlo09, Theorem 2.0.3 (4)], [Wlo09, Definition 3.2.6]);
• commutation with local analytic isomorphisms (CommutesWithLocalIsos): for a pull-back T' of the triple along a local analytic isomorphism g, the sequence over U' is the sequence over g(U') pulled back along g|_{U'} and cleaned ([Kol07, Theorem 107 (2)], [Kol07, 34.1]);
• indifference to empty boundary members (IndifferentToEmptyMembers): replacing the boundary by an empty extension does not change the sequence (the counterpart, for boundary members, of [Kol07, 32]).

The substance is the alignment of two runs of the three steps, the argument behind the second condition of [Kol07, 34.1]. For the first step it is made by a virtual descent over a pair of opens: a chain which maps into the canonical chains of both opens link by link, on which a third run is aligned with each of the two real runs (descentStateAux_rel). Here the virtual run is continued through the separation and monomial steps (step23Aux_rel, step23Aux_L_indiff):

• compatibility. For U ≤ V the virtual descent of the first step runs over the join chain stepAJoin U hU V hV from the larger of the two bounds. It is continued along bmoJoinCont: the exit open of the join descent, then the shrinkings of closure U inside it met with both canonical continuation chains, so that it maps into each of them link by link; step23Aux_rel along the identity carries the alignment to the terminal states (bmoJoinTerminal_rel_left, bmoJoinTerminal_rel_right). Both real sequences are then read off the one virtual terminal state on U (valueOn_eq_of_rel_id), and valueOn_restrict, the compatibility for one terminal state, closes.
• local isomorphisms. The same over the source manifold, with the pre-join chain preJoin of the pair U' ⊆ N, g(U') ⊆ M for the pulled-back triple, continued along bmoPreJoinCont (met with the canonical continuation of U' and the g-preimage of that of g(U')); the alignments along the identity (bmoPreJoinTerminal_rel_left) and along g (bmoPreJoinTerminal_rel_right, the triple of the virtual run being the pulled-back triple by IsPullbackOf.eq), then valueOn_eq_of_rel_id and valueOn_pullback_of_rel'.
• indifference. The canonical chains of T and of the boundary-extended triple coincide, the bound being read on the nonmonomial ideal, which does not see the empty members (step2ChainOpens_withBoundary, from roundOrderOn_withBoundary); along the common chain from the common bound the two descents have the same lists (descentStateAux_L_indiff), and so do the two continuations (step23Aux_L_indiff). bmoTerminal_L_indiff states this as a heterogeneous equality across the propositionally equal chains, which the value discharges by substituting the terminal open.

Three more transports of the value

theorem Hironaka.Manifold.TerminalState.valueOn_restrict {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {T : Manifold.AnalyticTriple ψ₀ M} {m : ℕ} {W V U : TopologicalSpace.Opens M.carrier} (st : TerminalState T m W) (hVW : V ≤ W) (hUV : U ≤ V) : st.valueOn ⋯ = ((st.valueOn hVW).pullback (M.restrictLE hUV) ⋯).eraseEmpty

The value on a smaller open is the value on the larger open restricted and cleaned: the compatibility for one terminal state (pullback_comp, eraseEmpty_pullback_eraseEmpty).

theorem Hironaka.Manifold.TerminalState.valueOn_eq_of_rel_id {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {T : Manifold.AnalyticTriple ψ₀ M} {m : ℕ} {W W' : TopologicalSpace.Opens M.carrier} (st : TerminalState T m W) (st' : TerminalState (T.pullback ContMDiffMap.id ⋯) m W') (hW'W : ⇑ContMDiffMap.id '' ↑W' ⊆ ↑W) (hrel : st'.L.eraseEmpty = (st.L.pullback (AnalyticMap.restrictMap ContMDiffMap.id W' W hW'W) ⋯).eraseEmpty) {U' : TopologicalSpace.Opens M.carrier} (hU'W' : U' ≤ W') (hU'W : U' ≤ W) : st'.valueOn hU'W' = st.valueOn hU'W

The identity form of valueOn_pullback_of_rel: a terminal state for the triple pulled back along the identity, whose cleaned list is the cleaned pull-back of the list of a terminal state along the inclusion W' ⊆ W, has the same value on every U' ≤ W': the inclusion composed with the restriction to U' is the restriction to U' (pullback_comp, pullback_congr, eraseEmpty_pullback_eraseEmpty).

theorem Hironaka.Manifold.TerminalState.valueOn_pullback_of_rel' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {T : Manifold.AnalyticTriple ψ₀ M} {m : ℕ} {N : AnalyticManifold 𝕜 E} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) {T' : Manifold.AnalyticTriple ψ₀ N} (hT'eq : T' = T.pullback g hg) {W : TopologicalSpace.Opens M.carrier} {W' : TopologicalSpace.Opens N.carrier} (hWW' : ⇑g '' ↑W' ⊆ ↑W) (st : TerminalState T m W) (st' : TerminalState T' m W') (hrel : st'.L.eraseEmpty = (st.L.pullback (AnalyticMap.restrictMap g W' W hWW') ⋯).eraseEmpty) {U' : TopologicalSpace.Opens N.carrier} (hU'W' : U' ≤ W') (hU'W : AnalyticMap.imageOpens g hg U' ≤ W) : st'.valueOn hU'W' = ((st.valueOn hU'W).pullback (AnalyticMap.restrictMap g U' (AnalyticMap.imageOpens g hg U') ⋯) ⋯).eraseEmpty

valueOn_pullback_of_rel for any triple equal to the pull-back, the form in which the alignment facts descentStateAux_rel and step23Aux_rel are stated.

The three naturality exports of the sequence

Every export is the corresponding proof for the first step (stepAFamOn_compat, stepAFamOn_pullback, stepAFamOn_indiff) with the continuation appended: the virtual descent of the pair (over the join chain stepAJoin, over the pre-join chain preJoin) is continued through the separation and monomial steps along a virtual continuation chain which maps into both real continuation chains link by link, the alignment of the first step (descentStateAux_rel) feeds that of the continuation (step23Aux_rel), and the transports of valueOn read the two real sequences off the one virtual terminal state.

The canonical terminal state, named

noncomputable def Hironaka.Manifold.BMO.bmoTerminal {𝕜 : 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 → 𝕜))) (hid : BMOmod.NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hidN : NonmonomialTransformIdentityMod (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (st3 : MonomialStep3Fam 𝕜 n m) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : TerminalState T m (step23ChainOpen T m U hU)

The canonical terminal state of the three steps over U at the threshold m (step23ChainState with its terminal bound); bmoSeqOn is its value on U.

Equations

• Hironaka.Manifold.BMO.bmoTerminal 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 := ⋯ }

theorem Hironaka.Manifold.BMO.bmoSeqOn_eq_valueOn {𝕜 : 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 → 𝕜))) (hid : BMOmod.NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hidN : NonmonomialTransformIdentityMod (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (st3 : MonomialStep3Fam 𝕜 n m) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : bmoSeqOn T m hT bo ⋯ ⋯ ⋯ st3 U hU = (bmoTerminal T m hT bo ⋯ ⋯ ⋯ st3 U hU).valueOn ⋯

Compatibility: the virtual join chain of the pair U ≤ V, continued

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.BMO.bmoJoinLinks {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (m : ℕ) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) : ℕ

The number of links of the virtual descent of the first step on the join chain, its bound the larger of the two.

Equations

• Hironaka.Manifold.BMO.bmoJoinLinks T m U hU V hV = Hironaka.Manifold.BMOmod.stepAJoinBound T U hU V hV + 1 - m

theorem Hironaka.Manifold.BMO.closure_subset_stepAJoin {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (hUV : U ≤ V) (j : ℕ) : closure ↑U ⊆ ↑(BMOmod.stepAJoin U hU V hV j)

noncomputable def Hironaka.Manifold.BMO.bmoJoinCont {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (m : ℕ) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (hUV : U ≤ V) : ℕ → TopologicalSpace.Opens M.carrier

The virtual continuation chain: the exit open of the join descent, then the shrinkings of closure U inside it met with both real continuation chains, so that it maps into each of them link by link.

Equations

• One or more equations did not get rendered due to their size.
• Hironaka.Manifold.BMO.bmoJoinCont T m U hU V hV hUV 0 = Hironaka.Manifold.BMOmod.stepAJoin U hU V hV (Hironaka.Manifold.BMO.bmoJoinLinks T m U hU V hV)

theorem Hironaka.Manifold.BMO.isCompact_closure_bmoJoinCont {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (m : ℕ) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (hUV : U ≤ V) (k : ℕ) : IsCompact (closure ↑(bmoJoinCont T m U hU V hV hUV k))

theorem Hironaka.Manifold.BMO.closure_bmoJoinCont_succ_subset {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (m : ℕ) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (hUV : U ≤ V) (k : ℕ) : closure ↑(bmoJoinCont T m U hU V hV hUV (k + 1)) ⊆ ↑(bmoJoinCont T m U hU V hV hUV k)

theorem Hironaka.Manifold.BMO.le_bmoJoinCont {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (m : ℕ) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (hUV : U ≤ V) (k : ℕ) : U ≤ bmoJoinCont T m U hU V hV hUV k

theorem Hironaka.Manifold.BMO.bmoJoinCont_le_left {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (m : ℕ) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (hUV : U ≤ V) (k : ℕ) : bmoJoinCont T m U hU V hV hUV k ≤ step2ChainOpens T m U hU k

theorem Hironaka.Manifold.BMO.bmoJoinCont_le_right {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (m : ℕ) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (hUV : U ≤ V) (k : ℕ) : bmoJoinCont T m U hU V hV hUV k ≤ step2ChainOpens T m V hV k

noncomputable def Hironaka.Manifold.BMO.bmoJoinExitState {𝕜 : 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 → 𝕜))) (hid : BMOmod.NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (hUV : U ≤ V) : BMOmod.BState (T.pullback ContMDiffMap.id ⋯) m (bmoJoinCont T m U hU V hV hUV 0) (m - 1)

The virtual descent of the first step for the pair (for T pulled back along the identity, on the join chain from the larger bound), read at its exit bound m − 1.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Hironaka.Manifold.BMO.bmoJoinTerminal {𝕜 : 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 → 𝕜))) (hid : BMOmod.NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hidN : NonmonomialTransformIdentityMod (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (st3 : MonomialStep3Fam 𝕜 n m) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (hUV : U ≤ V) : TerminalState (T.pullback ContMDiffMap.id ⋯) m (bmoJoinCont T m U hU V hV hUV m)

The virtual terminal state of the pair: the separation and monomial steps along the virtual continuation chain.

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.Manifold.BMO.bmoJoinExitState_rel_left {𝕜 : 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 → 𝕜))) (hid : BMOmod.NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (hUV : U ≤ V) : (bmoJoinExitState T m hT bo ⋯ ⋯ U hU V hV hUV).L.eraseEmpty = ((stepAExitState T m hT bo ⋯ ⋯ m ⋯ ⋯ U hU).L.pullback (AnalyticMap.restrictMap ContMDiffMap.id (bmoJoinCont T m U hU V hV hUV 0) (step2ChainOpens T m U hU 0) ⋯) ⋯).eraseEmpty

The alignment of the first step along the identity (descentStateAux_rel at the offset of bounds stepAJoinBound − stepABound, then alignRHS_congr to the number of links of U): the cleaned list of the virtual exit state is the cleaned pull-back of that of the real exit state of U.

theorem Hironaka.Manifold.BMO.bmoJoinExitState_rel_right {𝕜 : 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 → 𝕜))) (hid : BMOmod.NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (hUV : U ≤ V) : (bmoJoinExitState T m hT bo ⋯ ⋯ U hU V hV hUV).L.eraseEmpty = ((stepAExitState T m hT bo ⋯ ⋯ m ⋯ ⋯ V hV).L.pullback (AnalyticMap.restrictMap ContMDiffMap.id (bmoJoinCont T m U hU V hV hUV 0) (step2ChainOpens T m V hV 0) ⋯) ⋯).eraseEmpty

theorem Hironaka.Manifold.BMO.bmoJoinTerminal_rel_left {𝕜 : 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 → 𝕜))) (hid : BMOmod.NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hidN : NonmonomialTransformIdentityMod (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (st3 : MonomialStep3Fam 𝕜 n m) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (hUV : U ≤ V) : (bmoJoinTerminal T m hT bo ⋯ ⋯ ⋯ st3 U hU V hV hUV).L.eraseEmpty = ((bmoTerminal T m hT bo ⋯ ⋯ ⋯ st3 U hU).L.pullback (AnalyticMap.restrictMap ContMDiffMap.id (bmoJoinCont T m U hU V hV hUV m) (step23ChainOpen T m U hU) ⋯) ⋯).eraseEmpty

The relation carried through the separation and monomial steps (step23Aux_rel along the identity).

theorem Hironaka.Manifold.BMO.bmoJoinTerminal_rel_right {𝕜 : 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 → 𝕜))) (hid : BMOmod.NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hidN : NonmonomialTransformIdentityMod (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (st3 : MonomialStep3Fam 𝕜 n m) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (hUV : U ≤ V) : (bmoJoinTerminal T m hT bo ⋯ ⋯ ⋯ st3 U hU V hV hUV).L.eraseEmpty = ((bmoTerminal T m hT bo ⋯ ⋯ ⋯ st3 V hV).L.pullback (AnalyticMap.restrictMap ContMDiffMap.id (bmoJoinCont T m U hU V hV hUV m) (step23ChainOpen T m V hV) ⋯) ⋯).eraseEmpty

theorem Hironaka.Manifold.BMO.bmoSeqOn_compat {𝕜 : 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 → 𝕜))) (hid : BMOmod.NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hidN : NonmonomialTransformIdentityMod (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (st3 : MonomialStep3Fam 𝕜 n m) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (hUV : U ≤ V) : bmoSeqOn T m hT bo ⋯ ⋯ ⋯ st3 U hU = ((bmoSeqOn T m hT bo ⋯ ⋯ ⋯ st3 V hV).pullback (M.restrictLE hUV) ⋯).eraseEmpty

The compatibility CompatibleFamily.compat on the values ([Wlo09, Theorem 2.0.3 (4)], [Wlo09, Definition 3.2.6]; [Kol07, 34.1]): the sequence over U ≤ V is the sequence over V restricted to U and cleaned. Both are the virtual terminal state of the pair read on U (valueOn_eq_of_rel_id twice, then valueOn_restrict).

Local isomorphisms: the virtual pre-join chain of U' ⊆ N and g(U') ⊆ M, continued

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.BMO.bmoPreJoinLinks {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (m : ℕ) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g) (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')) : ℕ

The number of links of the virtual descent on the pre-join chain.

Equations

• Hironaka.Manifold.BMO.bmoPreJoinLinks T m g hg U' hU' = Hironaka.Manifold.BMOmod.preJoinBound T g hg U' hU' (Hironaka.Manifold.AnalyticMap.imageOpens g hg U') ⋯ + 1 - m

theorem Hironaka.Manifold.BMO.closure_subset_preJoin {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g) (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')) (j : ℕ) : closure ↑U' ⊆ ↑(BMOmod.preJoin g U' hU' (AnalyticMap.imageOpens g hg U') ⋯ j)

noncomputable def Hironaka.Manifold.BMO.bmoPreJoinCont {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (m : ℕ) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g) (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')) : ℕ → TopologicalSpace.Opens N.carrier

The virtual continuation chain over N: the exit open of the pre-join descent, then the shrinkings of closure U' met with the real continuation of U' and the g-preimage of the real continuation of g(U').

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.Manifold.BMO.isCompact_closure_bmoPreJoinCont {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (m : ℕ) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g) (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')) (k : ℕ) : IsCompact (closure ↑(bmoPreJoinCont T m g hg U' hU' k))

theorem Hironaka.Manifold.BMO.closure_bmoPreJoinCont_succ_subset {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (m : ℕ) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g) (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')) (k : ℕ) : closure ↑(bmoPreJoinCont T m g hg U' hU' (k + 1)) ⊆ ↑(bmoPreJoinCont T m g hg U' hU' k)

theorem Hironaka.Manifold.BMO.le_bmoPreJoinCont {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (m : ℕ) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g) (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')) (k : ℕ) : U' ≤ bmoPreJoinCont T m g hg U' hU' k

theorem Hironaka.Manifold.BMO.bmoPreJoinCont_le_left {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (m : ℕ) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g) (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')) (k : ℕ) : bmoPreJoinCont T m g hg U' hU' k ≤ step2ChainOpens (T.pullback g hg) m U' hU' k

theorem Hironaka.Manifold.BMO.image_bmoPreJoinCont_subset {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (m : ℕ) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g) (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')) (k : ℕ) : ⇑g '' ↑(bmoPreJoinCont T m g hg U' hU' k) ⊆ ↑(step2ChainOpens T m (AnalyticMap.imageOpens g hg U') ⋯ k)

noncomputable def Hironaka.Manifold.BMO.bmoPreJoinExitState {𝕜 : 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 → 𝕜))) (hid : BMOmod.NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g) (hT' : Manifold.AnalyticTriple.BMOClass m (T.pullback g hg)) (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')) : BMOmod.BState ((T.pullback g hg).pullback ContMDiffMap.id ⋯) m (bmoPreJoinCont T m g hg U' hU' 0) (m - 1)

The virtual descent of the first step for the pair (for the pulled-back triple pulled back once more along the identity, on the pre-join chain from the larger bound), read at its exit bound m − 1.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Hironaka.Manifold.BMO.bmoPreJoinTerminal {𝕜 : 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 → 𝕜))) (hid : BMOmod.NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hidN : NonmonomialTransformIdentityMod (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (st3 : MonomialStep3Fam 𝕜 n m) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g) (hT' : Manifold.AnalyticTriple.BMOClass m (T.pullback g hg)) (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')) : TerminalState ((T.pullback g hg).pullback ContMDiffMap.id ⋯) m (bmoPreJoinCont T m g hg U' hU' m)

The virtual terminal state of the pair over N.

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.Manifold.BMO.bmoPreJoinTerminal_rel_left {𝕜 : 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 → 𝕜))) (hid : BMOmod.NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hidN : NonmonomialTransformIdentityMod (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (st3 : MonomialStep3Fam 𝕜 n m) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g) (hT' : Manifold.AnalyticTriple.BMOClass m (T.pullback g hg)) (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')) : (bmoPreJoinTerminal T m hT bo ⋯ ⋯ ⋯ st3 g hg hT' U' hU').L.eraseEmpty = ((bmoTerminal (T.pullback g hg) m hT' bo ⋯ ⋯ ⋯ st3 U' hU').L.pullback (AnalyticMap.restrictMap ContMDiffMap.id (bmoPreJoinCont T m g hg U' hU' m) (step23ChainOpen (T.pullback g hg) m U' hU') ⋯) ⋯).eraseEmpty

The virtual terminal state aligned with the real terminal state of U' (for the pulled-back triple), along the identity of N (descentStateAux_rel and step23Aux_rel along the identity).

theorem Hironaka.Manifold.BMO.bmoPreJoinTerminal_rel_right {𝕜 : 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 → 𝕜))) (hid : BMOmod.NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hidN : NonmonomialTransformIdentityMod (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (st3 : MonomialStep3Fam 𝕜 n m) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g) (hT' : Manifold.AnalyticTriple.BMOClass m (T.pullback g hg)) (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')) : (bmoPreJoinTerminal T m hT bo ⋯ ⋯ ⋯ st3 g hg hT' U' hU').L.eraseEmpty = ((bmoTerminal T m hT bo ⋯ ⋯ ⋯ st3 (AnalyticMap.imageOpens g hg U') ⋯).L.pullback (AnalyticMap.restrictMap g (bmoPreJoinCont T m g hg U' hU' m) (step23ChainOpen T m (AnalyticMap.imageOpens g hg U') ⋯) ⋯) ⋯).eraseEmpty

The virtual terminal state aligned with the real terminal state of g(U') (for T), along g (descentStateAux_rel and step23Aux_rel along g; the triple of the virtual descent is the pulled-back triple by IsPullbackOf.eq, which is substituted inside).

theorem Hironaka.Manifold.BMO.bmoSeqOn_pullback {𝕜 : 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 → 𝕜))) (hid : BMOmod.NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hidN : NonmonomialTransformIdentityMod (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (st3 : MonomialStep3Fam 𝕜 n m) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g) {T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N} (hpull : T'.IsPullbackOf T g) (hT' : Manifold.AnalyticTriple.BMOClass m T') (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')) : bmoSeqOn T' m hT' bo ⋯ ⋯ ⋯ st3 U' hU' = ((bmoSeqOn T m hT bo ⋯ ⋯ ⋯ st3 (AnalyticMap.imageOpens g hg U') ⋯).pullback (AnalyticMap.restrictMap g U' (AnalyticMap.imageOpens g hg U') ⋯) ⋯).eraseEmpty

The commutation with local analytic isomorphisms ([Kol07, Theorem 107 (2)], [Kol07, 34.1]) in the form CommutesWithLocalIsos requires: for T' a pull-back of T along a local analytic isomorphism g, the sequence over U' is the sequence over g(U') pulled back along g|_{U'} and cleaned. Both are the virtual terminal state of the pair read on U' (valueOn_eq_of_rel_id along the identity of N, valueOn_pullback_of_rel' along g).

Indifference: the same chain from the same bound for the boundary-extended triple

theorem Hironaka.Manifold.BMO.step2ChainOpens_withBoundary {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (m : ℕ) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (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 = ∅) : step2ChainOpens (BDan.withBoundary T F' hsnc') m U hU = step2ChainOpens T m U hU

The canonical chains of T and of the boundary-extended triple coincide: the bound is read on the nonmonomial ideal, which does not see the empty members (roundOrderOn_withBoundary), and the chain is the shrink chain from it (substituting through the dependent inclusion proof).

theorem Hironaka.Manifold.BMO.bmoTerminal_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 → 𝕜))) (hid : BMOmod.NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hidN : NonmonomialTransformIdentityMod (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (st3 : MonomialStep3Fam 𝕜 n m) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (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')) : (bmoTerminal T m hT bo ⋯ ⋯ ⋯ st3 U hU).L ≍ (bmoTerminal (BDan.withBoundary T F' hsnc') m hT' bo ⋯ ⋯ ⋯ st3 U hU).L

The terminal lists agree across the propositionally equal canonical chains: the descents of the first step from the equal bounds have the same lists (descentStateAux_L_indiff, after substituting the bound and the number of links), and the continuations along the same chain from states with the same list have the same list (step23Aux_L_indiff, after substituting the chain).

theorem Hironaka.Manifold.BMO.bmoSeqOn_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 → 𝕜))) (hid : BMOmod.NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hidN : NonmonomialTransformIdentityMod (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (st3 : MonomialStep3Fam 𝕜 n m) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (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 { I := T.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' }) : bmoSeqOn T m hT bo ⋯ ⋯ ⋯ st3 U hU = bmoSeqOn { I := T.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' } m hT' bo ⋯ ⋯ ⋯ st3 U hU

The indifference to empty boundary members (the counterpart, for boundary members, of [Kol07, 32]) on each open, for the triple with the boundary replaced by F': the canonical chain and bound do not see the empty members, and the two runs along them have the same lists (bmoTerminal_L_indiff), so the values on U agree (the heterogeneous equality is discharged by substituting the terminal open).