The modified first step: the modified core is indifferent to empty boundary members

The counterpart, for boundary members, of the empty blow-up convention [Kol07, 32], for the modified first step of [Wlo09, Theorem 7.4.1]: deleting empty members of the boundary along an order embedding e : F'.ι ↪o E.ι of the index types does not change the modified core at a kept member. This is the counterpart of BDan.coreFamOn_indifferentToEmptyMembers without the first blow-up.

The stopped locus and H⁺ of the member e i of E are those of the member i of F' (hplus_withBoundary: the same set E^{e i} = F'^i and the same ideal), so the two modified cores are read on the same closed hypersurface (coreModOn_eq_of_eq); the two restricted triples have the same ideal (the pull-back of 𝓘 along the same inclusion) and boundaries, the traces of E − E^{e i} and of F' − F'^i, which correspond along e with the deleted members empty, so the indifference of the functor R one dimension down (a hypothesis here) identifies the two values on the trace, and the push-forward and the deletion of empty blow-ups are the same.

theorem Hironaka.Manifold.BMOmod.hplus_withBoundary {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin 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) (i : F'.ι) : hplus (BDan.withBoundary T F' hsnc') i = hplus T (e i)

H⁺ does not see the deleted members: the member i of F' is the member e i of E, and the ideal is the same.

theorem Hironaka.Manifold.BMOmod.restrictedTripleModOf_F_hyp_apply {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin 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) (i : F'.ι) {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) S 1) (hSeq : S = hplus T (e i)) (hSeq' : S = hplus (BDan.withBoundary T F' hsnc') i) (k : F'.ι) : (restrictedTripleModOf T (e i) hS hSeq).F.hyp (e k) = (restrictedTripleModOf (BDan.withBoundary T F' hsnc') i hS hSeq').F.hyp k

The trace of E − E^{e i} at the member e k is the trace of F' − F'^i at k (both empty at k = i; E^{e k} = F'^k otherwise).

theorem Hironaka.Manifold.BMOmod.restrictedTripleModOf_F_hyp_eq_empty {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (F' : Manifold.HypersurfaceFamily M.carrier) (e : F'.ι ↪o T.F.ι) (i : F'.ι) (he' : ∀ b ∉ Set.range ⇑e, T.F.hyp b = ∅) {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) S 1) (hSeq : S = hplus T (e i)) (b : T.F.ι) (hb : b ∉ Set.range ⇑e) : (restrictedTripleModOf T (e i) hS hSeq).F.hyp b = ∅

The trace of E − E^{e i} at a member outside the range of e is empty.

theorem Hironaka.Manifold.BMOmod.coreModOn_indifferentToEmptyMembers {𝕜 : 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) (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) (i : F'.ι) (he' : ∀ b ∉ Set.range ⇑e, T.F.hyp b = ∅) (hRi : R.IndifferentToEmptyMembers) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (hT₂ : Manifold.AnalyticTriple.BMOClass 1 (BDan.withBoundary T F' hsnc')) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : coreModOn R T (e i) hT U hU = coreModOn R (BDan.withBoundary T F' hsnc') i hT₂ U hU

The modified core is indifferent to empty boundary members (the counterpart, for boundary members, of [Kol07, 32]; the analogue of BDan.coreFamOn_indifferentToEmptyMembers without the first blow-up): the modified core at the member e i of E is the modified core at the member i of F'; the same H⁺, the same restricted ideal, the boundaries corresponding along e, and the functor R one dimension down indifferent (hRi).

theorem Hironaka.Manifold.BMOmod.coreModFam_indifferentToEmptyMembers {𝕜 : 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) (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) (i : F'.ι) (he' : ∀ b ∉ Set.range ⇑e, T.F.hyp b = ∅) (hRi : R.IndifferentToEmptyMembers) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (hT₂ : Manifold.AnalyticTriple.BMOClass 1 (BDan.withBoundary T F' hsnc')) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : (coreModFam R T (e i) hT).seqOn U hU = (coreModFam R (BDan.withBoundary T F' hsnc') i hT₂).seqOn U hU

coreModOn_indifferentToEmptyMembers for the CompatibleFamily coreModFam.