The modified first step: the run one dimension down on H⁺, pushed forward

The modified first step of [Wlo09, Theorem 7.4.1] restricts (I′, 1) = C(H(I)) to a hypersurface of maximal contact V(u₁) and repeats the modified algorithm for the restriction I′|_{V(u₁)}. This is the core of the proof of [Kol07, Lemma 102] ("consider the triple (S, I_0|_S, E_S) … push it forward"; BDan.coreFamOn) without the first blow-up of Z_{-1} (the stop, StepBRestrict.lean): on a relatively compact open U, the value of the modified functor one dimension down, R, on the restricted triple restrictedTripleMod T j over the trace U ∩ H⁺, pushed forward to U (pushforwardRestrict, the push-forward of [Kol07, Definition 30, 30.3] on each open), with its empty blow-ups deleted [Kol07, 32]: this is coreModOn. The functor R enters only through its values. The properties of a compatible family hold: no empty centres, and compatibility under restriction (coreModOn_compat: the compatibility of R on the traces, the push-forward commuting with the open inclusions, pushforwardRestrict_pullback_restrictLE, eraseEmpty_pushforwardRestrict_eraseEmpty).

The trace of an open on H⁺ and the lower-dimensional value there

noncomputable def Hironaka.Manifold.BMOmod.coreModTrace {𝕜 : 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.restrict (⋯.preimageOpens U))

The value of the modified functor one dimension down on the restricted triple over the trace U ∩ H⁺ of a relatively compact open U ("repeated for the restriction", [Wlo09, Theorem 7.4.1]).

Equations

• Hironaka.Manifold.BMOmod.coreModTrace R T j hT U hU = (R.fam (Hironaka.Manifold.BMOmod.restrictedTripleMod T j) ⋯).seqOn (⋯.preimageOpens U) ⋯

theorem Hironaka.Manifold.BMOmod.coreModTrace_compat {𝕜 : 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 V : TopologicalSpace.Opens M.carrier} (hU : IsCompact (closure ↑U)) (hV : IsCompact (closure ↑V)) (hUV : U ≤ V) : coreModTrace R T j hT U hU = ((coreModTrace R T j hT V hV).pullback (⋯.toAnalyticManifold.restrictLE ⋯) ⋯).eraseEmpty

The compatibility of R on the traces: the value over U ∩ H⁺ is the value over V ∩ H⁺ restricted and cleaned.

The modified core

noncomputable def Hironaka.Manifold.BMOmod.coreModOn {𝕜 : 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 → 𝕜)) (M.restrict U)

The modified core on U ([Wlo09, Theorem 7.4.1]; the counterpart of BDan.coreFamOn without the first blow-up): the run one dimension down on the restricted triple over the trace U ∩ H⁺, pushed forward to U (pushforwardRestrict), with its empty blow-ups deleted [Kol07, 32]. Nothing happens over the stopped components Z_{-1} ("the algorithm is stopped").

Equations

• Hironaka.Manifold.BMOmod.coreModOn R T j hT U hU = (AnalyticManifold.BlowUpSequence.pushforwardRestrict ⋯ U (Hironaka.Manifold.BMOmod.coreModTrace R T j hT U hU)).eraseEmpty

theorem Hironaka.Manifold.BMOmod.coreModOn_eq_of_eq {𝕜 : 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) {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) S 1) (hSeq : S = hplus T j) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : coreModOn R T j hT U hU = (AnalyticManifold.BlowUpSequence.pushforwardRestrict hS U ((R.fam (restrictedTripleModOf T j hS hSeq) ⋯).seqOn (hS.preimageOpens U) ⋯)).eraseEmpty

The modified core read on a closed hypersurface S = H⁺ (a substitution).

theorem Hironaka.Manifold.BMOmod.noEmptyCenters_coreModOn {𝕜 : 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)) : (coreModOn R T j hT U hU).NoEmptyCenters

The value of the modified core has no empty centres [Kol07, 32].

theorem Hironaka.Manifold.BMOmod.coreModOn_compat {𝕜 : 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 V : TopologicalSpace.Opens M.carrier} (hU : IsCompact (closure ↑U)) (hV : IsCompact (closure ↑V)) (hUV : U ≤ V) : coreModOn R T j hT U hU = ((coreModOn R T j hT V hV).pullback (M.restrictLE hUV) ⋯).eraseEmpty

The compatibility of the modified core ([Wlo09, Theorem 2.0.3 (4)], [Wlo09, Definition 3.2.6]): the value on U ≤ V is the value on V restricted to U and cleaned, from the compatibility of R on the traces, the push-forward commuting with the open inclusions (pushforwardRestrict_pullback_restrictLE), and the deletion of empty blow-ups moved through the push-forward (eraseEmpty_pushforwardRestrict_eraseEmpty).

noncomputable def Hironaka.Manifold.BMOmod.coreModFam {𝕜 : 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) : CompatibleFamily T

The modified core as a compatible family of the triple T, in the shape the link of the maximal-contact step takes.

Equations

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

@[simp]

theorem Hironaka.Manifold.BMOmod.coreModFam_seqOn {𝕜 : 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)) : (coreModFam R T j hT).seqOn U hU = coreModOn R T j hT U hU