The modified first step: the modified core is of order ≥ 1

[Kol07, Definition 66 (2′)–(4′)] at the mark 1 for the modified core of [Wlo09, Theorem 7.4.1]: on a relatively compact open U the modified core is a smooth blow-up sequence of order ≥ 1 starting with the restricted triple (U, 𝓘|_U, E|_U); every centre has only normal crossings with the boundary and lies in the zero set of the current controlled transform. This is the counterpart of BDan.coreOfListOf_isOfOrderGe_of_bridge and coreFamOn_isOfOrderGe without the first blow-up.

The argument: the run one dimension down on the trace U ∩ H⁺ is of order ≥ 1 for the restricted triple (the order clause of the lower functor, a hypothesis here), pulled back along the bridge to the bundled trace; [Kol07, Corollary 85] with the hypersurface in the boundary (FiniteSuccession.pushforward_isOfOrderGe_append: 𝓘|_U is trivially D-balanced at the mark 1 and of order ≤ 1) pushes the order clause forward, with the boundary (E − E^j) + Z_{-1} + H⁺: the member E^j = Z_{-1} ⊔ H⁺ is read as its two clopen pieces (stopLocus_union_hplus), the stopped piece Z_{-1} being a closed hypersurface in proper normal crossings with E − E^j (hasSncWithProper_stopLocus) and disjoint from H⁺ (hasSncWithProper_append_of_notMem), so that the reduced ideal sheaves of (E − E^j) + Z_{-1} + H⁺ and of E coincide (idealSheaf_congr_support: the same support), and the trace of Z_{-1} on H⁺ is empty (the ideal sheaf of the lower boundary is unchanged). The succession of the pushed-forward list is the push-forward of the succession (pushforwardBridge), and the deletion of empty blow-ups keeps the order clause (isOfOrderGe_eraseEmpty).

The stopped locus as a closed hypersurface in proper normal crossings with E − E^j

theorem Hironaka.Manifold.BMOmod.stopLocus_subset {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) : stopLocus T j ⊆ T.F.hyp j

theorem Hironaka.Manifold.BMOmod.mem_stopLocus_of_notMem_hplus {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) {x : M.carrier} (hx : x ∈ T.F.hyp j) (h : x ∉ hplus T j) : x ∈ stopLocus T j

theorem Hironaka.Manifold.BMOmod.stopLocus_union_hplus {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) : stopLocus T j ∪ hplus T j = T.F.hyp j

E^j = Z_{-1} ⊔ H⁺.

theorem Hironaka.Manifold.BMOmod.isAdaptedChart_stopLocus_restrOpen {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) {φ : OpenPartialHomeomorph M.carrier (Fin n → 𝕜)} {σ : Fin 1 ↪ Fin n} (h : Manifold.IsAdaptedChart (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (T.F.hyp j) φ σ) : Manifold.IsAdaptedChart (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (stopLocus T j) (φ.restrOpen (hplus T j)ᶜ ⋯) σ

An adapted chart of E^j, restricted to the complement of H⁺, is an adapted chart of the stopped locus (the mirror image of isAdaptedChart_hplus_restrOpen).

theorem Hironaka.Manifold.BMOmod.hasSncWithProper_stopLocus {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) : Manifold.HypersurfaceFamily.HasSncWithProper (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (T.F.emptyMember j) (stopLocus T j) 1

The boundary E − E^j has simple normal crossings with the stopped locus, properly (the mirror image of hasSncWithProper_hplus: the proper charts of E^j restricted off H⁺).

theorem Hironaka.Manifold.BMOmod.stopLocus_pullback {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g) : stopLocus (T.pullback g hg) j = ⇑g ⁻¹' stopLocus T j

The stopped locus pulls back along local analytic isomorphisms (Zminus1_comap).

The order clause

theorem Hironaka.Manifold.BMOmod.hplusRestrictMap_inclusion_eq {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) (U : TopologicalSpace.Opens M.carrier) : hplusRestrictMap T j (M.inclusion U) ⋯ = ContMDiffMap.comp (⋯.toAnalyticManifold.inclusion (⋯.preimageOpens U)) ⟨⇑(⋯.restrictBundleDiffeomorph U).symm, ⋯⟩

The restriction g|_{H⁺} for the open inclusion g = (U ⊆ M) is the inclusion of the trace U ∩ H⁺ composed with the bridge (both maps are the inclusion of the subtype).

theorem Hironaka.Manifold.BMOmod.coreModOn_isOfOrderGe {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (R : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} => Manifold.AnalyticTriple.BMOClass 1) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (hmax : ∀ (y : ↑↧M.carrier), Manifold.IdealSheaf.ord T.I y ≤ 1) (hRo : ∀ {N : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) N) (hT' : Manifold.AnalyticTriple.BMOClass 1 T') (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')), ((R.fam T' hT').seqOn U' hU').toSuccession.IsOfOrderGe (T'.pullback (N.inclusion U') ⋯).I 1 (T'.pullback (N.inclusion U') ⋯).F.idealSheaf) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : (coreModOn R T j hT U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I 1 (T.pullback (M.inclusion U) ⋯).F.idealSheaf

The modified core is of order ≥ 1 ([Kol07, Definition 66 (2′)–(4′)] at the mark 1, on each open; the counterpart of coreFamOn_isOfOrderGe without the first blow-up): the order clause of the run one dimension down on the trace, pulled back along the bridge, pushed forward by [Kol07, Corollary 85] with E^j = Z_{-1} ⊔ H⁺ read as two boundary members, the deletion of empty blow-ups keeping the clause.