The two stop clauses of the modified core of the modified first step

The modified first step of [Wlo09, Theorem 7.4.1] restricts (𝓘, 1) to the hypersurface of maximal contact H⁺ (the member Eʲ without its stopped components) and runs the modified resolution one dimension down there; the value is pushed forward (coreModOn, StepBCore.lean). Its order clause is [Kol07, Corollary 85] (coreModOn_isOfOrderGe, StepBOrder.lean). This module proves the two remaining clauses of the modified core, the stopped clause and the output clause of ClauseTools.lean, from the clauses hR8 and hR1 of the functor one dimension down, with respect to the boundary without the member, (E − Eʲ)|_U. This is the form the link of Step 2.2 uses, since E − Eʲ = E^{exc} is a sub-family both of the boundary of the triple of [Kol07, Theorem 103, Step 2.2], E^{exc} + H_r, and of the full transformed boundary (ClauseBridge.lean).

• strictTransformSeq_diff_succ_eq_preimage, strictTransformSeq_diff_stageMapAdd_eq_preimage: the stopped piece H_k \ S_k is the preimage of H \ S (the step of the induction of isClosed_strictTransformSeq_diff, iterated).
• ord_markedTransformSeq_stageMapAdd_eq_zero: the order 0 propagates along the fibre (the inner induction of notMem_center_of_ord_eq_zero, stated on its own).
• IsSmoothTransversalIdealAt.stageMapAdd_of_notMem_center: the predicate transports along a fibre no centre meets, without the hypothesis that the point is off the boundary.
• isSmoothTransversalIdealAt_of_eq_idealSheaf_of_hasSncWithProper: where J is the ideal sheaf of H and F has proper normal crossings with H, the predicate holds (the stopped case at a point of the boundary).
• OutputClause.pushforward: [Kol07, Corollary 85] for the output clause, complete: OutputClause.pushforward_of_mem_strictTransformSeq on the strict transform of S; off the strict transform of H the order is 0 (the ideal of the strict transform of H lies in the transform, idealSheaf_strictTransformSeq_le_markedTransformSeq); on the stopped piece the point lies over H \ S, where J is the ideal sheaf of H, and the predicate transports along the fibre.
• HFamData.StoppedClauseFam, HFamData.OutputClauseFam: the clauses for the data of the step at a member of maximal contact, with respect to the boundary without the member.
• coreModTraceLift, restrictedTripleMod_pullback_bundle_eq, coreModTraceLift_isOfOrderGe, coreModTraceLift_stoppedClause, coreModTraceLift_outputClause: the lower run on the trace, lifted along the bundle isomorphism, with its three clauses for the restricted triple of T|_U.
• coreModOn_stoppedClause, coreModOn_outputClause: the stopped clause of the modified core (StoppedClause.pushforward) and its output clause (OutputClause.pushforward, the stopped piece being Z_{-1} ∩ U, where 𝓘 is the ideal sheaf of Eʲ by mem_Zminus1_one_iff_isHypersurfaceIdealAt), through pushforwardBridge and the deletion of the empty blow-ups (stoppedClause_eraseEmpty, outputClause_eraseEmpty, with the order clause of [Kol07, Corollary 85] with respect to E − Eʲ).
• hFamDataMod_stoppedClauseFam, hFamDataMod_outputClauseFam: the data of the modified first step has both clauses.

Sources: the modified first step and the stop rule of [Wlo09, Theorem 7.4.1]; [Kol07, Corollary 85]; the proof of [Kol07, Lemma 102]. The statements themselves are not in the sources.

theorem AnalyticManifold.FiniteSuccession.strictTransformSeq_diff_succ_eq_preimage {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) {S H : Set M.carrier} (hSc : IsClosed S) (hSH : S ⊆ H) (hcl : IsClosed (H \ S)) (hc : B.CentersIn S) (i : Fin B.length) : B.strictTransformSeq H i.succ \ B.strictTransformSeq S i.succ = ⇑(B.map i) ⁻¹' (B.strictTransformSeq H i.castSucc \ B.strictTransformSeq S i.castSucc)

The stopped piece is the preimage of the stopped piece one stage down (the step of the induction of isClosed_strictTransformSeq_diff, stated on its own): for S ⊆ H closed with H \ S closed and the centres inside the strict transforms of S, H_{i+1} \ S_{i+1} = π_i⁻¹(H_i \ S_i).

theorem AnalyticManifold.FiniteSuccession.strictTransformSeq_diff_stageMapAdd_eq_preimage {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) {S H : Set M.carrier} (hSc : IsClosed S) (hSH : S ⊆ H) (hcl : IsClosed (H \ S)) (hc : B.CentersIn S) (i k : ℕ) (h : i + k < B.length + 1) : B.strictTransformSeq H ⟨i + k, h⟩ \ B.strictTransformSeq S ⟨i + k, h⟩ = ⇑(B.stageMapAdd i k h) ⁻¹' (B.strictTransformSeq H ⟨i, ⋯⟩ \ B.strictTransformSeq S ⟨i, ⋯⟩)

strictTransformSeq_diff_succ_eq_preimage iterated along stageMapAdd: the stopped piece at stage i + k is the preimage of the stopped piece at stage i.

theorem AnalyticManifold.FiniteSuccession.ord_markedTransformSeq_stageMapAdd_eq_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {I E₀ : M.IdealSheaf} (hge : S.IsOfOrderGe I 1 E₀) (i k : ℕ) (h : i + k < S.length + 1) {x : (S.stage ⟨i, ⋯⟩).carrier} (hx : Manifold.IdealSheaf.ord (S.markedTransformSeq I 1 ⟨i, ⋯⟩) x = 0) (y : (S.stage ⟨i + k, h⟩).carrier) (hy : (S.stageMapAdd i k h) y = x) : Manifold.IdealSheaf.ord (S.markedTransformSeq I 1 ⟨i + k, h⟩) y = 0

The order 0 propagates along the fibre (the inner induction of notMem_center_of_ord_eq_zero, stated on its own): over a point of order 0 at stage i, every point of stage i + k has order 0. A centre point has order ≥ 1 (ordAlongIdeal_le_ord_of_mem_support), so the blow-ups are local isomorphisms along the fibre and the marked transform is the pull-back there (birationalTransform_stalkIdeal_of_notMem, ord_pullback_of_isLocalDiffeomorphAt).

theorem Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt.stageMapAdd_of_notMem_center {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {I : M.IdealSheaf} {F : HypersurfaceFamily M.carrier} (hge : S.IsOfOrderGe I 1 F.idealSheaf) (hF : IsSnc ψ F) (i k : ℕ) (h : i + k < S.length + 1) {x : (S.stage ⟨i, ⋯⟩).carrier} (hP : IsSmoothTransversalIdealAt ψ (S.totalTransformSeqFrom F ⟨i, ⋯⟩) (S.markedTransformSeq I 1 ⟨i, ⋯⟩) x) (hcen : ∀ (l : ℕ) (hl : l < k) (z : (S.stage ⟨i + l, ⋯⟩).carrier), (S.stageMapAdd i l ⋯) z = x → z ∉ IdealSheaf.support (S.center ⟨i + l, ⋯⟩)) (y : (S.stage ⟨i + k, h⟩).carrier) (hy : (S.stageMapAdd i k h) y = x) : IsSmoothTransversalIdealAt ψ (S.totalTransformSeqFrom F ⟨i + k, h⟩) (S.markedTransformSeq I 1 ⟨i + k, h⟩) y

The predicate transports along a fibre no centre meets, without the hypothesis that the point is off the boundary: the predicate at a point x of stage i whose images at the stages i, …, i + k − 1 miss the centres blown up there transports to every point over it at stage i + k (totalTransform_of_notMem at each step). The hypothesis of stageMapAdd_of_forall_notMem_center that the point is off the boundary is present there so that the two persistence statements, for the predicate and for the boundary (notMem_totalTransformSeqFrom_of_forall_notMem_center, which needs it), have the same hypotheses and are applied together from those of the stopped clause; its proof does not need it, since totalTransform_of_notMem transports the predicate at every point off the centre. This form drops it, as the stopped piece lies on the other members of the boundary.

theorem Manifold.HypersurfaceFamily.isSmoothTransversalIdealAt_of_eq_idealSheaf_of_hasSncWithProper {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {H : Set M.carrier} (hH : IsClosedSubmanifold ψ H 1) {F : HypersurfaceFamily M.carrier} {J : M.IdealSheaf} {y : M.carrier} (hy : y ∈ H) (hJ : ∀ᶠ (a : ↑↧M.carrier) in nhds y, IdealSheaf.stalkIdeal J a = hH.idealSheaf.stalkIdeal a) (hFH : HasSncWithProper ψ F H 1) : IsSmoothTransversalIdealAt ψ F J y

The predicate at a point where the ideal is the ideal of a hypersurface in proper normal crossings with the boundary (the stopped case of [Wlo09, Theorem 7.4.1] at a point of the boundary): if J is the ideal sheaf of the smooth hypersurface H near y ∈ H and F has simple normal crossings with H properly, the predicate holds at y with c = 1. The chart of F at y adapted to H with proper normal crossings (hFH y hy) is restricted to where the two ideal sheaves agree; J_a = (z_{σ 0}) at the points of H (stalkIdeal_idealSheaf_eq_span) and J_a = ⊤ = (z_{σ 0}) off H; the members' coordinates avoid σ by properness.

theorem AnalyticManifold.FiniteSuccession.OutputClause.pushforward {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ S 1) (T : hS.toAnalyticManifold.FiniteSuccession) {J : M.IdealSheaf} {F : Manifold.HypersurfaceFamily M.carrier} {H : Set M.carrier} (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hFS : Manifold.HypersurfaceFamily.HasSncWithProper ψ F S 1) (hmax : ∀ (y : ↑↧M.carrier), Manifold.IdealSheaf.ord J y ≤ 1) (hT : T.IsOfOrderGe (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ J) 1 (hS.traceFamily F).idealSheaf) (hH : Manifold.IsClosedSubmanifold ψ H 1) (hSH : S ⊆ H) (hcl : IsClosed (H \ S)) (hle : hH.idealSheaf ≤ J) (hFH : Manifold.HypersurfaceFamily.HasSncWithProper ψ F H 1) (hstop : ∀ z ∈ H \ S, ∀ᶠ (a : ↑↧M.carrier) in nhds z, Manifold.IdealSheaf.stalkIdeal J a = hH.idealSheaf.stalkIdeal a) (hO : OutputClause (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) T (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ J) (hS.traceFamily F)) : OutputClause ψ (FiniteSuccession.pushforward hS T) J F

[Kol07, Corollary 85] for the output clause, complete: at a point x of the last stage with 1 ≤ ord: on the strict transform of S, OutputClause.pushforward_of_mem_strictTransformSeq; off the strict transform of H, the order is 0 (𝓘_{H_last} ≤ I_last by idealSheaf_strictTransformSeq_le_markedTransformSeq), a contradiction; on the stopped piece H_last \ S_last = g⁻¹(H \ S) (strictTransformSeq_diff_stageMapAdd_eq_preimage), x lies over a stopped point z where J is the ideal sheaf of H (hstop), the predicate holds at z (isSmoothTransversalIdealAt_of_eq_idealSheaf_of_hasSncWithProper) and transports along the fibre, which no centre meets (stageMapAdd_of_notMem_center, notMem_strictTransformSeq_of_stageMapAdd, centersIn_pushforward).

def Hironaka.Manifold.HFamData.StoppedClauseFam {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} (hf : HFamData ψ₀ s) : Prop

The stopped clause for the data of the step at a member of maximal contact (the field stopped_never_blownUp of BMOmodFam for the value at a member of maximal contact, with respect to the boundary without the member): for a triple of the class, a member j with 𝓘_{Eʲ} ≤ 𝓘^{(s-1)} and a relatively compact open, the value has the stopped clause for (𝓘|_U, (E − Eʲ)|_U). This is the form the link of Step 2.2 uses: the boundary of the triple of [Kol07, Theorem 103, Step 2.2], E^{exc} + H_r, and the full transformed boundary both contain E − Eʲ = E^{exc} as a sub-family.

Equations

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

def Hironaka.Manifold.HFamData.IsOfOrderGeEmptyMemberFam {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} (hf : HFamData ψ₀ s) : Prop

The order clause for the data of the step with respect to the boundary without the member ([Kol07, Corollary 85] at E − Eʲ): the value at a member of maximal contact is of order ≥ s for (𝓘|_U, (E − Eʲ)|_U). The normal-crossings clause is what StoppedClause.of_membersSubset and OutputClause.of_forall_mem need to change the boundary of the two clauses.

Equations

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

def Hironaka.Manifold.HFamData.OutputClauseFam {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} (hf : HFamData ψ₀ s) : Prop

The output clause for the data of the step at a member of maximal contact (the field output_isSmoothSubmanifoldIdeal of BMOmodFam at a member of maximal contact, with respect to the boundary without the member).

Equations

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

noncomputable def Hironaka.Manifold.BMOmod.coreModTraceLift {𝕜 : 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) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) ⋯.toAnalyticManifold

The lower run on the trace U ∩ H⁺, read on the bundled trace of U in H⁺ through the bundle isomorphism (the list pushforwardRestrict_eq pushes forward).

Equations

• Hironaka.Manifold.BMOmod.coreModTraceLift R T j hT U hU = (Hironaka.Manifold.BMOmod.coreModTrace R T j hT U hU).pullback ⟨⇑(⋯.restrictBundleDiffeomorph U).symm, ⋯⟩ ⋯

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

The restricted triple on H⁺, pulled back to the trace of U and along the bundle isomorphism, is the restricted triple of T|_U on the trace of H⁺ (the identification htr inside coreModOn_isOfOrderGe, stated on its own: restrictedTripleModOf_isPullbackOf with hplusRestrictMap_inclusion_eq).

theorem Hironaka.Manifold.BMOmod.coreModTraceLift_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) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (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) : (coreModTraceLift R T j hT U hU).toSuccession.IsOfOrderGe (restrictedTripleModOf (T.pullback (M.inclusion U) ⋯) j ⋯ ⋯).I 1 (restrictedTripleModOf (T.pullback (M.inclusion U) ⋯) j ⋯ ⋯).F.idealSheaf

The lifted lower run is of order ≥ 1 for the restricted triple of T|_U on the trace of H⁺ (the fact hL' inside coreModOn_isOfOrderGe, stated on its own: the order clause of the functor one dimension down pulled back along the bundle isomorphism, the triple identified by restrictedTripleMod_pullback_bundle_eq).

theorem Hironaka.Manifold.BMOmod.coreModTraceLift_stoppedClause {𝕜 : 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) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (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) (hR8 : AnalyticFamilyFunctor.StoppedClauseFam (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) R) : AnalyticManifold.FiniteSuccession.StoppedClause (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) (coreModTraceLift R T j hT U hU).toSuccession (restrictedTripleModOf (T.pullback (M.inclusion U) ⋯) j ⋯ ⋯).I (restrictedTripleModOf (T.pullback (M.inclusion U) ⋯) j ⋯ ⋯).F

The lifted lower run has the stopped clause for that restricted triple (the clause hR8 of the functor one dimension down on the trace, pulled back along the bundle isomorphism by stoppedClause_pullback).

theorem Hironaka.Manifold.BMOmod.coreModTraceLift_outputClause {𝕜 : 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) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (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) (hR1 : AnalyticFamilyFunctor.OutputClauseFam (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) R) : AnalyticManifold.FiniteSuccession.OutputClause (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) (coreModTraceLift R T j hT U hU).toSuccession (restrictedTripleModOf (T.pullback (M.inclusion U) ⋯) j ⋯ ⋯).I (restrictedTripleModOf (T.pullback (M.inclusion U) ⋯) j ⋯ ⋯).F

The lifted lower run has the output clause for that restricted triple (hR1 on the trace, pulled back by outputClause_pullback).

theorem Hironaka.Manifold.BMOmod.coreModOn_isOfOrderGe_emptyMember {𝕜 : 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) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (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) (hmax : ∀ (y : ↑↧M.carrier), Manifold.IdealSheaf.ord T.I y ≤ 1) : (coreModOn R T j hT U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I 1 ((T.pullback (M.inclusion U) ⋯).F.emptyMember j).idealSheaf

The modified core is of order ≥ 1 with respect to (𝓘|_U, (E − Eʲ)|_U) (Kol07, Corollary 85, pushforward_isOfOrderGe_of_isOfOrderGe_traceFamily, at the boundary E − Eʲ on the lifted lower run; the deletion of the empty blow-ups by isOfOrderGe_eraseEmpty). coreModOn_isOfOrderGe is the same clause with the full boundary.

theorem Hironaka.Manifold.BMOmod.coreModOn_stoppedClause {𝕜 : 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) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (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) (hmax : ∀ (y : ↑↧M.carrier), Manifold.IdealSheaf.ord T.I y ≤ 1) (hle : ⋯.idealSheaf ≤ T.I) (hR8 : AnalyticFamilyFunctor.StoppedClauseFam (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) R) : AnalyticManifold.FiniteSuccession.StoppedClause (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (coreModOn R T j hT U hU).toSuccession (T.pullback (M.inclusion U) ⋯).I ((T.pullback (M.inclusion U) ⋯).F.emptyMember j)

The stopped clause of the modified core with respect to (𝓘|_U, (E − Eʲ)|_U) (the stop rule of the modified first step of [Wlo09, Theorem 7.4.1]): StoppedClause.pushforward on the lifted lower run with S := H⁺ ∩ U and H := Eʲ ∩ U (the stopped locus is closed; 𝓘_{Eʲ} ≤ 𝓘 is the maximal contact of the member), the order clause of [Kol07, Corollary 85] with respect to E − Eʲ for the deletion of the empty blow-ups (stoppedClause_eraseEmpty), the list push-forward read through pushforwardBridge and pushforwardRestrict_eq.

theorem Hironaka.Manifold.BMOmod.coreModOn_outputClause {𝕜 : 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) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (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) (hmax : ∀ (y : ↑↧M.carrier), Manifold.IdealSheaf.ord T.I y ≤ 1) (hle : ⋯.idealSheaf ≤ T.I) (hR1 : AnalyticFamilyFunctor.OutputClauseFam (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) R) : AnalyticManifold.FiniteSuccession.OutputClause (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (coreModOn R T j hT U hU).toSuccession (T.pullback (M.inclusion U) ⋯).I ((T.pullback (M.inclusion U) ⋯).F.emptyMember j)

The output clause of the modified core with respect to (𝓘|_U, (E − Eʲ)|_U): OutputClause.pushforward on the lifted lower run. The stopped piece is Z_{-1} ∩ U, where 𝓘 is the ideal sheaf of Eʲ (mem_Zminus1_one_iff_isHypersurfaceIdealAt) and E − Eʲ has proper normal crossings with Eʲ (hasSncWithProper_emptyMember); outputClause_eraseEmpty for the deletion of the empty blow-ups.

theorem Hironaka.Manifold.BMOmod.hFamDataMod_isOfOrderGeEmptyMemberFam {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (R : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} => Manifold.AnalyticTriple.BMOClass 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) (hRc : R.CommutesWithLocalIsos) (hRi : R.IndifferentToEmptyMembers) : (hFamDataMod R ⋯ ⋯ ⋯).IsOfOrderGeEmptyMemberFam

The order clause of the data of the modified first step with respect to E − Eʲ (hFamDataMod).

theorem Hironaka.Manifold.BMOmod.hFamDataMod_stoppedClauseFam {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (R : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} => Manifold.AnalyticTriple.BMOClass 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) (hRc : R.CommutesWithLocalIsos) (hRi : R.IndifferentToEmptyMembers) (hR8 : AnalyticFamilyFunctor.StoppedClauseFam (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) R) : (hFamDataMod R ⋯ ⋯ ⋯).StoppedClauseFam

The stopped clause of the data of the modified first step (hFamDataMod, from the clause hR8 of the functor one dimension down).

theorem Hironaka.Manifold.BMOmod.hFamDataMod_outputClauseFam {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (R : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} => Manifold.AnalyticTriple.BMOClass 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) (hRc : R.CommutesWithLocalIsos) (hRi : R.IndifferentToEmptyMembers) (hR1 : AnalyticFamilyFunctor.OutputClauseFam (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) R) : (hFamDataMod R ⋯ ⋯ ⋯).OutputClauseFam

The output clause of the data of the modified first step (hFamDataMod, from the clause hR1 of the functor one dimension down).